register-machine-typelevel: A computationally universal register machine implementation at the type-level

[ bsd3, language, library ] [ Propose Tags ]

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).


[Skip to Readme]

Modules

[Index]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0
Dependencies base (>=4.8 && <=4.9) [details]
License BSD-3-Clause
Author Csongor Kiss
Maintainer kiss.csongor.kiss@gmail.com
Category Language
Home page https://github.com/kcsongor/register-machine-type
Source repo head: git clone https://github.com/kcsongor/register-machine-type
Uploaded by kcsongor at 2016-04-04T23:01:31Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 797 total (5 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-04-04 [all 1 reports]

Readme for register-machine-typelevel-0.1.0.0

[back to package description]

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