Expand literate Haskell semantics

[Gabriella439]

… to include:

• Binary encoding
• α-normalization
• β-normalization
• Equivalence checking

Related to: #959

Note that this does not include binary decoding. I was mainly
focused on completing all the dependencies for equivalence checking,
and binary decoding was not necessary for that, yet.

[Nadrieril]

I didn't read through all of it but it looks very clean. Were you able to read this at all? It seems we don't have a parser yet.

[Gabriella439]

@Nadrieril: I haven't actually tested that the code works, yet. I can begin work on the parser for the next step.

The main reason I focused on this part first is that I wanted to flush out some non-trivial code (e.g. the β-normalization logic) to make sure that people are okay with the coding style before I proceed further.

[Nadrieril]

This pile of Applications is a bit hard to follow. Could we do

let (@) = Application
in  betaNormalize (g @ (NaturalFold @ (NaturalLiteral (m - 1)) @ _B @ g @ b))

or something like that?

[Nadrieril]

Thanks for the impressive work! Looks good to me. Normalization of builtins can be hard to follow, but I'm not sure we can do much better anyways

[Gabriella439]

@Nadrieril: I took a stab at your suggestion by using GHC's support for pattern synonyms, like this:

{-| Convenient synonym for `Application` so that β-normalization code is easier
    to read
-}
pattern (:@) :: Expression -> Expression -> Expression
pattern f :@ x = Application f x

infixl :@

… which does make the code much clearer, but as I was applying the change the type-checking began to slow down significantly until I hit this warning:

BetaNormalization.lhs:(103,1)-(2577,68): error: [-Werror]
    Pattern match checker exceeded (2000000) iterations in
    an equation for ‘betaNormalize’. (Use -fmax-pmcheck-iterations=n
    to set the maximum number of iterations to n)
    |
103 | betaNormalize (Constant c) = Constant c
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

… so I think I'll avoid using the pattern synonym for now until we begin using GHC 8.10 to build the literate Haskell semantics, which appears to have fixed the performance issue (See: https://gitlab.haskell.org/ghc/ghc/-/issues/11822)