Simon Peyton-Jones wrote:
| Another workaround is to pass in several 'stringer' functions,
| one to use at each type. Not beautiful, but it works.
This reminds me of a workaround for a similar problem I encountered. In
Lava, we have several different monads that can interpret the same circuit
description. We could for example have the following monads, with their
own run functions:
type Sim a = ...
runSim :: Sim a -> ...
type Prove a = ...
runProve :: Prove a -> ...
type Vhdl a = ...
runVhdl :: Vhdl a -> ...
If I write a circuit description, I will leave the actual underlying monad
type polymorphic (only restricted by some classes):
myCircuit :: Circuit m => m Bit
myCircuit = ...
If I now want to write a function that first proves myCircuit correct, and
then generates Vhdl:
generateMyCircuit = ... runProve myCircuit ... runVhdl myCircuit ...
This works fine. But not if I want to abstract from this, and write a
general function that does this for any circuit:
proveNgenerate circ = ... runProve circ ... runVhdl circ ...
^^^^ ^^^^
different types!!!
This does not work, because "circ" is not polymorphic. A solution (which
is the one Simon proposes) is to give two parameters to proveNgenerate,
which will in practice always be the same:
proveNgenerate circ circ' = ... runProve circ ... runVhdl circ' ...
And then, when you use proveNgenerate:
proveNgenerate myCircuit myCircuit
This is ugly!!
Another solution, is to introduce a new type, called Both, which lifts two
monads/circuits/etc. into one:
data Both m n a = Pair (m a) (n a)
And we can make instance declarations:
instance (Monad m, Monad n) => Monad (Both m n) where ...
instance (Circuit m, Circuit n) => Circuit (Both m n) where ...
...
Further, we make a function called "unboth":
unboth :: Both m n a -> (m a, n a)
unboth (Pair x y) = (x, y)
Now we can implement proveNgenerate:
proveNgenerate circ = ... runProve circ1 ... runVhdl circ2 ...
where
(circ1, circ2) = unboth circ
Quite nice I think, because the use of the function now is:
proveNgenerate myCircuit
Look at the type of proveNgenerate:
proveNgenerate :: Both Prove Vhdl a -> ...
In my "Both" library in Lava, I even added the following:
type Triple m n p = Both m (Both n p)
untriple m = (x, y, z)
where
(x, m') = unboth m
(y, z) = unboth m'
type Quadruple m n p q = ...
...
Which makes things a little bit more general to use.
Regards,
Koen.
--
Koen Claessen,
[EMAIL PROTECTED],
http://www.cs.chalmers.se/~koen,
Chalmers University of Technology.
