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          |

brendanzab

#![allow(dead_code)]

#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum Type {                             // t ::=
    Unit,                               //   | ()
    Int,                                //   | Int
    Float,                              //   | Float
}

type Expr = Box<ExprNode>;

brendanzab

(** This is a demonstration of implementing interpreters in an extensible way
    that offers a partial solution to the expression problem. The idea is that
    the language can be extended with more features after the fact, without
    altering previous definitions. It also has the benefit of grouping the
    related extensions to the syntax and semantic domains together with the
    relevant evaluation rules in a per-feature way.

    This approach used is similar to the one described by Matthias Blume in
    {{:https://www.microsoft.com/en-us/research/video/records-sums-cases-and-exceptions-row-polymorphism-at-work/}
    Records, sums, cases, and exceptions: Row-polymorphism at work}.

brendanzab

// WARNING: I have never programmed in gleam before and this is probably 
// considered very unideomatic/cursed. You have been warned! :P

import gleam/io
import gleam/option.{type Option, None, Some}

type Iterator(a) {
  Iterator(next: fn () -> Option(#(a, Iterator(a))))
}

brendanzab

(* Based on https://effekt-lang.org/examples/comefrom.html *)

module ComeFrom () : sig

  val label : unit -> unit (* Label *)
  val try_with : ?label:(unit -> unit (* E *)) -> ('a -> 'b (* Label *)) -> 'a -> 'b (* E *)

end = struct

  type 'a Effect.t += Label : unit Effect.t

brendanzab

-- ------------------------------- --
-- Base types                      --
-- ------------------------------- --

data Top {
    Unit,
}

data Bot { }

brendanzab

-- ------------------------------- --
-- Non-dependent functions         --
-- ------------------------------- --

codata Fun(a b: Type) {
    Fun(a, b).ap(a b: Type, x: a) : b,
}

-- ------------------------------- --
-- Top type                        --

brendanzab

use std::hash::Hash;

pub trait Key {
  type T: Hash + Eq;
}

pub trait Map<K : Key> {
  type T<V>;

  fn new<V>() -> Self::T<V>;

brendanzab

(* inspired by https://github.com/Tobi-3/build-systems-a-la-carte-with-effect-handlers/*)

type key = string
type value = int

type _ Effect.t +=
  | Fetch : key -> value Effect.t
  | NeedInput : key -> value Effect.t
  | GetValue : key -> value option Effect.t
  | SetValue : key * value -> unit Effect.t