Changes between Version 22 and Version 23 of IntermediateTypes


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

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v22 v23  
    173173would result in a data constructor with type
    174174{{{
    175   T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b
     175T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b
    176176}}}
    177177This means that (unlike in the previous intermediate language) all data constructor return types have the form `T a1 ... an` where
     
    223223In the paper we'd write
    224224{{{
    225         axiom CoT : (forall t. T t) :=: (forall t. [t])
     225axiom CoT : (forall t. T t) :=: (forall t. [t])
    226226}}}
    227227and then when we used `CoT` at a particular type, `s`, we'd say
    228228{{{
    229         CoT @ s
     229CoT @ s
    230230}}}
    231231which encodes as `(TyConApp instCoercionTyCon [TyConApp CoT [], s])`