Archive for the 'Datatypes a la carte' Category

First-order logic a la carte

What’s covered in today’s post isn’t strictly a trick for handling binding (in this case, binding is handled by HOAS, though the method doesn’t appear to be limited to using HOAS).  However, the approach that’s summaried, datatypes a la carte, is a neat trick that I’ve only recently come across.  In short, the trick can be boiled down to: “build larger datatypes from smaller datatypes by taking their coproduct”.

The following article demonstrates one benefit of doing this: building a datatype representing first-order formulae, we can then define a series of transformation steps (at each stage eliminating a logical connective) which transforms an arbitrary FOL formula into implicative normal form.  What’s really unique about this approach is that every step of the transformation is guaranteed, by the type system, to eliminate the corresponding connective from the input formula.

By Kenneth Knowles, in the Monad.Reader Issue 11, available from the Monad.Reader archive:

Classical first-order logic has the pleasant property that a formula can be reduced to an elegant implicative normal form through a series of syntactic simplifications. Using these transformations as a vehicle, this article demonstrates how to use Haskell’s type system, specifically a variation on Swierstra’s “Data Types a la Carte” method, to enforce the structural correctness property that these constructors are, in fact, eliminated by each stage of the transformation.

Advertisements