[TYPES] Types-list post from devriese@cs.tcd.ie requires approval

[Karl Crary]

I would add our formulation of recursive types in that paper came from 
Mendler (and can be found in the Nuprl book of Constable et al.).  I'm 
not sure to whom it is originally due.

This is the simple formulation of higher-order isorecursive types, in 
that it only forms types.  Higher-kinded recursive types are then 
encoded using it.  Others have looked at formulations in which 
higher-kinded recursive type constructors are introduced directly, at 
the cost of more complicated roll/unroll operations.  The basic idea is 
that roll/unroll operate on types taking the form of a recursive 
constructor within a context (usually an elimnation context).  I've seen 
this done fairly often.  I don't know the canonical reference, but I 
think that Rossberg's Alice ML does something like that.

    -- Karl Crary


Stephanie Weirich wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi Edsko,
>
> What you need is a higher-kinded version of Fix (parameterized  
> recursive type), with the associated fold and unfold rules. You can  
> find these rules in the paper:
>
>     Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99
>
>     http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf
>
> --Stephanie
>
>   
>> From: Edsko de Vries <devriese at cs.tcd.ie>
>> Date: January 24, 2008 11:38:26 AM EST
>> To: types-list at lists.seas.upenn.edu
>> Subject: Isorecursive types and type abstraction
>>
>>
>> (Originally sent to haskell-cafe; someone suggested posting it here)
>>
>> Hi,
>>
>> Most descriptions of recursive types state that iso-recursive types
>> (with explicit 'fold' and 'unfold' operators) are easy to typecheck,
>> and that equi-recursive types are much more difficult. My question
>> regards using iso-recursive types (explicitly, not implicitly using
>> algebraic data types) together with type abstraction and application.
>>
>> The usual typing rules for fold and unfold are
>>
>>          e :: Fix X. t
>>   -----------------------------  Unfold
>>   unfold e :: [X := Fix X. t] t
>>
>>       e :: [X := Fix X. t] t
>>   ----------------------------- Fold
>>        fold e : Fix X. t
>>
>> This works ok for the following type:
>>
>>   ListInt = Fix L. 1 + Int * L
>>
>> (where "1" is the unit type). If
>>
>>   x :: ListInt
>>
>> then
>>
>>   unfold x :: 1 + Int * ListInt
>>
>> using the Unfold typing rule. However, this breaks when using type
>> abstraction and application. Consider the polymorphic version of list:
>>
>>   List = Fix L. /\A. 1 + A * L A
>>
>> Now if we have
>>
>>   x :: List Int
>>
>> we can no longer type
>>
>>   unfold x
>>
>> because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of
>> course, we can unroll List Int by first unrolling List, and then
>> re-applying the unrolled type to Int to get
>>
>>   (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int
>>
>> which can be simplified to
>>
>>   1 + Int * List Int
>>
>> but this is not usually mentioned (that I could find; in  
>> particular, TAPL does not mention it) and I'm worried that there  
>> are subtleties here that I'm missing--nor do I have an exact  
>> definition of what this 'extended' unrolling rule should do.
>>
>> Any hints or pointers to relevant literature would be appreciated!
>>
>> Edsko
>>
>> PS. One way to simplify the problem is to redefine List as
>>
>>   List = /\A. Fix L. 1 + A * L
>>
>> so that List Int can easily be simplified to the right form (Fix ..);
>> but that can only be done for regular datatypes. For example, the  
>> nested
>> type
>>
>>   Perfect = Fix L. /\A. A + Perfect (A, A)
>>
>> cannot be so rewritten because the argument to Perfect in the  
>> recursive
>> call is different.
>>
>>
>>     
>
>
>