Name: Anonymous 2012-08-31 13:45
implemented in Haskell's type system
data S
data K
data App a b
data X
data Y
data Z
type Eval a = Eval' a b => b
class Eval' a b | a -> b
instance Eval' S S
instance Eval' K K
instance Eval' X X
instance Eval' Y Y
instance Eval' Z Z
instance Eval' a a' => Eval' (App (App K a) b) a'
instance Eval' a a' => Eval' (App K a) (App K a')
instance Eval' (App (App a c) (App b c)) d => Eval' (App (App (App S a) b) c) d
instance (Eval' a a', Eval' b b') => Eval' (App (App S a) b) (App (App S a') b')
instance Eval' a a' => Eval' (App S a) (App S a')% ghci a.hs -XFlexibleContexts -XFlexibleInstances -XFunctionalDependencies -XMultiParamTypeClasses -XRankNTypes -XUndecidableInstances
GHCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( a.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t undefined :: Eval X
undefined :: Eval X :: X
*Main> :t undefined :: Eval (App K X)
undefined :: Eval (App K X) :: App K X
*Main> :t undefined :: Eval (App (App K X) Y)
undefined :: Eval (App (App K X) Y) :: X
*Main> :t undefined :: Eval (App (App (App S K) S) X)
undefined :: Eval (App (App (App S K) S) X) :: X