Nominal Types via Energies

Introduction

The Narya project is interesting for a variety of mathematical reasons, most notably being the fact that it is the first proof assistant to attempt to support Higher Observational Type Theory. However, quite apart from these mathematical innovations, the Narya source code is a treasure trove of elaborator implementation techniques which I have not seen anywhere else.

One of these techniques has to do with nominality. In Narya, one can have two definitions that look like this:

def MyPair : Type := sig ( fst : Nat, snd : Nat )
def YourPair : Type := sig ( fst : Nat, snd : Nat )

and Narya treats MyPair and YourPair as two non-convertible types. This is different from the way most languages handle nominal types, which is by having dedicated top-level declarations. For instance, in Haskell (using OverloadedRecordDot and NoFieldSelectors so that field names don’t clash), we would write

data MyPair = MyPair { fst :: Nat, snd :: Nat }
data YourPair = YourPair { fst :: Nat, snd :: Nat }

If we instead wrote

type MyPair = (Nat, Nat)
type YourPair = (Nat, Nat)

then MyPair and YourPair would be convertible. In other words, Narya uses def for both new nominal types and type synonyms, while Haskell distinguishes these two cases with data and type respectively.

One benefit of Narya’s approach is that we can actually do some computation before hitting the sig. For instance, as is found in the Narya docs, we can make a type like the following:

def Covec (A : Type) (n : Nat) : Type := match n [
| zero. ↦ sig ()
| suc. n ↦ sig ( car : A, cdr : Covec A n )]

Covec A (suc. n) then behaves as a record type with fields .car and .cdr, but it is not convertable with any previously existing record type; it is a totally fresh record type.

To me, this seemed very magical until I spent a lot of time reading the comments in the Narya source code. I now have a slightly better understanding of how it works, and I want to share this understanding with the world.

This understanding takes the form of a SOGAT treatment, because that’s how I think these days. The following SOGATification of Narya’s implementation strategy is original to me, and I don’t know if it is correct (either in a mathematical sense or in the sense of accurately modeling what’s going on in Narya).

SOGAT Treatment

A typical dependent type theory would start with the following two judgment types.

\[\begin{align*} &\ms{Ty} \colon \ms{Type} \\ &\ms{El} \colon \ms{Ty} \to \ms{Type}^+ \end{align*}\]

In Narya’s type theory, we instead start with the following (the potential/kinetic nomenclature is, as far as I know, due to Shulman).

\[\begin{align*} &\mb{data}\:\:\ms{Energy}\colon \ms{Type}\:\:\mb{where} \\ &\quad\mb{Kinetic} \colon \ms{Energy} \\ &\quad\mb{Potential} \colon \ms{Energy} \\ &\ms{Ty} \colon \ms{Type} \\ &\ms{El} \colon\ms{Energy} \to \ms{Ty} \to \ms{Type} \\ &\ms{El}_K := \ms{El}\,\mb{Kinetic} \\ &\ms{El}_P := \ms{El}\,\mb{Potential} \\ &\ms{BehavesLike} \colon \{A \colon \ms{Ty}\} \to \ms{El}_K\,A \to \ms{El}_P\,A \to \ms{Prop} \end{align*}\]

The idea is that the “potential” elements describe the behavior of the “kinetic” elements, without affecting their equality. The binding structure then allows introducing a new kinetic element that behaves like a given potential element.

\[\begin{align*} &\ms{let}_P \colon \{A \colon \ms{Ty}\} \to \{B \colon \ms{Ty}\} \to (a \colon \ms{El}_P\,A) \to ((a' \colon \ms{El}_K\,A) \to \ms{BehavesLike}\,a'\,a \to \ms{El}_K\,B) \to \ms{El}_K\,B \end{align*}\]

To connect this to the earlier example, one can think of

def MyPair : Type := sig ( fst : Nat, snd : Nat )
def p : MyPair := ( fst := 1, snd := 2 )

as using the above binding structure. That is, sig ( fst : Nat, snd : Nat ) is a potential element of Type, and then the name MyPair is bound in def p ... to a fresh kinetic element of Type that behaves like sig ( fst : Nat, snd : Nat ).

We can then formulate \(\Sigma\)-types taking advantage of this (we only treat binary \(\Sigma\)-types rather than general record types for simplicity). This is somewhat tricky because there is only one kind of type; types aren’t split into kinetic and potential. Thus, in order to have a “potential type”, we need to introduce a universe. We do this via an internalization of a “small type” judgment, following Sterling’s planned approach to universes in pterodactyl.

\[\begin{align*} &\ms{Small} \colon \ms{Ty} \to \ms{Prop} \\ &\ms{U} \colon \ms{Ty} \\ &(\ms{code},\ms{decode}) \colon (A \colon \ms{Ty}) \times \ms{Small}\,A \cong \ms{El}_K\,\ms{U} \\ &\ms{el}_K\,(A \colon \ms{El}_K\,\ms{U}) := \ms{El}_K\,(\ms{decode}\,A).0 \\ &\ms{el}_P\,(A \colon \ms{El}_K\,\ms{U}) := \ms{El}_P\,(\ms{decode}\,A).0 \end{align*}\]

Then we define \(\Sigma\)-types in the following way.

\[\begin{align*} &\Sigma \colon (A \colon \ms{El}_K\,\ms{U}) \to (B \colon \ms{el}_K\,A \to \ms{El}_K\,\ms{U}) \to \ms{El}_P\,\ms{U} \\ &(\ms{pair},\ms{proj}) \colon \{A \colon \ms{El}_K\,\ms{U}\} \to \{B \colon \ms{el}_K\,A \to \ms{El}_K\,\ms{U}\} \to \{X \colon \ms{El}_K\,\ms{U}\} \to \{p \colon \ms{BehavesLike}\,X\,(\Sigma\,A\,B)\} \to \\ &\quad (a \colon \ms{el}_K\,A) \times (b \colon \ms{el}_K\,(B\,a)) \cong \ms{el}_K\,X \end{align*}\]

The idea here is that \(\ms{BehavesLike}\,X\,(\Sigma\,A\,B)\) is a “witness” to the fact that \(X\) should have the introduction, elimination, beta and eta laws of a \(\Sigma\)-type. Crucially, however, from \(\ms{BehavesLike}\,X\,(\Sigma\,A\,B)\) and \(\ms{BehavesLike}\,X'\,(\Sigma\,A\,B)\) we cannot conclude that \(X = X'\), though we can easily conclude that \(X \cong X'\).¹

Where this really starts to shine is \(\Pi\)-types. We have both kinetic and potential elements of \(\Pi\)-types, as defined in the following way.

\[\begin{align*} &\Pi \colon (A \colon \ms{Ty}) \to (B \colon \ms{El}_K\,A \to \ms{Ty}) \to \ms{Ty} \\ &(\ms{lam}_K,\ms{app}_K) \colon \{A \colon \ms{Ty}\} \to \{B \colon \ms{El}_K\,A \to \ms{Ty}\} \to ((a \colon \ms{El}_K\,A) \to \ms{El}_K\,(B\,a)) \cong \ms{El}_K\,(\Pi\,A\,B) \\ &(\ms{lam}_P,\ms{app}_P) \colon \{A \colon \ms{Ty}\} \to \{B \colon \ms{El}_K\,A \to \ms{Ty}\} \to ((a \colon \ms{El}_K\,A) \to \ms{El}_P\,(B\,a)) \cong \ms{El}_P\,(\Pi\,A\,B) \\ &(\ms{lam}_{BL},\ms{app}_{BL}) \colon \{A \colon \ms{Ty}\} \to \{B \colon \ms{El}_K\,A \to \ms{Ty}\} \to (f \colon \ms{El}_K\,(\Pi\,A\,B)) \to (f' \colon \ms{El}_P\,(\Pi\,A\,B)) \to \\ &\quad ((a \colon \ms{El}_K\,A) \to \ms{BehavesLike}\,(\ms{app}_K\,f\,a)\,(\ms{app}_P\,f'\,a)) \cong \ms{BehavesLike}\,f\,f' \end{align*}\]

This allows us to make a definition like

def MyPair (A : Type) : Type := sig ( fst : A, snd : A )

and then conclude that MyPair Nat behaves like sig ( fst : Nat, snd : Nat ).

Implementation

It’s all very well and good to have a theoretical framework for this stuff, but it wouldn’t be very useful unless it came along with an implementation strategy. This section probably won’t be comprehensible to anyone who hasn’t implemented a normalization-by-evaluation based elaborator.

First of all, we change up the data structures for syntax and values. In Narya, Shulman uses two data structures (terms and values) for nbe. I prefer to split types and values into two separate data types, so in total I have four data structures:

We can then further incorporate the kinetic/potential divide with a type parameter, using DataKinds. The syntax for a minimal version of this (not yet been tested) might look something like the following

type Name = Text

data Energy = Kinetic | Potential

-- an element of a with one more name bound
data Abs a = Abs Name a

data ElS :: Energy -> Type where
  -- BId = backwards index, aka DeBruijn index
  Var :: BId -> ElS e
  LetP :: ElS Potential -> Abs (ElS Kinetic) -> ElS Kinetic
  -- Note that while elaborating, we must perform a "smallness" check before
  -- forming `Code a`
  Code :: TyS -> ElS Kinetic
  -- kinetic/potential introduction/eliminators for pi types
  Lam :: Abs (ElS e) -> ElS e
  App :: ElS e -> ElS Kinetic -> ElS e
  -- We must again perform a "smallness" check for each of the fields before
  -- forming `Sig fs`.
  Sig :: [(Name, TyS)] -> ElS Potential
  -- Introduction/elimination for record types
  Cons :: [(Name, ElS Kinetic)] -> ElS Kinetic
  Proj :: ElS Kinetic -> Name -> ElS Kinetic

data TyS
  = U
  | Decode (ElS Kinetic)
  | Pi TyS (Abs TyS)

The trick then is to keep track of the \(\ms{BehavesLike}\) witnesses by incorporating them into neutral values. This looks something like the following:

type Env = [ElV Kinetic]

data Clo a = Clo Env Name a

data Spine
  = SId
  | SApp Spine (ElV Kinetic)
  | SProj Spine Name

data BehavesLike
  = TrueNeutral
  | BehavesLike (ElV Potential)

data ElV :: Energy -> Type where
  -- FId = forwards index, aka DeBruijn level
  VNeu :: FId -> Spine -> BehavesLike -> ElV a
  VCode :: TyV -> ElV Kinetic
  VLam :: Clo (ElS e) -> ElV e
  VSig :: Env -> [(Name, TyS)] -> ElV Potential
  VCons :: [(Name, ElV Kinetic)] -> ElV Kinetic
  
data TyV
  = VU
  | VDecode (ElV Kinetic)
  | VPi TyV (Clo TyS)

In the actual Narya source code, the values are significantly more complex because they also deal with glued evaluation, but we ignore that for simplicity.

When evaluating LetP t1 (Abs x t2) we first evaluate t1 to v1, and then evaluation t2 in a context where x is bound to the value VNeu i SId (BehavesLike v1), where i is the current context length. That is, x is bound to a fresh neutral which behaves like v1.

Now, the point here is that the BehavesLike field of VNeu is completely ignored during conversion checking, but during elaboration when we are checking against a type VDecode (VNeu i sp (BehavesLike (VSig ...))), we accept literal record syntax like [ fst := 1, snd := 2 ], and when we are elaborating projection syntax r.fst and r synthesizes a type VDecode (VNeu i sp (BehavesLike (VSig ...))), we elaborate the correct projection.

Conclusion

As mentioned before, I haven’t yet built an elaborator on these principles yet. I wanted to write this blog post before to straighten out my thoughts about this, and also to get feedback on my interpretation of kinetic/potential energy before I go to write an elaborator.

If you have any feedback on this, please comment on the accompanying mathstodon post.

1. Shulman uses the phrase “definitionally isomorphic” to describe \(X\) and \(X'\) in this situation. I believe that the precise meaning of “definitionally isomorphic” is something like: \(X\) and \(X'\) are definitionally isomorphic if either \(X\) and \(X'\) are definitionally equal, or if we have \(\ms{BehavesLike}\,X\,(F\,X_1,\ldots,X_n)\) and \(\ms{BehavesLike}\,X'\,(F\,X_1',\ldots,X_n')\) and \(X_i\) is definitionally isomorphic to \(X_i'\) for each \(i\).↩︎