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

Lennart Augustsson lennart at augustsson.net
Mon May 25 09:26:08 EDT 2009

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 <byorgey at seas.upenn.edu> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list