Implement a model of computation using a type system
My limited Haskell-fu has come up with this implementation of SK-calculus in Haskell's type system:

data S = S
data K = K
data A l r = A l r

class C i o | i -&gt; o
instance C (A (A K a) b) a
instance C (A (A (A S a) b) c) (A (A a c) (A b c))