[Haskell-beginners] Is complete decoupling and abstraction possible in Haskell?

[Tomer Libal]

Hi,

I must add that although in general Theorem provers are very performance
oriented, we are not interested in performance in our prover as it is used
mainly for testing different refinements and extensions. Therefore, we
consider haskell as well (as c++).

Also, is there a big reference project, implemented in Haskell, that
exhibits some of the OO concepts like decoupling, modulation and
abstraction? I understand functional programming has other core values like
ease of programming and easy validation of correctness but is it also
suitable for large structured projects worked on by many programmers (using
decoupling for example)?

I have read the previous thread about Monads with great interest. The
abstration ideas contained in Wadler's papers gave me hope that there is a
way to do a full decoupling and abstraction in Haskell, but I have no idea
how.
I am interested in building a completely generic resolution theorem prover
that all of its parts can be implemented separately. In fact, we already
have this prover programmed in c++ but I would be glad if I can reprogram it
in Haskell for further extensions of the different parts.

The idea of the resolution prover is to get a set of clauses in clasual
logic and to try and refute them by using resolution.

Some of the parts that need to be decoupled are:
- Refinements which are datastructures that return the pair (or more) of
clauses each time that need to be processed. They are chosen according to
some heuristic, i.e. smallest clauses, etc. Each Refinement instance should
be able to return the next pair to be processed according to its inner state
and heuristics.
- Resolvers that process two clauses and tries to unify a specific literal
in each. The abstraction here deals with each resolver processing in a
different way. Some do factorization and some modulation and each one of
this processes have several kinds that should be decoupled as well (i.e.
modulator that works by a brute force BFS or
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20090116/15ad9255/attachment.htm