[Haskell-cafe] Using type classes for polymorphism of data constructors

[Thomas Sutton]

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