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

[Lauri Alanko]

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=10.1.1.6.6483

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.


Lauri