Changes between Version 18 and Version 19 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 3:53:38 PM (8 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