Hi,<br><br>I have read the previous thread about Monads with great interest.
The abstration ideas contained in Wadler&#39;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.<br>
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.<br>
<br>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.<br><br>Some of the parts that need to be decoupled are:<br>-
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.<br>
- 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 in a smarter way).<br>- Post processors that are applied to all successfull resolvents and perform manipulation on the Refinements states, like adding new clauses (called also resolvents), forward subsumption, deletion of tautologies, etc.)<br>
<br>As an example for abstraction in the Refinement state, we have in the c++ version an interactive refinement that gets as argument another refinement and deals with obtaining commands from the user:<br>- do x steps in automatic mode i.e. execute the inner refinement for x steps.<br>
- tries to unifies two clauses on all positions, etc.<br><br>Also the user interface module should be deoupled as it can be a simple command like or a GUI.<br><br>My naive approach was to create a class for each abstract part of the prover and the different instances will implement the specific implementations. <br>
<br>My main question is if it is feasible to achieve in Haskell and even if it is Feasible, if such decoupling should be attempted in Haskell in the first place or that other languages are more suitable. I guess my main question is if projects prgrammed by several programmers with a complete decoupling between them can be done in Haskell.<br>
<br>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++).<br>

<br>
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)?<br>

<br>to give an example for the main function (many parts are missing):<br><br>class Refinement a where<br>getClauses :: Maybe (Clause, Clause)<br><br>loop&nbsp; timeout refinement = <br>&nbsp; let<br>&nbsp;&nbsp;&nbsp; clauses = getClauses refinement<br>
&nbsp;&nbsp;&nbsp; timedout = isTimeout t<br>&nbsp; in<br>&nbsp;&nbsp;&nbsp; if timedout then Timedout t else<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; case clauses of<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Nothing -&gt; Exahusted<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Just (c1, c2) -&gt; let<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; resolvents = unifyOnAllLiterals c1 c2 -- list of all resolvents<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; in<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; if emptyClauseIsContained resolvents <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; then Success unifier -- unifer is the global unifier<br><br><br>