Thomas Sutton wrote:
Main> :t (Impl (Prop "p") (Poss (Prop "p"))) -- "p -> <>p" Impl (Prop "p") (Poss (Prop "p")) :: PC
So the type says that this is a formula in the predicate calculus? (Even though you combine two formulae of modal logics.) Are you happy with that? Just wondering? Also, are you fine to take the conjunction of a PC and Modal formula, which is admitted by your types? (If not, you may want to use phantom types.) So it seems like the type doesn't carry a lot of information. Then we could also use different types. In particular, we could do without existentials. The types we get will (additionally) record the arity of the outermost constructor. (In your model, the type records the kind of logic of the outermost constructor.) class (Show f) => Formula f data PC0 = Prop String data Formula x => PC1 x = Neg x data (Formula x, Formula y) => PC2 x y = Conj x y | Disj x y | Impl x y instance Formula PC0 instance Formula x => Formula (PC1 x) instance (Formula x, Formula y) => Formula (PC2 x y) instance Show PC0 where show (Prop s) = s instance Formula x => Show (PC1 x) where show (Neg x) = "~" ++ show x instance (Formula x, Formula y) => Show (PC2 x y) where show (Conj a b) = (show a) ++ " /\\ " ++ (show b) show (Disj a b) = (show a) ++ " \\/ " ++ (show b) show (Impl a b) = (show a) ++ " -> " ++ (show b) data Formula x => Modal1 x = Poss x | Necc x instance Formula x => Formula (Modal1 x) instance Formula x => Show (Modal1 x) where show (Poss a) = "<>" ++ (show a) show (Necc a) = "[]" ++ (show a) main = do print (Prop "p") print (Poss (Prop "p")) print (Impl (Prop "p") (Poss (Prop "p"))) (Again, just wondering whether this might be an Ok solution.) Thomas Sutton wrote:
In Java (C#, Python, etc) I'd do this ...
Please post your Java code. I might want to add it to the OOHaskell demo suite. Ralf
-----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] On Behalf Of Thomas Sutton Sent: Thursday, June 23, 2005 3:27 AM To: haskell-cafe@haskell.org Subject: [Haskell-cafe] Re: Using type classes for polymorphism of dataconstructors
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe