register-machine-typelevel alternatives and similar packages
Based on the "Language" category.
Alternatively, view register-machine-typelevel alternatives based on common mentions on social networks and blogs.
-
stylish-haskell
DISCONTINUED. Haskell code prettifier [Moved to: https://github.com/haskell/stylish-haskell] -
ministg
Ministg is an interpreter for a high-level, small-step, operational semantics for the STG machine.
InfluxDB – Built for High-Performance Time Series Workloads

* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of register-machine-typelevel or a related project?
README
register-machine-type
Universal Register Machine implemented at the type-level of Haskell
This is just a proof of concept!
Available on Hackage
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 registerr
by 1, and then jumps to labell
(that is the instruction located at indexl
).Dec r l1 l2
- if the value of registerr
is 0, jumps tol2
, otherwise decrementsr
and jumps tol1
.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