[Haskell-cafe] Haskell type system and Barendregt's Lambda Cube classification

[Vladimir Ivanov]

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 <dan.doel at gmail.com> wrote:
> On Friday 25 December 2009 11:35:38 am Vladimir Ivanov wrote:
>> Dear All,
>>
>> Recently, I've been playing with self-application and fixed-point
>> 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 F-omega, 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 F-omega.
>>
>> 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 Haskell-alike
> 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
>