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.

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