Changes between Version 46 and Version 47 of Commentary/Compiler/GenericDeriving


Ignore:
Timestamp:
Dec 20, 2011 1:18:59 PM (4 years ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/GenericDeriving

    v46 v47  
    157157}}}
    158158
     159=== Names ===
     160
     161As an aside, note that we have to come up with names like `UU` and `KK` for the `Universe`
     162even though we really just wanted to use `U1` and `K1`, like before. Then we would have
     163a type and a constructor with the same name, but that's ok. However, `Universe` defines
     164both a type (with constructors) and a kind (with types). So if we were to use `U1` in the
     165`Universe` constructors, then we could no longer use that name in the `Interprt`
     166constructors. It's a bit annoying, because we are never really interested in the type
     167`Universe` and its constructors: we're only interested in its promoted variant.
     168This is a slight annoyance of automatic promotion: when you define a "singleton type"
     169(like our GADT `Interprt` for `Universe`) you cannot reuse the constructor names.
     170Oh well.
     171
    159172== Metadata representation ==
    160173{{{