| Copyright | (c) Murdoch J. Gabbay 2020 |
|---|---|
| License | GPL-3 |
| Maintainer | murdoch.gabbay@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Nominal.Examples.Style
Description
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 Source #
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 Source #
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 Source #
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 Source #
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 Source #
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