Re: [Haskell-cafe] Haskell type system and the lambda cube

2009/5/24 Petr Pudlak :

On Sun, May 24, 2009 at 12:18:40PM +0400, Eugene Kirpichov wrote:

...

Haskell has terms depending on types (polymorphic terms) and types depending on types (type families?), but no dependent types.

But how about undecidability? I'd say that lambda2 or lambda-omega have undecidable type checking, whereas Haskell's Hindley-Milner type system is decidable.

It isn't, in the presence type classes (what else could the {-# LANG UndecidableInstances #-} be for? :) ) and type families. If all Haskell had would be HM, it would be System F.

From this I get that Haskell's type system can't be one of the vertices of the cube.

Well, it surely has some features not described by the cube, but I'd leave an explanation to the gurus around here :)

(BWT, will some future version of Haskell consider including some kind of dependent types?)

Petr

...

2009/5/24 Petr Pudlak :

...

Hi, I'm trying to get some better understanding of the theoretical foundations behind Haskell. I wonder, where exactly does Haskell type system fit within the lambda cube? http://en.wikipedia.org/wiki/Lambda_cube I guess it could also vary depending on what extensions are turned on.

   Thanks, Petr _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

-- Eugene Kirpichov Web IR developer, market.yandex.ru