Using type classes for polymorphism of data constructors
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
On Sat, 11 Jun 2005, Thomas Sutton wrote:
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 <>.
Is there a need for a custom DSL or will it be possible to express theorems in Haskell? QuickCheck can test properties which are just Haskell functions with random input, so it would be comfortable to use these properties for proving, too. There is also the proof editor Alfa. As far as know it is written in Haskell but the theorems are not expressed in Haskell.
On Sat, 11 Jun 2005, Thomas Sutton wrote:
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 <>.
Is there a need for a custom DSL or will it be possible to express theorems in Haskell? Having used HOL a bit, I'm not sure that using a general PL as the user interface to a theorem prover is such a great idea. The goal of
On 13/06/2005, at 8:29 PM, Henning Thielemann wrote: the project (an honours project) is to be able to construct [counter-] models using as wide a range of /labelled tableaux calculi/ as possible, thus the need for a DSL of some description (to specify each calculus). The theorems themselves will be expressed using the operators described for each calculus (using the DSL). It will be, in essence, a meta theorem prover.
QuickCheck can test properties which are just Haskell functions with random input, so it would be comfortable to use these properties for proving, too. There is also the proof editor Alfa. As far as know it is written in Haskell but the theorems are not expressed in Haskell. I've not looked at QuickCheck yet, though I've been meaning to get to it for quite a while; I'll have to bump it up the queue.
Cheers, 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
participants (2)
-
Henning Thielemann -
Thomas Sutton