[Haskell-cafe] Gödel's System T

Lauri Alanko la at iki.fi
Thu Nov 11 11:11:56 EST 2010

On Thu, Nov 11, 2010 at 04:04:07PM +0000, Aaron Gray wrote:
> On 11 November 2010 11:43, Petr Pudlak <deb at pudlak.name> wrote:
> > Thanks Dan, the book is really interesting, all parts of it. It looks like
> > I'll read the whole book.

> Watch out for the decidability issue though :-
>     http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

Just to clarify, the "issue" is that you cannot convert System F to
implicitly typed Curry-style: the explicit type abstractions and type
applications are there for a reason. For the same reason, rank-N
polymorphism in Haskell requires explicit type annotations.

There's still nothing wrong with System F as it stands, though.


More information about the Haskell-Cafe mailing list