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

[Henning Thielemann]

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.