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

[Thomas Sutton]

On 11/06/2005, at 11:18 PM, Thomas Sutton wrote:
> 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?

I've finally managed to find a way to get this to work using  
existentially quantified type variables and am posting it here for  
the benefit of the archives (and those novices like myself who will  
look to them in the future). My solution looks something like the  
following:

A type class over which the constructors ought to be polymorphic:

 > class (Show f) => Formula f where
 >         language :: f -> String

A type exhibiting such polymorphism:

 > data PC
 >         = Prop String
 >         | forall a.   (Formula a)            => Neg a
 >         | forall a b. (Formula a, Formula b) => Conj a b
 >         | forall a b. (Formula a, Formula b) => Disj a b
 >         | forall a b. (Formula a, Formula b) => Impl a b
 > instance Formula PC where
 >         language _ = "Propositional Calculus"
 > instance Show PC where
 >         show (Prop s)   = s
 >         show (Neg s)    = "~" ++ (show s)
 >         show (Conj a b) = (show a) ++ " /\\ " ++ (show b)
 >         show (Disj a b) = (show a) ++ " \\/ " ++ (show b)
 >         show (Impl a b) = (show a) ++ " -> " ++ (show b)

Another such type:

 > data Modal
 >         = forall a. (Formula a) => Poss a
 >         | forall b. (Formula b) => Necc b
 > instance Formula Modal where
 >         language _ = "Modal Logic"
 > instance Show Modal where
 >         show (Poss a) = "<>" ++ (show a)
 >         show (Necc a) = "[]" ++ (show a)

Some example values of those types:

Main> :t (Prop "p")                    -- "p"
Prop "p" :: PC

Main> :t (Poss (Prop "p"))                -- "<>p"
Poss (Prop "p") :: Modal

Main> :t (Impl (Prop "p") (Poss (Prop "p")))        -- "p -> <>p"
Impl (Prop "p") (Poss (Prop "p")) :: PC

I also have a sneaking suspicion I'd also be able to solve this  
problem using dependant types, but I have not investigated that  
approach.

Cheers,
Thomas Sutton