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

voigt@tcs.inf.tu-dresden.de wrote:

...

2009/5/24 Petr Pudlak : If all Haskell had would be HM, it would be System F.

That cannot be quite right, can it? System F has more powerful polymorphism than HM.

As I recall HM is along the edge to \lambda^2. Haskell 98 is typically described in terms of System F_\omega. I've heard people say GADTs are a subset of (or equivalent to?) System F_c, though I'm not familiar with F_c myself. Like most interesting languages, Haskell as a whole doesn't belong on one of the vertices. I've yet to see a nice diagram that presents non-vertex languages like HM and what arcs can cause one to (often unexpectedly) degenerate into another. -- Live well, ~wren

Type checking is decidable for all of the lambda cube, but not type inference. Haskell 98 is a subset of Fw, Haskell with extensions is an superset of Fw. -- Lennart On Mon, May 25, 2009 at 12:59 PM, Brent Yorgey wrote:

On Sun, May 24, 2009 at 10:39:50AM +0200, Petr Pudlak wrote:

...

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,

I don't think that's true.  Unless I am mistaken, type checking is decidable for all the vertices of the lambda cube.

...

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

I doubt it.  But there is a lot of current research into bringing as much of the power of dependent types into the language (e.g. type families) without actually bringing in all the headaches of full-spectrum dependent types.

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