Sat Oct 15 10:15:49 EDT 2011

Getting unstuck with recursive type class definitions.

It really shouldn't be such a big deal.  This is just pattern
matching, but done on types instead of data structures.

What do I want to do?

I have a type like this:

  (i1 :& i2 :& ...) -> m (o1 :& o2 :& ...)

And I want to map this to a type like this:

  ([i], m [o])

Let's do it in 2 steps: one for the input, and one for the output.

I have something like

       (Term t :& ...)


And I need to create a value of Term t such that it can be passed to
the function.

Amazing.. I got it to work with fundeps and undecidable instances:

class TermApp m f | f -> m where
  termApp :: [VarName] -> f -> ([STerm], m [STerm])

instance (MakeVar t, TermApp m f) => TermApp m ((Term t) -> f) where
  termApp (n:ns) f = ((i:is), mos) where
    term :: Term t = makeVar n
    (is, mos) = termApp ns (f term)
    Term i = term

instance (Monad m) => TermApp m (m (Term t)) where
  termApp _ mt = ([], ms) where
    ms = do
      (Term s) <- mt
      return [s]

Then with a bit of effort the output tuple recursion also works.  I
had to use liftM snd and liftM fst to make it type correctly without
annotations that I did not know how to write.

instance (Monad m, TermApp m (m os))
         => TermApp m (m (Term t, os)) where
  termApp _ m_t_ts = ([], mss) where
    mss = do
      (Term s) <- liftM fst m_t_ts
      ss <- snd $ termApp [] (liftM snd m_t_ts)
      return (s : ss)

The rest should be straightforward.  Inputs can already be printed:

varnames = map (\n -> "in" ++ (show n)) [0..]

compile f = (is, os) where
  (is, mos) = termApp varnames f
  os = ()
For outputs the monad needs to be executed.

The trick was to change the Asm type such that it uses STerm in the
result as opposed to Term.  This allows the Asm constructore to be
used as a finial continuation of the state-continuation monad,
grabbing state (environment) and the argument passed to the
coninuation (list of result terms).

data Asm = Asm Env [STerm]

asm :: SC Asm Env [STerm] -> Asm
asm (SC c) = c env0 Asm