Changes between Version 18 and Version 19 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 3:53:38 PM (9 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v18 v19  
    166166=== GADTs ===
    167167
    168  * representation
     168The internal representation of GADTs is as regular algebraic datatypes that carry coercion evidence as arguments.  A declaration like
     169{{{
     170data T a b where
     171  T1 :: a -> b -> T [a] (a,b)
     172}}}
     173would result in a data constructor with type
     174{{{
     175  T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b
     176}}}
     177This means that (unlike in the previous intermediate language) all data constructor return types have the form `T a1 ... an` where
     178`a1` through `an` are the parameters of the datatype. 
     179
     180However, we also generate wrappers for GADT data constructors which have the expected user-defined type, in this case
     181{{{
     182$wT1 = /\a b. \x y. T1 [a] (a,b) a b [a] (a,b) x y
     183}}}
     184Where the 4th and 5th arguments given to `T1` are the reflexive coercions
     185{{{
     186[a]   :: [a] :=: [a]
     187(a,b) :: (a,b) :=: (a,b)
     188}}}
    169189 
    170  * wrappers
    171 
    172 
    173190=== Representation of coercion assumptions ===
    174191
     
    216233 * simplExpr
    217234
     235=== Loose Ends ===
     236
     237Some loose ends that came up during implementation of FC:
     238
     239 * there is a strange unsafeCoerce that we could not figure out the purpose of in the FFI, a warning is currently emitted when it is used
     240
     241 * removed the -DBREAKPOINT definition in the Makefile because it induced a module loop, we should probably fix this