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

[Thomas Sutton]

On 13/06/2005, at 8:29 PM, Henning Thielemann wrote:
> 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  
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