On Fri, 12 Sep 2014, Tslil Clingman
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.