# register-machine-type

Universal Register Machine implemented at the type-level of Haskell

*This is just a proof of concept!*

The machine consists of a set of registers, a contiguous instruction pool (starting at index 0)
and supports the following 3 instructions:
- `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.

This formulation is identical to the Lambek machine, with the addition of an explicit `Halt`

instruction, for convenience. This means that that Haskell's type system is Turing complete (with TypeFamilies and UndecidableInstances).

If the execution of a given program terminates, it will result in the type `Halted ip rs`

, where `ip`

is the
index of the instruction that halted the machine (there might be multiple `Halt`

instructions in the code)
and `rs`

is a list representing the resulting state of the registers.

Since the machine is implemented at the type-level of Haskell, the instructions are executed during
the type-checking phase. This means that a program that doesn't terminate will hang the type-checker.

(Be careful with using an on-the-fly type checker editor plugin, as checking a
non-terminating (or even a relatively complex) program will consume **a lot** of RAM!)

### An example

Initialises R1 to 5, then raises 2 to the power of the value of R1,
leaving the result (32) in R0. Uses R2 as a scratch register,
thus the machine is initialised with 3 registers.

```
pow2 :: ('Halted a (r ': rs) ~
Run
'[
-- Instr | label index
-- set R1 to 5
Inc (R 1) (L 1) -- 0
, Inc (R 1) (L 2) -- 1
, Inc (R 1) (L 3) -- 2
, Inc (R 1) (L 4) -- 3
, Inc (R 1) (L 5) -- 4
-- set R0 to 1
, Inc (R 0) (L 6) -- 5
-- R0 = 2^R1
, Dec (R 1) (L 7) (L 12) -- 6
-- R2 = R0
, Dec (R 0) (L 8) (L 9) -- 7
, Inc (R 2) (L 7) -- 8
-- R0 = 2*R2
, Dec (R 2) (L 10) (L 6) -- 9
, Inc (R 0) (L 11) -- 10
, Inc (R 0) (L 9) -- 11
, Halt -- 12
]) => Proxy r
pow2 = Proxy
```

# TODO

- composable gadgets (that is reusable components, for these to work, their used registers and labels need to be separated)
- more examples
- formally prove correctness