
Thanks for the thorough answer, Dan.
That's exactly what I was looking for.
During further search, I stumbled on an excellent introductory
description of recursive types in a draft of Robert Harper's book
"Programming Languages: Theory and Practice"
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
 vi
On Fri, Dec 25, 2009 at 10:48 PM, Dan Doel <[email protected]> wrote:
> On Friday 25 December 2009 11:35:38 am Vladimir Ivanov wrote:
>> Dear All,
>>
>> Recently, I've been playing with selfapplication and fixedpoint
>> combinators definition in Haskell.
>>
>> It is possible to type them in Haskell using recursive types.
>>
>> I took Y & U combinators:
>> > newtype Rec a = In { out :: Rec a > a }
>> >
>> > u :: Rec a > a
>> > u x = out x x
>> >
>> > y :: (a > a) > a
>> > y f = let uf = f . u in uf (In uf)
>>
>> Recursive types are part of System Fomega, which corresponds to
>> lambda omega in Barendregt's Lambda Cube.
>> For all type systems in Lambda Cube it is proven that they are
>> strongly normalizing. But using "y" I can easily construct a term even
>> without a normal form.
>>
>> So, I got a contradition and conclude that type system implementation
>> in Haskell contains something, that is absent from System Fomega.
>>
>> My question is: what's particular feature in Haskell type system, that
>> breaks strong normalization property? Or am I totally wrong
>> classifying it in terms of Lambda Cube?
>
> General recursive types are not part of F_omega. It only has...
>
> Â Â1) Type functions of arbitrary order
> Â Â Â/\ F : * > *. /\ T : *. F T
> Â Â2) Universal quantification over the above spaces
> Â Â ÂPi F : * > *. Pi T : (* > *) > *. T F
>
> You can encode inductive and coinductive types in such a type system. If F is
> the shape functor, then the encoding of the inductive type is:
>
> ÂPi R : *. (F R > R) > R
>
> and the encoding of the coinductive type is:
>
> ÂEx R : *. F R * R
>
> where:
>
> ÂEx R : *. T[R] = Pi Q : *. (Pi R : *. T[R] > Q) > Q
>
> and:
>
> Â A * B = Pi R : *. (A > B > R) > R
>
> (and
>
> Â A + B = Pi R : *. (A > R) > (B > R) > R
>
> if you need it to encode F R, although often one may be able to massage F into
> a more suitable form to avoid using the * and + encodings).
>
> However, as you can imagine, Rec cannot be encoded. Allowing such types adds
> general recursion back in. In type theories that do support Haskellalike
> algebraic/(co)inductive definitions (which none in the lambda cube do; they're
> plain lambda calculi), the total ones restrict what types you can declare (to
> strictly positive types, usually) to make types like Rec illegal.
>
>  Dan
>
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

