The following is a cleaned-up transcript of three live coding lectures I delivered on the Haskell Nominal Datatypes package github / Hackage, at the Scottish Programming Languages and Verification Summer School (SPLV) 2020. Thanks to the organisers.

Lecture 1¶

View on YouTube

Setting up the environment¶

Imports¶

import Data.List
singleton :: a -> [a]
singleton x = [x]
import Data.Maybe

import Language.Nominal

Some switches¶

:set -XDeriveAnyClass -XDeriveGeneric -XDeriveDataTypeable

Ask ghci to print types of expressions after each evaluation:

:set +t -- Print an expression’s type after each evaluation
:t head -- like this

Atoms¶

Let's give ourselves three labels:

labelList = ["a","b","c"]

freshAtomsIO converts an m of labels into an m of atoms, where m is any Traversable (e.g. List).
We create a list of three atoms, one for each label.

The @ notation is just a compact way to assign a value to atomList, and simultaneously pattern-matching on it to assign values to a, b, and c. It's equivalent to

atomList <- ...
[a,b,c] = atomList

:t freshKAtomsIO
atomList@[a,b,c] <- freshAtomsIO labelList
[a,b,c]

(The argument to freshKAtomsIO just provides traversable data over which to create atoms. We don't actually use the input, aside from using it to determine how many atoms to create. This is so that if you have a list of stuff and you want an atom for each element, you can do so conveniently.)

Raw atoms aren't mean to be pretty, but we can beautify this. showAtom will pretty-print a, b, and c (but pass through d):

showAtom n = fromMaybe (show n) (elemIndex n atomList >>= \i -> return $ labelList!!i)
d <- freshAtomIO
map showAtom [a,b,c,d]

Atom is an instance of Eq and Ord:

[a < b, b < a, a == a, a == b]

(Atom-)swapping¶

We have a swapping action swp.
This acts on base datatypes with atoms ...

:t swp    
swp a b atomList
showAtom <$> swp a b [a,b,c]

... and trivially on base datatypes without atoms, like strings and integers ...

swp a b ("Hello world",42)

... but also on things that are not base datatypes, such as the function justAtom:

justAtom :: Atom -> Maybe Atom
justAtom n
 | n == a = Just a 
 | otherwise = Nothing 

justAtom' = swp a b justAtom

justAtom maps a to Just a, and its swapped version justAtom' maps b to Just b:

fmap showAtom . justAtom <$> atomList
fmap showAtom . justAtom' <$> atomList

Indeed, we can swap in showAtom itself! showAtom' maps b to "a" --- not "b", because a is an atom and "a" is a string:

showAtom' = swp a b showAtom
showAtom' <$> [a,b,c]

Swappings act both on the left and on the right of a function's definition (both on input and on output). This means that a function can "mention" atoms, but if it does so symmetrically on both sides, it may be unaffected (this is called equivariance for functions):

identityAtom :: Atom -> Atom
identityAtom n
 | n == a = a
 | n == b = b
 | n == c = c
 | otherwise = n

identityAtom' = swp a b identityAtom

showAtom . identityAtom' <$> atomList
showAtom . identityAtom' <$> atomList

Many types of atom¶

Atom is actually a synonym for KAtom Tom, where Tom is an empty datatype. So if you have an Atom, you have a Tom. You can also have atoms of other types, like KAtom Int or KAtom ().

The second type is phantom; just used to generate many types of atoms. The typechecker will put us right if we mix atoms of incorrect types (see ka == kb below):

ka <- (freshKAtomIO :: IO (KAtom Int))
ka' <- (freshKAtomIO :: IO (KAtom Int))
kb <- (freshKAtomIO :: IO (KAtom Char))

ka == ka'  -- expect a `Bool`
ka == kb  -- expect a type error

<interactive>:1:7: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Expected type: KAtom Int
        Actual type: KAtom Char
    • In the second argument of ‘(==)’, namely ‘kb’
      In the expression: ka == kb
      In an equation for ‘it’: it = ka == kb

Names¶

A name is an atom with a label. This is motivated by the very common case that atomic identifiers are identified with semantic information, such as a display name, or a type.

We can construct a name using Name, and destruct it using nameLabel and nameAtom:

:t Name  -- constructor
:t (nameLabel, nameAtom)  -- destructors

As Atom == KAtom Tom, so also Name == KName Tom. So a name has two types attached to it: the type of its atomic ID, and the type of its label. KName Tom Int is a name with a Tom-ID and an Int-label.

That's not confusing in the slightest, is it?

-- set up our atoms
ka <- (freshKAtomIO :: IO (KAtom Int))
ka' <- (freshKAtomIO :: IO (KAtom Int))
kb <- (freshKAtomIO :: IO (KAtom Char))

-- set up our names
nka = Name 42 ka
nka' = Name "forty-two" ka'
nkb = Name 42 kb

ka == ka'  -- expect a `Bool`
ka == kb  -- expect a type error

<interactive>:1:7: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Expected type: KAtom Int
        Actual type: KAtom Char
    • In the second argument of ‘(==)’, namely ‘kb’
      In the expression: ka == kb
      In an equation for ‘it’: it = ka == kb

If you thought having names with two type parameters was fun, read on to experience the theories of equality, ordering, and abstraction.

Just remember: names are used to push information around. You can put the subtleties of this into a single package ... or reinvent the wheel yourself with every instance.

Name equality and ordering¶

Names inherit equality and ordering from the atom; labels are not considered.

This has the (possibly counterintuitive) effect that names with different labels may be equal (as per Eq), whereas names with the same label may not be:

[Name "a" a == Name "b" a, Name "a" a == Name "a" b]
[Name "a" a <= Name "a" a, Name "a" a <= Name "a" b]
Name id a == Name (\x -> x * x) a

There are engineering reasons for deciding equality and ordering of names by their atomic identifiers.

Names are identifiers just like atoms. They point to semantic information (their label) and for convenience, they allow the programmer to carry this semantic information along with the identifier that refers to it.

If you don't want this and prefer e.g. a reader monad, nothing stops you from doing this. But if you do use a name, you should still be able to use your identifiers efficiently, e.g. decide their equality and sort them (e.g. for structures like Set and Map, which require Ord instances). This should hold even if the semantic information associated to the identifier is complex (e.g. a function). This is just the distinction between a thing and the representation of that thing.

Name id a is a representation of id that we have called a. Name (\x -> x * x) a is a representation of \x -> x*x that we have also called a. (You probably shouldn't do this, so don't.)

Let's create some names, and try a swapping. Note how the atoms are swapped but the strings (which have a trivial swapping action) remain unchanged:

nameList@[na, nb, nc] = uncurry Name <$> zip labelList atomList
swp a b nameList
atomList

Names with labels that mention atoms / names¶

Labels of names may contain names (think System F, where types of term-variables may mention type-variables). These are subject to swappings just like everything else:

complexNameList@[nna, nnb, nnc] = uncurry Name <$> zip nameList atomList
swp a b complexNameList

The slogan is:

Swappings always distribute.

We can swap by names instead of atoms. swpN just discards labels and calls swp. That is,

swpN na na = swp (nameAtom na) (nameAtom nb)

atomList
nameList
swp a b nameList
swpN na nb nameList
swpN nna nnb nameList

Abstractions¶

Let's recall our environment:

labelList = ["a","b","c"]
atomList@[a,b,c] <- freshAtomsIO labelList
nameList@[na, nb, nc] = uncurry Name <$> zip labelList atomList
atomList
nameList

Given a label $\alpha$, and atom a, and some data t, we can abstract the atom in that data and tag it with a label (think: $\lambda a:\alpha.t$):

:t abst'
abst' "Hello world" a na

Since a name is just a labelled atom, and in practice we may have the atom and label parcelled up as a name already, we provide a compact form in abst:

:t abst
helloWorldName = Name "Hello world" a
abst helloWorldName na 
[abst na na, abst nb nb]

Equality of abstractions¶

abst na na looks like $\lambda a.a$ and abst nb nb looks like $\lambda b. b$. Are these abstractions equal?

abst na na == abst nb nb

Actually no, but only because na is labelled by "a" and nb is labelled by "b". abst pulls the label and stores it, so that abst na na is actually more like $\lambda a:{\tt a}.a$ and abst nb nb is actually more like $\lambda b:{\tt b}.b$ (note the different labels).
This is a feature, not a bug:

Abstractions inherit the label of the name they are called with.

Let's do this again with names with labels from the unit type (), so that all labels are trivial:

nameList@[ma,mb,mc] <- freshNamesIO [(),(),()]
:t ma
abst ma ma == abst mb mb  -- think:  λa.a == λb.b
abst ma mb == abst mc mb  -- think: λa.b == λc.b

Abstraction is capturing¶

Abstraction abst captures the atomic ID of its first argument, in its second argument:

abst_ma = abst ma 
abst_mb = abst mb 
nameList
map abst_ma nameList
map abst_mb nameList

Swapping distributes as usual over everything, so we expect swp a b abst_ma and swpN ma mb abst_ma to equal abst_mb:

map (\n -> swp a b abst_ma n == abst_mb n) nameList
map (\n -> swpN ma mb abst_ma n == abst_mb n) nameList

A little more on equality of abstractions¶

Let's just revisit how names and abstractions calculate their equality:

na' = na `withLabel` "a'"  -- a name with the atomic ID of `na` but with label "a'"
nb' = nb `withLabel` "b'"  -- a name with the atomic ID of `nb` but with label "b'"
na == na' -- atomic ids equal 
nb == nb' -- atomic ids equal
abst na na == abst na' na'  -- "a" /= "a'" so labels not equal

Concretion¶

There are many ways to unpack an abstraction. Here, we consider concretion:

:t conc
[(abst na na) `conc` nb, nb] 
(abst na na) `conc` nb == nb

Note that labels are preserved by concretion. Only the atomic identifiers are affected:

nb
abst na (na, na `withLabel` "A")
abst na (na, na `withLabel` "A") `conc` nb -- the concrete atom has the atomic ID of `nb`, but retains its original label (in this case, "a")

The action of concretion if a name is not fresh, behaviour is undefined.

(na, nb)
abst na (na, nb) `conc` na -- this is fine
abst na (na, nb) `conc` nb -- this returns a result but it is not fine

You may now be trying to think of ways to statically ensure this. This is hard to do for concretion, but this package offers other ways to program on abstractions, many of which do provide static safety guarantees.

If you want safer ways to unpack abstractions, check out @@, @@:, and @@. discussed below.

Summary¶

In summary: there is nontrivial cognitive load associated to understanding how atoms, names, abstractions, and concretions are set up and behave. This is the design that I found led to the cleanest code in practice.

The bits of the above that are not needed, need not be used. If Atom is enough for you, that's fine. On the other hand, if you need to tag atoms of multiple types with complex semantic information and then manipulate it locally, then Name is your friend.

Lecture 2¶

View on YouTube

To recap Lecture 1:

There are atoms and names.
Atom is a type of atomic identifiers.
Name s is a type of atomic IDs labelled with elements of s. Think of these as an object-level type annotation, as the $s$ in $\lambda a:s.t$.
Name-equality and -ordering is inherited from the atomic IDs. Labels are ignored.
Atom = KAtom Tom and Name = KName Tom. You can substitute your favourite type for Tom, if you want multiple types of atoms.
We have swapping swp and swpN. Every type is swappable with a swapping action given by distributing uniformly into structure. In particular, swp a b $ abst x y == abst (swp a b x) (swp a b y).
There's no such thing as a single type with two plausible swapping actions. Swapping is always definable and in a unique way (if you find a counterexample, let me know). The content of a Swappable a typeclass constraint is not a true constraint on a, so much as instructions to the compiler to "switch on" the swappability machine for this type.
We have abstraction abst and concretion conc.
Abstraction is total.
Concretion is morally partial, but implemented as a total function. Correctness of freshness conditions is not handled at the Haskell type level. (This is a feature, not a bug: other parts of the machine provide such guarantees if desired.)

Basic setup¶

:set -XDeriveAnyClass -XDeriveGeneric -XDeriveDataTypeable
import Data.List
import Data.Maybe
import GHC.Generics
import Data.Generics hiding (Generic, typeOf)
import Language.Nominal.Utilities

labelList = [(),(),()]
atomList@[a,b,c] <- freshAtomsIO labelList
nameList@[ma, mb, mc] = uncurry Name <$> zip labelList atomList
nameList'@[na, nb, nc] = uncurry Name <$> zip ["a","b","c"] atomList
nameList
nameList'

Two canonical programs¶

Both programs below use abstraction to create two local scopes out of a single name. These are canonical programs for the package: if you want to reimplement Nominal in another language, you could start by making sure it correctly handles these.

-- Input a name and output two local binding scopes using that name
(\a -> (abst a a, abst a a)) ma
(abst ma ma, abst ma ma)
(\a -> (abst a a, abst a a)) ma == (abst ma ma, abst ma ma)
-- Unpack a pair of local scopes and concrete them at two names
(\(x,y) -> (x `conc` ma, y `conc` mb)) ((\a -> (abst a a, abst a a)) ma)
(ma, mb)
(\(x,y) -> (x `conc` ma, y `conc` mb)) ((\a -> (abst a a, abst a a)) ma) == (ma, mb)

An inductive datatype with binding¶

Nominal techniques were originally invented to represent inductive datatypes of syntax with binding. So let's have a go at one of these.

data UL = Var (Name ()) | App UL UL | Lam (KAbs (Name ()) UL) deriving (Eq, Generic, Data, Swappable, Show)
:t (Var, App, Lam)
[va, vb, vc] = map Var [ma, mb, mc]
[va, vb, vc]

Give ourselves a function lam to more easily generate terms with binding:

lam :: UL -> UL -> UL
lam (Var n) x = Lam $ abst n x  -- only defined if first argument is `Var n`, i.e. a "variable" in `UL`.

-- test `lam`:
lam va va
lam vb vb
lam va vb
[lam va va == lam vb vb, lam va vb == lam vb vb]

alpha-equivalence is automatic:

lam va (lam va va) == lam vb (lam va va)  -- λa.λa.a = λb.λa.a
lam va (lam va va) == lam va (lam vb vb)  -- λa.λa.a = λb.λb.b
lam vb (lam va (va `App` vb)) == lam vb (lam vb (vb `App` vb))  -- λb.λa.a b ≠  λb.λb.b b
lam vb (lam va (va `App` vb)) == lam va (lam vb (vb `App` va))  -- λb.λa.a b =  λa.λb.b a

Swappings distribute uniformly through binders just like they distribute through everything else:

App (Var ma) (Var mb)
swpN ma mb $ App (Var ma) (Var mb)
swpN ma mb (lam va va) == lam vb vb
swpN ma mb (lam va vb) == lam vb va

Capture-avoiding substitution is easily defined (there is even a typeclass for it, so we just define it as an instance).

We use a bit of "magic" from scrap-your-boilerplate (SYB) to be particularly slick, but even without this the definitions would be very easy:

:set -XLambdaCase -XTypeSynonymInstances -XFlexibleInstances -XMultiParamTypeClasses -XInstanceSigs  -- For the SYB

instance KSub (Name ()) UL UL where
   sub :: Name () -> UL -> UL -> UL
   sub v t = rewrite $ \case
      Var v' | v' == v -> Just t
      _                -> Nothing

sub ma vb (lam vb (App vb va)) == lam vc (App vc vb)  -- (λb. b a) [a ↦ b] =  λc. c b

The function fun below is an abstraction by ma of the function "abstract by ma". Yes, you can abstract atoms over functions and not just over inductive datatypes, which is significant because it means you can locally scope atoms over complex non-inductive data (more on this when we study Nom, below).

Check carefully how concretion interacts with application below:

fun = abst ma $ lam va
(fun `conc` mb) vb == lam vb vb
(fun `conc` mb) vb == lam va va
(fun `conc` ma) vb == lam va vb

The `Nom` monad¶

Let's recall our environment again:

labelList = [(),(),()]
atomList@[a,b,c] <- freshAtomsIO labelList
nameList@[ma, mb, mc] = uncurry Name <$> zip labelList atomList
complexNameList@[nna, nnb, nnc] = uncurry Name <$> zip nameList atomList

Recall abstraction. We construct Abs with abst and destruct it with conc:

:t abst
:t abst ma ma
:t abst ma ma `conc` mb

abst is also functorial:

singleton <$> abst ma ma

But how else do we manage scope, and how else can we exit and abstraction?

If conc feels imperative and unidiomatic, you are probably wanting Nom:

The `Nom` type-former¶

Enter Nom. Its constructor is res, which creates a scope of local atoms. There's also a resN variant which takes a list of names, strips their labels, and passes control to res:

:t res
res [a,b] [a,b,c]
res [a,c] [a,b]
resN [ma,mc] [a,b]
res [a,b] [nna,nnb,nnc]

abst is functorial, res (restrict atoms) and resN (restrict atoms from names) are monadic:

singleton <$> abst ma (ma,mb)
singleton <$> res [a]  (ma,mb)
resN [ma] (ma, mb) >>= resN [mb]
abst ma (ma, mb) >>= abst mb  -- type error; no Monad instance

<interactive>:1:1: error:
    • No instance for (Monad (KAbs (KName Tom ()))) arising from a use of ‘>>=’
    • In the expression: abst ma (ma, mb) >>= abst mb
      In an equation for ‘it’: it = abst ma (ma, mb) >>= abst mb

Equality on Abs is abstractive. Equality on Nom is generative.

abst ma a == abst mb b -- true, because both bound identifiers mapped to a single fresh atom
res [a] a == res [b] b   -- false, because two distinct scopes unpacked

If you want to study equality of data-in-local-scope, you need a notion of unification up to permutation. Fortunately, Nominal has one of them:

unifiablePerm (res [a] a) (res [b] b)
unifyPerm a a
unifyPerm a b
unifyPerm [a,b] [b,a]
unifyPerm [a,a] [a,a]
unifyPerm [a,b] [a,a]
---unifyPerm (res [a] [a,b]) (res [b] [b,a])
unifyPerm (abst ma [a,b]) (abst mb [b,a])

For efficiency, the unifiability machine only works when it will return at most one unifier. This means it is not programmed to work on sets (which could generate factorial many unifiers). There is nothing mathematically wrong with this; we just haven't implemented the machinery for it:

unifyPerm (S.fromList [a,b]) (S.fromList [b,a])  -- type error.  no unifiability instance for set due to state space explosion

<interactive>:1:12: error:
    Not in scope: ‘S.fromList’
    No module named ‘S’ is imported.
<interactive>:1:31: error:
    Not in scope: ‘S.fromList’
    No module named ‘S’ is imported.

`freshAtom` and `freshName`¶

One way to generate elements of Nom is using freshAtom and freshName. These are just like freshAtomIO and freshNameIO, but they wrap the freshly-generated atomic identifiers in a Nom monad rather than an IO monad:

:t freshAtom
:t freshName
:t freshAtoms
:t freshNames

freshAtom
freshAtoms [(),()]  -- only length of list matters here
freshName "Hello world"
freshNames ["Hello", "World"]

Here's a simple calculation. It generates two fresh atoms and calculates their equality. See unNom below to learn how to escape the final Nom binding:

freshAtom >>= \a -> freshAtom >>= \b -> return $ a == b

Lecture 3¶

View on YouTube

-- set up our environment again
:set -XDeriveAnyClass -XDeriveGeneric -XDeriveDataTypeable -XScopedTypeVariables
import Data.List
import Data.Maybe
import GHC.Generics
import Data.Generics hiding (Generic, typeOf)
import Language.Nominal.Utilities
import Data.Set as S

labelList = [(),(),()]
atomList@[a,b,c] <- freshAtomsIO labelList
nameList@[ma, mb, mc] = uncurry Name <$> zip labelList atomList
nameList'@[na, nb, nc] = uncurry Name <$> zip ["a","b","c"] atomList

The notion of support may be familiar from nominal sets. It exists in Nominal too, but its incarnation here is purely structural. A type is a KSupport instance (and so has a supp function) when that type can be traversed structurally and any atoms in it simply picked out and collected in a set.

Where a type has such structure, its support coincides with the mathematical notion. However, there are entities (like functions) for which support is mathematically well-defined but for which there is no KSupport instance.

This is entirely normal and to be expected. E.g. equality is mathematically well-defined on functions, but they have no Eq instance, and for similar reasons:

supp [a,b] -- {a,b}
supp [ma,mb] -- {a,b}
supp $ abst ma (ma,mb) -- {b}
supp $ abst ma nna -- {}
supp $ res [a,b] [b,c] -- {c}
supp $ S.fromList [a,b] -- {a,b}

Nameless types¶

Some types are nameless, meaning that once we have arrived at this type no atoms have survived. Examples of nameless types include (), Bool, Char, Int, and Integer. If a and b are nameless, so are [a] and (a,b), and so forth.

(Elements of) nameless types have empty support and trivial permutation action:

supp (42 :: Int)  -- emptyset
swp a b ["abracadabra"]  -- the "a" and "b" on the right are chars, not atoms!

(It would be nice to be able to say something like Num a => instance KSupport s a where supp a = ∅ but unfortunately the Haskell type system doesn't do backtracking, so a rule like this would swallow the typechecker's flow of control and you'd get confusing errors when it fails on proving Num a.)

Restriction¶

A restriction operation intuitively is a "please remove these atoms from my support" operation.

We have a typeclass for that, KRestrict, with a function restrict:

:t restrict

Action on nameless types is trivial:

restrict [a,b,c] (42 :: Int) 
restrict [a] True

Action on names and atoms is undefined. There's no clear way to restrict an atom in an atom or a name:

restrict [a] a -- type error, no instance
restrict [a] na -- type error, no instance

<interactive>:1:1: error:
    • No instance for (KRestrict Tom Atom) arising from a use of ‘restrict’
    • In the expression: restrict [a] a
      In an equation for ‘it’: it = restrict [a] a

Action on Nom is to add the atoms to the local scope:

[a,b,c]
restrict [a] $ res [b] [a,b,c]

Note the difference in types between res and restrict. res is a constructor.

They are related using the monadic structure of Nom by

restrict = (=<<) . res   -- on `Nom`
res = \as -> restrict as . return  -- on `Nom`

:t res  -- constructor for Nom
:t restrict  -- restriction

:t \as -> restrict as . return
:t (=<<) . res

Action on lists and sets is to delete elements:

[a,b,c]
restrict [a] [a,b]
restrict [a] [[a,b],[a,c],[b,c]]
restrict [a] $ S.fromList [a,b]
restrict [a] $ S.fromList [[a,b],[a,c],[b,c]]

This holds even if the underlying type has its own restriction action:

restrict [a] [res [a] a, res [b] a, res [c] a]  -- last two elements deleted

Action on pairing and on Maybe is pointwise --- meaning that the restriction action is passed through to the underlying types:

[a,b,c]
restrict [a] . Just $ res [b] [a,b,c]
restrict [a] . Just $ res [a] [a,b,c]
restrict [a] (res [a] [a,b,c], [a,b,c]) -- instance missing in nom-0.1.0.2; have updated for next version

<interactive>:1:1: error:
    • No instance for (KRestrict Tom (KNom Tom [Atom], [Atom])) arising from a use of ‘restrict’
    • In the expression: restrict [a] (res [a] [a, b, c], [a, b, c])
      In an equation for ‘it’: it = restrict [a] (res [a] [a, b, ....], [a, b, c])

Action on abstractions is capture-avoiding: (todo -mjg)

restrict [a] $ abst ma (res [b] [a,b,c]) -- todo -mjg
restrict [a] $ abst mc (res [b] [a,b,c]) -- todo -mjg

<interactive>:1:1: error:
    • No instance for (KRestrict Tom (KAbs (KName Tom ()) (KNom Tom [Atom]))) arising from a use of ‘restrict’
    • In the expression: restrict [a]
      In the expression: restrict [a] $ abst ma (res [b] [a, b, c])
      In an equation for ‘it’: it = restrict [a] $ abst ma (res [b] [a, b, c])

`unNom` and `newA`¶

Let's look at the types first:

:t unNom
:t newA

`unNom`¶

All unNom does is to map the locally scoped names in the KNom binding down into a using its KRestrict. That is, we transform Nom-bindings in KNom s a into restrict-bindings in a.

This is more powerful than you might expect because typical result types, such as Bool or Int, have a trivial restriction action given by throwing away any atoms in local scope (since truth-values and integers cannot contain names). Thus, unNom has a dual character:

as a way to convert a KNom binding into a KRestrict binding, and
as a way to escape a nameful computation and return a (nameless) result.

unNom is a flexible operator that unifies several distinct behaviours into a single principle.

--- This trivial computation generates two atoms and checks they are equal (they are not).
unNom (res [a,b] (a == b))    
-- The interest here is that once we calculate `False :: Bool`, we can throw away the `a` and `b` using the 
-- native `restrict` instance on `Bool`.

-- This trivial computation passes the `Nom`-restricted atom `a` down to the native restriction action on lists.
-- The effect in this instance is to apply sets subtraction.  This is another very common case.
unNom (res [a] [a,b,c])

-- In this case, the outermost `Nom`-binding gets passed to and merged with the inermost one.
-- The effect in this instance is a monad `join` action.
unNom (res [a] $ res [b] [a,b,c])

`newA`¶

This inputs a function on atoms, and applies it to a fresh atom. It can be derived from unNom as follows:

newA = \f -> unNom $ freshKAtom >>= f

:t newA
:t \f -> unNom $ freshKAtom >>= f

-- Generate a fresh atom, put it in a singleton list, and calculate the length of the list
newA (\(d :: Atom) -> length [d])
-- Generate a fresh atom and calculate whether it's an element of a set
newA $ \(d :: Atom) -> d `S.member` supp [a,b,c,d]
newA $ \(d :: Atom) -> d `S.member` supp (res [d] [a,b,c,d])

-- Generate a fresh name and return it wrapped in a `Nom` binding
newA $ \(d :: Atom) -> return d :: Nom Atom

new is just newA but for names. It inputs a function on names, and a label, and applies the function to a name with that label and a fresh atomic identifier.

:t new

-- This trivial computation generates a fresh name labelled "Hello world", and immediately calculates its label.
new "Hello World" $ (nameLabel :: Name s -> s) 
-- We need the type annotation on `nameLabel` for technical reasons, to choose a specific type (`Tom`) for the atomic ID of the name.

Binder¶

This is a typeclass for generalised binders. Both Nom and Abs are instances.

:t (@>)  -- binder constructor. 
:t (@@) -- binder destructor

Your best bet to understand this key construct may be to read the source code. Here is a very brief illustration of how the instances work. There is no computational content in these examples; they just illustrate how the result is guided by the types:

([a] @> ma) :: Nom (Name ())  -- a `Nom` binding made by invoking `@>` at a `Nom` type
(ma @> ma) :: KAbs (Name ()) (Name ())  -- an `Abs` binding made by invoking `@>` at an `Abs` type

What makes Binder particularly useful is that it comes with three destructors. In practice, these get used all the time:

:t (@@) -- exit a binder to a `Nom`
:t (@@!) -- exit a binder, releasing fresh atoms as required
:t (@@.) -- exit a binder to a type with `KRestrict`; any locally scoped atoms get merged into `a` using its `restrict` instance

Here are three forms illustrating the differences:

(res [a] [a,b]) @@  \_l x -> x -- get a `Nom` monad with `a` bound
(res [a] [a,b]) @@! \_l x -> x  -- fresh atom is generated for the locally-scoped `a`, and released
(res [a] [a,b]) @@. \_l x -> x -- restrict `a` in a list of atoms just deletes that atom

We are free to use l as well as x, if we like. This trivial computation just forms a tuple:

(res [a] [a,b]) @@  \l x -> (l,x) 
(res [a] [a,b]) @@! \l x -> (l,x) 
(res [a] [a,b]) @@. \l x -> (l,x) -- restrict `a` in a list of atoms just deletes that atom

<interactive>:1:1: error:
    • No instance for (KRestrict Tom ([KAtom Tom], [Atom])) arising from a use of ‘@@.’
    • In the expression: (res [a] [a, b]) @@. \ l x -> (l, x)
      In an equation for ‘it’: it = (res [a] [a, b]) @@. \ l x -> (l, x)

Here are more examples, this time acting on abstraction-the-binder:

abst ma ma @@! const Just
abst ma ma @@  const Just
-- abst ma ma @@. const Just -- type error
abst ma ma @@! \_ x -> [x]
abst ma ma @@  \_ x -> [x]
abst ma ma @@. \_ x -> [x]

Easter eggs¶

conc has a few little surprise instances:

[a,b,c]
res [a] [a,b] `conc` ()   -- `conc` () acts like `unNom`
-- check out @`conc` Proxy@
res [a] [a,b] `conc` [a]  -- `conc` at a list of atoms tries to concrete at these atoms
res [a] [a,b] `conc` [c]
res [a,b] [a,b] `conc` [b,a]

Notes on style¶

As a matter of style, I suggest:

Work monadically with atoms, where this is possible and does not contort the code.
Postpone generation of concrete atomic identifiers to the end, again where possible.
Don't gratuitously access the local context of atoms; let the monad carry it around, instead.

-- This is bad because we directly inspect and count the atoms in the local name-context.
badCountBinding :: Swappable a => Nom a -> Int
badCountBinding x' = x' @@! \atms _ -> length atms

-- This is a good way to implement a `KRestrict` instance for `Nom`.  Local context is managed monadically.
goodRestrict :: Swappable a => [Atom] -> Nom a -> Nom a
goodRestrict atms x' = x' >>= \x -> res atms x
-- This is a bad one; note how we generate fresh atoms using `@@!`, then restrict them.
badRestrict :: Swappable a => [Atom] -> Nom a -> Nom a
badRestrict atms' a' = a' @@! \atms a -> res (atms' ++ atms) a

-- This is a good way to define the `Eq` instance for `Nom`.  Local context is managed monadically and
-- destroyed only at computations' end, when we have a `Bool`:
goodEq :: Eq a => Nom a -> Nom a -> Bool
a1' `goodEq` a2' = unNom $ a1' >>= \a1 -> a2' >>= \a2 -> return $ a1 == a2
-- This is a bad way to do it.  Local context is destroyed in two stages (which is bad); first at `Nom a -> Bool` (also bad) and then at `Bool` (OK)
badEq :: (Swappable a, Eq a) => Nom a -> Nom a -> Bool
a1' `badEq` a2' = a1' @@! \_ a1 -> a2' @@! \_ a2 -> a1 == a2

Lecture 1¶

Setting up the environment¶

Imports¶

Some switches¶

Atoms¶

(Atom-)swapping¶

Many types of atom¶

Names¶

Name equality and ordering¶

Names with labels that mention atoms / names¶

Abstractions¶

Equality of abstractions¶

Abstraction is capturing¶

A little more on equality of abstractions¶

Concretion¶

Summary¶

Lecture 2¶

Basic setup¶

Two canonical programs¶

An inductive datatype with binding¶

The Nom monad¶

The Nom type-former¶

freshAtom and freshName¶

Lecture 3¶

Nameless types¶

Restriction¶

unNom and newA¶

unNom¶

newA¶

Binder¶

Easter eggs¶

Notes on style¶

The `Nom` monad¶

The `Nom` type-former¶

`freshAtom` and `freshName`¶

`unNom` and `newA`¶

`unNom`¶

`newA`¶