Language.Nominal.Examples.Style

Commented examples of coding style. (Or: ways to abuse this code.)

Documentation

It's tempting to try to provide static guarantees of good behaviour with respect to name-handling. However, this is expensive and may be impossible: sometimes what makes code good or bad depends on how the output is used.

For example: a substitution of a term for a bound name may involve generating a fresh identifier for that name. This is reasonable, because we expect the choice of name to be destroyed by the substitution. We can rewrite the code to avoid this name-generation, at some expense, and arguably this stilts the coding style, but either way it is not clear how a type system can provide a comprehensive answer.

Here, we give examples of programs (that may even still work, but) are arguably ugly. So: this file is devoted to some programs that you might think twice about writing.

bad_countBinding :: Swappable a => Nom a -> Int

You probably shouldn't count the atoms bound in a KNom.

bad_countBinding :: Swappable a => Nom a -> Int
bad_countBinding x' = x' @@! \atms _ -> length atms

bad_countOrder :: Swappable a => Nom a -> Bool

You probably shouldn't look at the order of the atoms bound in a KNom.

bad_countOrder :: Swappable a => Nom a -> Bool
bad_countOrder x' = x' @@! \atms _ -> isSorted atms

badRestrict :: Swappable a => [Atom] -> Nom a -> Nom a

It's OK to create fresh IDs for bound atoms, but doing so unnecessarily is deprecated.

For example, here is code for a restrict instance of Nom (code simplified for clarity):

restrict :: Swappable a => [Atom] -> Nom a -> Nom a
restrict atms x' = x' >>= \x -> res atms x

We can simplify it down to this:

restrict = (=<<) . res 

The code for badRestrict below does the same thing, but unnecessarily unpacks the local binding, generates fresh IDs for its atoms, and then rebinds.

badRestrict :: Swappable a => [Atom] -> Nom a -> Nom a
badRestrict atms' a' = a' @@! \atms a -> res (atms' ++ atms) a

okRestrict :: Swappable a => [Atom] -> Nom a -> Nom a

Contrast badRestrict with the similar okRestrict. What separates them is the use of '(@!)' instead of '(.)' (respectively). The latter '(@.)' avoids an intermediate generation of explicit fresh IDs for the bound atoms, and so is better.

In fact okRestrict is equivalent to the actual restrict instance; it's just expressed using higher-level tools.

okRestrict :: Swappable a => [Atom] -> Nom a -> Nom a
okRestrict atms a' = a' @@. \_ -> res atms

Also OK:

okRestrict' atms' = join . fmap (res atms')

badEq :: Eq a => Nom a -> Nom a -> Bool

Still on the theme of trying to be parsimonious with generating atoms here is code for an equality instance of KNom:

instance Eq a => Eq (KNom s a) where
   a1' == a2' = exit $ a1' >>= \a1 -> a2' >>= \a2 -> return $ a1 == a2

Note how we exit at Bool. Contrast with the deprecated version, in which we exit earlier than required, and furthermore, we exit twice (code simplified for clarity):

badEq :: Eq a => Nom a -> Nom a -> Bool
badEq a1' a2' = withExit a1' $ \_ a1 -> withExit a2' $ \_ a2 -> a1 == a2