Hi all,
I've just started working on a theorem prover (labelled tableaux in
case anyone cares) in Haskell. In preparation, I've been attempting
to define some data types to represent logical formulae. As one of
the requirements of my project is generality (i.e. it must be easily
extendible to support additional logics), I've been attempting to
build these data types modularly.
The end goal in all of this is that the user (perhaps a logician
rather than a computer scientist) will describe the calculus they
wish to use in a simple DSL. This DSL will then be translated into
Haskell and linked against some infrastructure implementing general
tableaux bits and pieces. These logic implementations ought to be
composable such that we can define modal logic to be propositional
calculus with the addition of [] and <>.
In Java (C#, Python, etc) I'd do this by writing an interface Formula
and have a bunch of abstract classes (PropositionalFormula,
ModalFormula, PredicateFormula, etc) implement this interface, then
extend them into the connective classes Conjunction, Disjunction,
etc. The constructors for these connective classes would take a
number of Formula values (as appropriate for their arity).
I've tried to implement this sort of polymorphism in Haskell using a
type class, but I have not been able to get it to work and have begun
to work on implementing this "composition" of logics in the DSL
compiler, rather than the generated Haskell code. As solutions go,
this is far from optimal.
Can anyone set me on the right path to getting this type of
polymorphism working in Haskell? Ought I be looking at dependant types?
Thanks in advance,
Thomas Sutton
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
