Re: [Haskell-cafe] Hello and type-level SKI

On Fri, 12 Sep 2014, Brandon Allbery wrote:

On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger wrote:

...

But this is impossible! The type system of Haskell can be handled by a Hindley-Milner-Damas style type checker. Such a type checker always comes to a halt with a Yea or Nay answer. So one cannot get a simulation of the combinators S, K, I inside the Haskell type system.

What have I misunderstood? And, in case GHC really does now handle stuff beyond the HMD horizon, what does the New Core language look like?

Standard Haskell is (or was) H-M extended with typeclasses. GHC moved beyond that years ago; internally it's System Fw ( http://en.wikipedia.org/wiki/System_F#System_F.CF.89), and its Core language reflects this.

Thanks, Brandon! OK, so the way one simulates, ridiculous word, a Turing machine is to write code for a function in Haskell. The (simulation of) running of the Turing machine, if I understand correctly, is Haskell's attempt to calculate a type for the function. Specifically, the type inferencer's attempt. I will look at the implementation of S, K, and I, and try to figure out how this works. oo--JS.

-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net