Skip to content
Pure Type System for Erlang
Branch: master
Clone or download
Latest commit 6b87671 Dec 29, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
include fix extract error Oct 26, 2017
priv/normal fix build Jul 13, 2018
src Church encoding sample Dec 29, 2018
.travis.yml fix build Dec 29, 2018 test infinite run travis Dec 29, 2018 test infinite run travis Dec 29, 2018
rebar.config cleanup Oct 1, 2017

OM: Pure Type System for Erlang

Build Status

An intermediate Om language is based on Henk languages described first by Erik Meijer and Simon Peyton Jones in 1997. Later on in 2015 a new implementation of the ideas in Haskell appeared, called Morte. It used Boehm-Berarducci encoding of recursive data types into non-recursive terms. Morte has constants, variables, and kinds, is based only on pi, lambda and apply constructions, one axiom and four deduction rules. The Om language resembles Henk and Morte both in design and in implementation. This language indended to be small, concise, easily provable, clean and be able to produce verifiable programs that can be distributed over the networks and compiled at target with safe linkage.

$ curl -fsSL > mad
$ chmod +x mad"
$ ./mad dep com pla bun om

The OM Systax is the following:

   <> ::= #option

    I ::= #identifier

    U ::= * < #number >

    O ::= U | I | ( O ) | O O
            | λ ( I : O ) → O
            | ∀ ( I : O ) → O

OM is an implementation of PTS with Infinite Number of Universes, the pure lambda calculus with dependent types. It can be compiled (code extraction) to bytecode of Erlang virtual machines BEAM and LING.

Trusted PTS with Infinite Universes

In repository OM you may found following parts of core:

OM ships with different "modes" (spaces of types with own encodings), or "preludes", which you may find in priv directory. They are selectable with om:mode("normal").


This is a minimal practical prelude similar to Morte's base library of Gabriel Gonzalez. It contains common inductive constructions encoded using plain Church (or Boehm-Berarducci if you wish) encoding, and two basic (co)monadic effect systems: IO (free monad, for finite I/O) and IOI (free comonad, for infinitary I/O, long-term processes). The generated code is being sewed with Erlang effects that are passed as parameters to pure functions.

Note: all these folders (modules) are encoded in plain CoC in OM repository to demonstrate you the basic principles how things work. Later all these should be written in EXE languages and translated to OM automatically. You may think of OM as the low-level typed assembler of type theory.


  • Maxim Sokhatsky


You can’t perform that action at this time.