[Haskell-cafe] Non-termination using Free Monads and Data Types a la Carte

[Alexander Solla]

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.

Consider:

math :: Math :<: f => MathExpr a -> Free f ()
blank :: f :<: (Textual :+: Math)
      => Free f ()
      -> Free (Blank k f) ()
equals :: Free (Math :+: (Blank L Math)) ()
       -> Free (Math :+: (Blank R Math)) ()
       -> Free Equation ()

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:

blank . math :: ( f :<: (Textual :+: Math)
                , Math :<: f
                ) => MathExpr a -> Free (Blank k f) ()

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)

The problem happens when I try to evaluate (using scoped type signatures to
get around my comment above):

test :: Free Equation ()
test = (hoistFree (inj :: Blank 'L Math a -> (Math :+: Blank 'L Math) a)
     . blank
     . (math :: MathExpr x -> Free Math ())
     $ "hi"
     )
     `equals` (math $ "world")

which apparently loops, pegging my CPU at 100%. The computation prints its
result as:

Free (Equation (Free (DirectSum {unDirectSum = Right

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.

Relatively minimal source is available at:
  monad: http://lpaste.net/93471
  data types a la carte: http://lpaste.net/93472

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130927/16040e82/attachment.htm>