printing `hello world!` by running a brainfuck interpreter in haskell's type system

TypeHeck.hs

{-# LANGUAGE
  DataKinds,
  KindSignatures,
  TypeFamilies,
  TypeOperators,
  UndecidableInstances
#-}

import Data.Kind (Type)
import GHC.TypeLits (AppendSymbol, Nat, Symbol, type (+), type (-), symbolVal)

data TypeHeckOp = Inc | Dec | Lft | Rgt | Out | Loop TypeHeck
type TypeHeck = [TypeHeckOp]
data TypeHeckState (m0 :: Nat) (m1 :: Nat) (m2 :: Nat) (m3 :: Nat) (memoryIndex :: Nat) (outputBuffer :: Symbol)

type family Output (typeHeckState :: Type) :: Symbol where
  Output (TypeHeckState _ _ _ _ _ outputBuffer) = outputBuffer

type family Exec (prog :: TypeHeck) (typeHeckState :: Type) :: Type where
  Exec '[] typeHeckState = typeHeckState
  Exec ('Inc ': rest) typeHeckState = Exec rest (ExecInc typeHeckState)
  Exec ('Dec ': rest) typeHeckState = Exec rest (ExecDec typeHeckState)
  Exec ('Lft ': rest) typeHeckState = Exec rest (ExecLft typeHeckState)
  Exec ('Rgt ': rest) typeHeckState = Exec rest (ExecRgt typeHeckState)
  Exec ('Out ': rest) typeHeckState = Exec rest (ExecOut typeHeckState)
  Exec ('Loop loopBody ': rest) typeHeckState = Exec rest (ExecLoop loopBody typeHeckState)

type family ExecInc (typeHeckState :: Type) :: Type where
  ExecInc (TypeHeckState m0 m1 m2 m3 0 outputBuffer) = TypeHeckState (m0 + 1) m1 m2 m3 0 outputBuffer
  ExecInc (TypeHeckState m0 m1 m2 m3 1 outputBuffer) = TypeHeckState m0 (m1 + 1) m2 m3 1 outputBuffer
  ExecInc (TypeHeckState m0 m1 m2 m3 2 outputBuffer) = TypeHeckState m0 m1 (m2 + 1) m3 2 outputBuffer
  ExecInc (TypeHeckState m0 m1 m2 m3 3 outputBuffer) = TypeHeckState m0 m1 m2 (m3 + 1) 3 outputBuffer

type family ExecDec (typeHeckState :: Type) :: Type where
  ExecDec (TypeHeckState m0 m1 m2 m3 0 outputBuffer) = TypeHeckState (m0 - 1) m1 m2 m3 0 outputBuffer
  ExecDec (TypeHeckState m0 m1 m2 m3 1 outputBuffer) = TypeHeckState m0 (m1 - 1) m2 m3 1 outputBuffer
  ExecDec (TypeHeckState m0 m1 m2 m3 2 outputBuffer) = TypeHeckState m0 m1 (m2 - 1) m3 2 outputBuffer
  ExecDec (TypeHeckState m0 m1 m2 m3 3 outputBuffer) = TypeHeckState m0 m1 m2 (m3 - 1) 3 outputBuffer

type family ExecLft (typeHeckState :: Type) :: Type where
  ExecLft (TypeHeckState m0 m1 m2 m3 memoryIndex outputBuffer) = TypeHeckState m0 m1 m2 m3 (memoryIndex - 1) outputBuffer

type family ExecRgt (typeHeckState :: Type) :: Type where
  ExecRgt (TypeHeckState m0 m1 m2 m3 memoryIndex outputBuffer) = TypeHeckState m0 m1 m2 m3 (memoryIndex + 1) outputBuffer

type family ExecOut (typeHeckState :: Type) :: Type where
  ExecOut (TypeHeckState m0 m1 m2 m3 0 outputBuffer) = TypeHeckState m0 m1 m2 m3 0 (AppendSymbol outputBuffer (NatToChar m0))
  ExecOut (TypeHeckState m0 m1 m2 m3 1 outputBuffer) = TypeHeckState m0 m1 m2 m3 1 (AppendSymbol outputBuffer (NatToChar m1))
  ExecOut (TypeHeckState m0 m1 m2 m3 2 outputBuffer) = TypeHeckState m0 m1 m2 m3 2 (AppendSymbol outputBuffer (NatToChar m2))
  ExecOut (TypeHeckState m0 m1 m2 m3 3 outputBuffer) = TypeHeckState m0 m1 m2 m3 3 (AppendSymbol outputBuffer (NatToChar m3))

type family ExecLoop (loopBody :: TypeHeck) (typeHeckState :: Type) :: Type where
  ExecLoop _ (TypeHeckState 0 m1 m2 m3 0 outputBuffer) = TypeHeckState 0 m1 m2 m3 0 outputBuffer
  ExecLoop _ (TypeHeckState m0 0 m2 m3 1 outputBuffer) = TypeHeckState m0 0 m2 m3 1 outputBuffer
  ExecLoop _ (TypeHeckState m0 m1 0 m3 2 outputBuffer) = TypeHeckState m0 m1 0 m3 2 outputBuffer
  ExecLoop _ (TypeHeckState m0 m1 m2 0 3 outputBuffer) = TypeHeckState m0 m1 m2 0 3 outputBuffer
  ExecLoop loopBody typeHeckState = ExecLoop loopBody (Exec loopBody typeHeckState)

type family NatToChar (n :: Nat) :: Symbol where
  NatToChar 32 = " "
  NatToChar 33 = "!"
  NatToChar 44 = ","
  NatToChar 100 = "d"
  NatToChar 101 = "e"
  NatToChar 104 = "h"
  NatToChar 108 = "l"
  NatToChar 111 = "o"
  NatToChar 114 = "r"
  NatToChar 119 = "w"

{-
  >++++++++++[
    <++++++++++>-
    ]
  <++++.---.+++++++..+++.>>+++++[
    <+++++++>-
    ]
  <---.>+++++++++[
    <+++++++++>-
    ]
  <++++++.<.+++.------.--------.>>>++++[
    <++++++++>-
    ]
  <+.
-}
type HelloWorldProg = [
  'Rgt, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Loop '[
    'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Rgt, 'Dec
    ],
  'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Out, 'Dec, 'Dec, 'Dec, 'Out, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Out, 'Out, 'Inc, 'Inc, 'Inc, 'Out, 'Rgt, 'Rgt, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Loop '[
    'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Rgt, 'Dec
    ],
  'Lft, 'Dec, 'Dec, 'Dec, 'Out, 'Rgt, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Loop '[
    'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Rgt, 'Dec
    ],
  'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Out, 'Lft, 'Out, 'Inc, 'Inc, 'Inc, 'Out, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Out, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Dec, 'Out, 'Rgt, 'Rgt, 'Rgt, 'Inc, 'Inc, 'Inc, 'Inc, 'Loop '[
    'Lft, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Inc, 'Rgt, 'Dec
    ],
  'Lft, 'Inc, 'Out
  ]

helloWorld :: f (Output (Exec HelloWorldProg (TypeHeckState 0 0 0 0 0 "")))
helloWorld = helloWorld

greet :: String
greet = symbolVal helloWorld

main :: IO ()
main = putStrLn greet