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

On Thu, Nov 11, 2010 at 04:04:07PM +0000, Aaron Gray wrote:

On 11 November 2010 11:43, Petr Pudlak 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