what-is-a-type-value-called.md

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:

type tm = ..
type ty = ..

type value = ..
type ??? = ..     (* What do I call the “type” version of a value? *)

Some solutions that I’ve tried in the past, non of which I’m fully happy with:

type tm = ..
type ty = ..

type vtm = ..
type vty = ..

type expr = ..
type ty = ..

type vexpr = ..
type vty = ..

module Syntax = struct
  type expr = ..
  type ty = ..
end

module Semantics = struct
  type expr = ..
  type ty = ..
end

Footnotes

1. Or an “expression” ↩