[Haskell-cafe] Hello and type-level SKI
Jay Sulzberger
jays at panix.com
Sat Sep 13 04:06:09 UTC 2014
On Fri, 12 Sep 2014, Brandon Allbery <allbery.b at gmail.com> wrote:
> On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger <jays at panix.com> 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 at gmail.com ballbery at sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
>
More information about the Haskell-Cafe
mailing list