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.

In [1]:

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

In [2]:

```
import Language.Nominal
```

In [3]:

```
:set -XDeriveAnyClass -XDeriveGeneric -XDeriveDataTypeable
```

Ask `ghci`

to print types of expressions after each evaluation:

In [4]:

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

Let's give ourselves three labels:

In [5]:

```
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
```

In [6]:

```
: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`

):

In [7]:

```
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`

:

In [8]:

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

We have a **swapping action** `swp`

.

This acts on base datatypes with atoms ...

In [9]:

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

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

In [10]:

```
swp a b ("Hello world",42)
```

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

:

In [11]:

```
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`

:

In [12]:

```
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:

In [13]:

```
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):

In [14]:

```
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
```

`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):

In [15]:

```
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
```

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`

:

In [16]:

```
: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?

In [17]:

```
-- 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
```

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.

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:

In [18]:

```
[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:

In [19]:

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

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:

In [20]:

```
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)`

In [21]:

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

Let's recall our environment:

In [22]:

```
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$):

In [23]:

```
: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`

:

In [24]:

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

`abst na na`

looks like $\lambda a.a$ and `abst nb nb`

looks like $\lambda b. b$. Are these abstractions equal?

In [25]:

```
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:

In [26]:

```
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 `abst`

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

In [27]:

```
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`

:

In [28]:

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

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

In [29]:

```
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
```

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

In [30]:

```
: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:

In [31]:

```
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.

In [32]:

```
(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.

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.

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.)

In [33]:

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

In [34]:

```
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'
```

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.

In [35]:

```
-- 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)
```

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

In [36]:

```
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:

In [37]:

```
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:

In [38]:

```
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:

In [39]:

```
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:

In [40]:

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

In [41]:

```
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:

In [42]:

```
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
```

`Nom`

monad¶Let's recall our environment again:

In [43]:

```
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`

:

In [44]:

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

`abst`

is also functorial:

In [45]:

```
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`

:

`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`

:

In [46]:

```
: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:

In [47]:

```
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
```

Equality on `Abs`

is **abstractive**. Equality on `Nom`

is **generative**.

In [48]:

```
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:

In [49]:

```
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:

In [50]:

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

`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:

In [51]:

```
: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:

In [52]:

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

In [53]:

```
-- 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:

In [54]:

```
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}
```

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:

In [55]:

```
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.)*

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`

:

In [56]:

```
:t restrict
```

**Action on nameless types** is trivial:

In [57]:

```
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:

In [58]:

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

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

In [59]:

```
[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`
```

In [60]:

```
:t res -- constructor for Nom
:t restrict -- restriction
:t \as -> restrict as . return
:t (=<<) . res
```

**Action on lists and sets** is to delete elements:

In [61]:

```
[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:

In [62]:

```
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:

In [63]:

```
[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
```

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

In [64]:

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

`unNom`

and `newA`

¶Let's look at the types first:

In [65]:

```
: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.

In [66]:

```
--- 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`

In [67]:

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

In [68]:

```
-- 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.

In [69]:

```
: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.
```

This is a typeclass for generalised binders. Both `Nom`

and `Abs`

are instances.

In [70]:

```
: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:

In [71]:

```
([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*:

In [72]:

```
: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:

In [73]:

```
(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:

In [74]:

```
(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
```

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

In [75]:

```
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]
```

`conc`

has a few little surprise instances:

In [76]:

```
[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]
```

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.

In [77]:

```
-- 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
```