brendanzab

data Bool { T, F }

data Nat { Z, S(n: Nat) }

def (n1: Nat).eq(n2: Nat): Bool {
    Z => n2.match {
        Z => T,
        S(_) => F,
    },
    S(n1) => n2.match {

brendanzab

%% Intuitionistic type theory in Twelf by Brendan Zabarauskas
%%
%% Inspired by the examples found in “An Equational Logical Framework 
%% for Type Theories” https://arxiv.org/abs/2106.01484

tp : type.
el : tp -> type.

%% Equality

brendanzab

module type Isorecursive = sig

  type t
  type 'a layer

  val roll : t layer -> t
  val unroll : t -> t layer

end

brendanzab

module Option = struct

  type 'a shape = [
    | `Some of 'a
    | `None
  ]

  module type S = sig

    type 'a t

brendanzab

module Expr = struct

  module Layer = struct

    type 'a t =
      | Mul of 'a * 'a
      | Add of 'a * 'a
      | Int of int

    let map (f : 'a -> 'b) (layer : 'a t) : 'b t =

brendanzab

(** An evaluator for an imperative language with loop, break, and continue in
    continuation passing style. *)

type expr =
  | Var of string
  | Let of string * expr * expr
  | Seq of expr * expr

  | Unit

brendanzab

type index = int
type level = int


type expr =
  | Var of index
  | Let of string * expr * expr
  | Fun_lit of string * expr
  | Fun_app of expr * expr

brendanzab

(** Set examples in OCaml from {{:https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf}
    “On Understanding Data Abstraction, Revisited”} by William R. Cook
*)

(** ADT-style set implementations.

    See Section 2 of the paper.
*)
module Abstract_data_types = struct

brendanzab

What is a type” in the semantic domain called?

One frustration I’ve run into when making a type checker/elaborator for a programming language is the following gap in terminology:

• term¹ / value
• type / ???

This most commonly pops up when using normalisation-by-evaluation as part of a type checker, for example in the elab-system-f-bidirectional or elab-dependent projects in my language garden:

Footnotes

1. Or an “expression” ↩

brendanzab

-- UML Class diagram:
--
-- ┌───────────────────────────────────┐
-- │ BankAccount                       |
-- ├───────────────────────────────────┤
-- │ - owner : String                  |
-- │ - balance : Dollars = 0           |
-- ├───────────────────────────────────┤
-- │ + getOwner() : String             |
-- │ + getBalance() : Dollars          |