A brainfuck interpreter written in Haskell typeclasses

brainfuck.hs

{-# LANGUAGE
 TypeOperators, MultiParamTypeClasses, FunctionalDependencies,
 FlexibleInstances, UndecidableInstances
 #-}

module Brainfuck where

{- Usage:

Programs are encoded as cons-lists chained by (:-) and terminated by C0.
Input and output are encoded as a cons-list of slightly strange peano numerals:
    ...
  -3: L (C1 (C1 C0))
  -2: L (C1 C0)
  -1: L C0
   0: C0
   1: R C0
   2: R (C1 C0)
   3: R (C1 (C1 C0))
    ...

ex.
> type Prog = In :- Lb :- Out :- Dec :- Rb :- Out :- C0
> type Input = R (C1 (C1 (C1 (C1 C0)))) :- C0

To run a program, look at the type of `go` after applying the program and
then the input as arguments. As the output list is pushed to as a stack, the
chronologically last output will be at the head of the list.

GHCi:
>>> :t go (undefined :: Prog) (undefined :: Input)
go (undefined :: Prog) (undefined :: Input)
  :: C0
     :- (R C0
         :- (R (C1 C0)
             :- (R (C1 (C1 C0))
                 :- (R (C1 (C1 (C1 C0)))
                     :- (R (C1 (C1 (C1 (C1 C0))))
                         :- C0)))))

Reading from the bottom up, this shows the outputs:
  R (C1 (C1 (C1 (C1 C0)))) = 5
  R (C1 (C1 (C1 C0)))      = 4
  R (C1 (C1 C0))           = 3
  R (C1 C0)                = 2
  R C0                     = 1
  C0                       = 0
as expected from the program (,[.-].) and input (5).

-}

data Lt  -- <
data Gt  -- >
data Inc -- +
data Dec -- -
data Out -- .
data In  -- ,
data Lb  -- [
data Rb  -- ]

data C0
data C1 a

infixr :-
data a :- b

data L a
data R a

data Bf p i o l n r

class Preprocess xs ys zs | xs -> ys zs
instance Preprocess C0 C0 C0
instance (Preprocess xs ys as, Preprocess as bs cs)
  => Preprocess (Lb :- xs) (C1 ys :- bs) cs
instance Preprocess (Rb :- xs) C0 xs
instance Preprocess xs ys zs => Preprocess (Lt  :- xs) (Lt  :- ys) zs
instance Preprocess xs ys zs => Preprocess (Gt  :- xs) (Gt  :- ys) zs
instance Preprocess xs ys zs => Preprocess (Inc :- xs) (Inc :- ys) zs
instance Preprocess xs ys zs => Preprocess (Dec :- xs) (Dec :- ys) zs
instance Preprocess xs ys zs => Preprocess (Out :- xs) (Out :- ys) zs
instance Preprocess xs ys zs => Preprocess (In  :- xs) (In  :- ys) zs

class Step x y | x -> y

instance Step (Bf (Lt :- ps) is os ls n (r :- rs)) (Bf ps is os (n :- ls) r rs)
instance Step (Bf (Lt :- ps) is os ls n C0) (Bf ps is os (n :- ls) C0 C0)
instance Step (Bf (Gt :- ps) is os (l :- ls) n rs) (Bf ps is os ls l (n :- rs))
instance Step (Bf (Gt :- ps) is os C0 n rs) (Bf ps is os C0 C0 (n :- rs))

instance Succ n n' => Step (Bf (Inc :- ps) is os ls n rs) (Bf ps is os ls n' rs)
instance Succ n' n => Step (Bf (Dec :- ps) is os ls n rs) (Bf ps is os ls n' rs)

instance Step (Bf (Out :- ps) is os ls n rs) (Bf ps is (n :- os) ls n rs)

instance Step (Bf (In :- ps) (i :- is) os ls n rs) (Bf ps is os ls i rs)
instance Step (Bf (In :- ps) C0 os ls n rs) (Bf ps C0 os ls (L C0) rs)

instance Step (Bf (C1 p :- ps) is os ls C0 rs) (Bf ps is os ls C0 rs)
instance Eval (Bf p is os ls (L n) rs) (Bf C0 is' os' ls' n' rs')
  => Step (Bf (C1 p :- ps) is os ls (L n) rs) (Bf (C1 p :- ps) is' os' ls' n' rs')
instance Eval (Bf p is os ls (R n) rs) (Bf C0 is' os' ls' n' rs')
  => Step (Bf (C1 p :- ps) is os ls (R n) rs) (Bf (C1 p :- ps) is' os' ls' n' rs')

class Succ x y | x -> y, y -> x
instance Succ C0 (R C0)
instance Succ (L C0) C0
instance Succ (L (C1 n)) (L n)
instance Succ (R n) (R (C1 n))

class Eval x y | x -> y
instance Eval (Bf C0 i o l n r) (Bf C0 i o l n r)
instance
  ( Step (Bf (p :- ps) i o l n r) (Bf p' i' o' l' n' r')
  , Eval (Bf p' i' o' l' n' r') (Bf C0 i'' o'' l'' n'' r'')
  ) => Eval (Bf (p :- ps) i o l n r) (Bf C0 i'' o'' l'' n'' r'')

class Run p i o | p i -> o where go :: p -> i -> o
instance
  ( Preprocess p p' C0
  , Eval (Bf p' i C0 C0 C0 C0) (Bf p'' i' o l' n' r')
  ) => Run p i o where
    go = undefined