<div dir="ltr"><div>I am trying to use a data types a la carte approach to define a free monad for templating purposes. I am using Edward Kmett's free package, and a module implementing data types a la carte's injections, modelled on the IOSpec Types module. I have written a few combinators, but I am stuck. My program keeps diverging, and I don't see why.</div>
<div><br></div><div>Consider:</div><div><br></div><div><font face="courier new, monospace">math :: Math :<: f => MathExpr a -> Free f ()</font></div><div><font face="courier new, monospace">blank :: f :<: (Textual :+: Math) </font></div>
<div><font face="courier new, monospace"> => Free f () </font></div><div><font face="courier new, monospace"> -> Free (Blank k f) ()</font></div><div><font face="courier new, monospace">equals :: Free (Math :+: (Blank L Math)) ()</font></div>
<div><font face="courier new, monospace"> -> Free (Math :+: (Blank R Math)) ()</font></div><div><font face="courier new, monospace"> -> Free Equation () </font></div><div><br></div><div>The intention is that a blank takes in a properly typed abstract syntax tree and tags it with "blank k", so that the parsers/renderers do the "right thing" (when I get around to implementing them) The composition (blank . math) has the type:</div>
<div><br></div><div><font face="courier new, monospace">blank . math :: ( f :<: (Textual :+: Math)</font></div><div><font face="courier new, monospace"> , Math :<: f</font></div><div><font face="courier new, monospace"> ) => MathExpr a -> Free (Blank k f) ()</font></div>
<div><font face="courier new, monospace"><br></font></div><div>Notice that f must be simultaneously less than or equal to the join of Textual and Math, and greater than or equal to Math. So the only possibility for f is Math. (I realize the compiler can't infer this without more work on my part)</div>
<div><br></div><div>The problem happens when I try to evaluate (using scoped type signatures to get around my comment above):</div><div><br></div><div><font face="courier new, monospace">test :: Free Equation ()</font></div>
<div><font face="courier new, monospace">test = (hoistFree (inj :: Blank 'L Math a -> (Math :+: Blank 'L Math) a)</font></div><div><font face="courier new, monospace"> . blank</font></div><div><font face="courier new, monospace"> . (math :: MathExpr x -> Free Math ())</font></div>
<div><font face="courier new, monospace"> $ "hi"</font></div><div><font face="courier new, monospace"> )</font></div><div><font face="courier new, monospace"> `equals` (math $ "world")</font></div>
<div><br></div><div>which apparently loops, pegging my CPU at 100%. The computation prints its result as:</div><div><br></div><div><font face="courier new, monospace">Free (Equation (Free (DirectSum {unDirectSum = Right</font></div>
<div><br></div><div>at which point the value is truncated and GHCi quits. So it apparently gets as far as figuring out that the first argument to equals is in the latter part of the direct sum, but it doesn't seem t be able to compute blank.</div>
<div><br></div><div>Relatively minimal source is available at:</div><div> monad: <a href="http://lpaste.net/93471">http://lpaste.net/93471</a></div><div> data types a la carte: <a href="http://lpaste.net/93472">http://lpaste.net/93472</a></div>
<div><br></div><div>All my functions are total and I don't see a bottom here, but I was never any good at fixed point combinators. Any ideas?</div></div>