Language.RM.TypeLevel

Computationally universal register machine implementation at the type-level.

This formulation is identical to the Lambek machine, with the addition of an explicit Halt instruction, for convenience.

This means (or rather, this is made possible by the fact) that that Haskell's type system is Turing complete (at least with TypeFamilies and UndecidableInstances).

Construct and run the machine

type family Run is :: Machine

Run a list of instructions (Instr)

If the program terminates, the result is a Halted machine. (See the Halting problem)

Otherwise the execution hangs the type-checker and eventually consumes all the available RAM.

Equations

Run is = Execute (Init is)

data Machine where

GADT representing the register machine

Constructors

Halted :: Label -> [Nat] -> Machine

Instructions

data Instr where

The GADT representing the intructions

The following 3 instructions are supported:

Inc r l - increments register r by 1, and then jumps to label l (that is the instruction located at index l).

Dec r l1 l2 - if the value of register r is 0, jumps to l2, otherwise decrements r and jumps to l1.

Halt - halts the machine.

The Ptr arguments are specifying the register.

Some examples

Inc (R 1) (L 1)
Dec (R 1) (L 7) (L 12)
Halt

Constructors

Inc :: Ptr -> Label -> Instr

Dec :: Ptr -> Label -> Label -> Instr

Halt :: Instr

type Inc = Inc

Alias to avoid having to tick the promoted Inc constructor

type Dec = Dec

Alias to avoid having to tick the promoted Dec constructor

type Halt = Halt

Alias to avoid having to tick the promoted Halt constructor

Operands

data Ptr where

Pointer to a register.

Constructors

Ptr :: Nat -> Ptr

type R = Ptr

Alias to avoid having to tick the promoted Ptr constructor

data Label where

Constructors

L :: Nat -> Label

type L = L

Alias to avoid having to tick the promoted L constructor