Henk — Pure Type System for Erlang VM

Abstract

Henk is a minimal yet powerful functional programming language based on the top vertice of Henk Barendregt's λ-Cube — Pure Type System (or Thierry Coquand's Calculus of Inductive Constructions). It implements the λPω logic, similar to Morte, but uses countable universes and a friendly Miranda-style syntax. Henk serves as an intermediate minimal fibrational proto language for the whole Groupoid Infinity stack, providing a sound foundation for theorem proving in higher languages with general induction principle like Frank and Christine.

Key features include Church encoding of all inductive data types, a robust FFI system for Erlang integration, and native support for Let-bindings and Case-expressions to bridge the gap between pure PTS and practical execution for constrained environments.

Multilingual Core

Henk supports multiple surface syntaxes, allowing for both higher-level mathematical modeling and low-level lambda programming.

AUT-68 (Automath)

Original AUT-68 by Nikolaas Govert de Bruijn. Designed for low-level Calculus of Construction programming and formal mathematical verification.

-- head
(a: *) (xs: [email protected] a) xs ([email protected] a)
((x: a) (_: [email protected] a) Maybe.Just.main a x)
(Maybe.Nothing.main a)

-- foldr
(a: *) (b: *) (f: [x: a] [y: b] b) (z: b) (xs:
[List: *] [Cons: [head: a] [tail: List] List]
[Nil: List] List) xs ([List: *] [Cons: [head:
a] [tail: List] List] [Nil: List] List) ((head:
a) (tail: b) f head tail) z

-- map
(a: *) (b: *) (f: [_ : a] b) (xs: [List: *] [Cons:
[head: a] [tail: List] List] [Nil: List] List) xs
([List: *] [Cons: [head: b] [tail: List] List]
[Nil: List] List) ((head: a) (tail: [List: *]
[Cons: [head: b] [tail: List] List] [Nil: List]
List) (List: *) (Cons: [head: b] [tail: List]
List) Nil: List) Cons (f head)(tail List Cons Nil))
((List: *) (Cons: [head: b] [tail: List] List)
(Nil: List) Nil)

Minimalist, binder-driven syntax for categorical foundational proofs.

Miranda-style

Miranda by David Turner. The root of Haskell-like languages, optimized for higher programming purposes and readability.

module Data.List where

head x = case x of
    Nil  -> Nothing
    Cons h t -> Just h

foldr f z xs = case xs of
    Nil      -> z
    Cons h t -> f h t

map f xs = case xs of
    Nil      -> Nil
    Cons h t -> Cons (f h) t

Familiar, expressive syntax for practical functional engineering.

Proven Semantics

Compact Formal Core

The core of Henk consists of 5 fundamental AST nodes of the single type called Dependent Type Pi, the fibrational generalization of functions from algebraic geometry:

type term =
  | Var of name
  | Universe of level
  | Pi of name * term * term
  | Lam of name * term * term
  | App of term * term

Operational Semantics

Henk leverages Definition Equality and β-reduction. Inductive types are represented as their own elimination principles (Church encoding). The compiler performs type erasure on Universes and Pi types, extracting pure runtime terms to Erlang Abstract Format.

Infinitary I/O

Henk supports two distinct models of side-effects, both purely represented within the Type System.

Recursive (Monad)

The Monadic IO model uses a Church-encoded Free Monad. It is suitable for sequential imperative-style programs.

module Test.Recursive where
import Control.IO

echo = io_bind io_get_line (\s -> io_put_line s)

main = replicate_io five echo

View Source
REPL: run_io Test.Recursive.main

Corecursive (Comonad)

The Comonadic IOI model represents IOI as an infinite state machine (anamorphism). It is the canonical model for long-running servers.

module Test.Corecursive where
import Control.IOI

step m = case m of
    Nothing -> iof_get_line_f (\s -> Just Any s)
    Just s  -> iof_put_line_f s (Nothing Any)

main = mk_io Any (Maybe Any) (Nothing Any) step

View Source
REPL: run_ioi Test.Corecursive.main

Continuous Practicum

$ mix henk.base --syntax=miranda
Compiling Henk base library...
  Compiling [miranda] priv/henk/Control/IO.henk -> Control.IO... OK
  Compiling [miranda] priv/henk/Control/IOI.henk -> Control.IOI... OK
  Compiling [miranda] priv/henk/Data/Bool.henk -> Data.Bool... OK
  Compiling [miranda] priv/henk/Data/Fin.henk -> Data.Fin... OK
  Compiling [miranda] priv/henk/Data/List.henk -> Data.List... OK
  Compiling [miranda] priv/henk/Data/Maybe.henk -> Data.Maybe... OK
  Compiling [miranda] priv/henk/Data/Nat.henk -> Data.Nat... OK
  Compiling [miranda] priv/henk/Data/Prod.henk -> Data.Prod... OK
  Compiling [miranda] priv/henk/Prelude.henk -> Prelude... OK

Henk base library compilation finished.

$ mix henk.repl --syntax=miranda
🧊 Henk Programming Language version 11.3.15 [miranda syntax]
Copyright (c) 2015-2026 Groupoid Infinity
https://groupoid.github.io/henk/

miranda> :eval map
TYPE: (f : Any) -> (xs : Any) -> Any
TERM: \f -> \xs -> xs Any Nil (\h -> \t -> Cons (f h) t)
miranda> :check map
TYPE: (f : Any) -> (xs : Any) -> Any
miranda> map id
= \xs -> xs Any Nil (\h -> \t -> Cons (id h) t)
miranda> :eval map id [1]
TYPE: Any
TERM: \x2 -> \R -> \nil -> \cons -> cons (Nil Any) x2
miranda>