Henk: Pure Type System

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 the Böhm-Berarducci encoding of recursive data types into non-recursive terms. Morte has constants, variables, and kinds, is based only on П, λ and apply constructions, one axiom and four deduction rules. The Henk language resembles Henk design and Morte implementation. This language is 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.

$ mix deps.get
$ iex -S mix

The Henk Syntax is the following:

   <> ::= #option

    I ::= #identifier

    U ::= * < #number >

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

Henk is an implementation of PTS with an 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 an Infinite Universes

In repository henk you may find the following parts of core:

• Parser
• Typechecker
• Eraser
• Code Extractor

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

normal

henk.groupoid.space/lib/normal/
  ├── Bool
  ├── Cmd
  ├── Eq
  ├── Equ
  ├── Frege
  ├── IO
  ├── IOI
  ├── Lazy
  ├── Leibnitz
  ├── List
  ├── Maybe
  ├── Mon
  ├── Monad
  ├── Monoid
  ├── Morte
  ├── Nat
  ├── Path
  ├── Prod
  ├── Prop
  ├── Sigma
  ├── Simple
  ├── String
  ├── Unit
  └── Vector

This is a minimal practical prelude similar to Morte's base library of Gabriella Gonzalez. It contains common inductive constructions encoded using plain Church (or Böhm-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 Henk repository to demonstrate you the basic principles how things work. Later all these should be written in Per languages and translated to Henk automatically (if possible). You may think of Henk as the low-level typed assembler of type theory.

PTS

• AUTOMATH, a language for mathematics. [Nicolaas Govert de Bruijn]
• Lambda Calculi with Types [Henk Barendregt]
• The Calculus of Constructions [Thierry Coquand, Gerard Huet]
• Introduction to Generalized Type Systems [Henk Barendregt]
• Some remarks about Dependent Type Theory [Thierry Coquand]
• Henk: a typed intermediate language [Erik Meijer, Simon Peyton Jones]
• Morte: an intermediate language for super-optimizing functional programs [Gabriella Gonzalez]
• Henk: Pure Type System for Erlang [Maksym Sokhatskyi]
• Система доведення теорем з однiєю аксiомою [Maksym Sokhatskyi]

Credits

• Maksym Sokhatskyi 🇺🇦