[Haskell-cafe] Hello and type-level SKI

[Jay Sulzberger]

On Fri, 12 Sep 2014, Tslil Clingman <maximum.yellow at gmail.com> wrote:

> Greetings all,
>
> I've been reading this list for a short while and I thought I'd like to
> begin to contribute where possible. This message pretty much serves to
> say:
>
> - Hello, Haskell!
> - This community is great, and it's always been a great pleasure to read
>  the newsgroup(s)
> - Here is a small and likely multiply re-re-discovered `proof' of why the type
>  system is Turing Complete
>
>> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
>>   FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
>
>> data S2 x y
>> data S1 x
>> data S
>> data K1 x
>> data K
>> data I
>
>> class Apply a b c | a b -> c
>> instance Apply K x (K1 x)
>> instance Apply S x (S1 x)
>> instance Apply (S1 x) y (S2 x y)
>> instance Apply I x x
>> instance Apply (K1 x) y x
>> instance (Apply x z xz, Apply y z yz, Apply xz yz a) => Apply (S2 x y) z a
>
>> -- The core function
>> apply :: (Apply a b c) => a -> b -> c
>> apply _ _ = undefined
>> -- Hereendeththelesson --
>
>> -- For `ease of use', but not strictly necessary
>> data X
>> data Y
>> data Z
>> s = undefined :: S
>> k = undefined :: K
>> i = undefined :: I
>> x = undefined :: X
>> y = undefined :: Y
>> z = undefined :: Z
>> -- Example
>> reverse = apply (apply s (apply k (apply s i))) k
>
> I just thought I'd share this snippet here, but if this is not the right
> place, or it's too long or something please don't hesitate to let me know.
>
> Thanks for your attention,
> Yours &c.,
> Tslil

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?

oo--JS.