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{{{