Typefuck

Ah, so lovely to see you again, gentle readers. It's been a long time - and I have no explanations for my absence - but you must forgive me - after all, long does the mind dwell on mysteries, and long can mysteries dwell unseen.

But worry not, gentle readers, for I have a gift for you. As you know I have a fondness for implementing programming languages - it makes me think of kittens, polymorphic types and lockers full of stolen credit cards.

Enough to bring a nostalgic tear to anyone's eye.

Especially those who value esoteric knowledge.

Secrets await you, fair soul, who may read this code and wonder how much I had to drink.

Brainfuck implemented within the Haskell type checker

WTF:
Typefuck is a brainfuck which runs within the Haskell type checker - that is, prior to compilation. If a rationale is to be sought, it is as another proof that the GHC type checker is turing complete.

Here are the type level commands

-- | Add +
data A = A
deriving Show

-- | Minus -
data M = M
deriving Show

-- | Right >
data R = R
deriving Show

-- | Left <
data L = L
deriving Show

-- | Iterate [ ]
data I bf = I bf
deriving Show

-- | Put .
data P = P
deriving Show

-- | Get ,
data G = G
deriving Show

So the simple brainfuck program: ,>,[-<+>]<.
(which adds two numbers)

is equivalent to the Haskell type

type Add =
   Cons G
   (Cons R
   (Cons G
   (Cons (I (Cons M
            (Cons L
            (Cons A
            (Cons R Nil)))))
   (Cons L
   (Cons P Nil
   )))))


Use the Brainfuck type to evaluate.

The first type parameter represents the program, while the second represents the input.

Input and output are represented as Cons-ed linked lists of unary integers, constructed from Succ, Zero, and Neg (for negative integers)

Assert that the function 'show_type' has this type to show a value level solution for the problem (though all working is done within the type checker)

Example:

spoon@utensil:~/Desktop$ ghci
GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
Prelude> :m +Typefuck
Prelude Typefuck> show_type :: Brainfuck Add (Cons (Succ (Succ (Succ Zero))) (Cons (Succ (Succ Zero)) Nil))
Loading package syb ... linking ... done.
Loading package base-3.0.3.1 ... linking ... done.
Loading package typefuck-0.0.1 ... linking ... done.
Cons (Succ (Succ (Succ (Succ (Succ Zero))))) Nil