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

[Dan Doel]

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