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

Eugene Kirpichov ekirpichov at gmail.com
Sun May 24 05:31:33 EDT 2009


2009/5/24 Petr Pudlak <deb at pudlak.name>:
> 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 <deb at pudlak.name>:
>> > 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 at 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


More information about the Haskell-Cafe mailing list