[Haskell-cafe] Monadic bind with associated types + PHOAS?

[Ryan Ingram]

This is an idea that has been bouncing around in my head for a while,
having to do with embedded languages.

A few of the talks at CUFP this year mentioned using Haskell to embed
a DSL that gets compiled into the output of the program; the hydraulic
engine talk embedded the code for the real-time safety computation in
the trucks, and one of the finance talks embedded a language for
designing Excel spreadsheets.

One thing that often comes up is a desire to do a pass on the
resultant code to optimize it, but it's pretty difficult with the
standard monadic formulation because of embedded functions.  You can't
do introspection on functions in Haskell; they aren't elements of Eq
or Show.  This has caused, for example, some implementations of FRP to
switch to using arrows instead.  However, I find the arrow syntax
cumbersome and I feel it tends to obfuscate what is actually going on
in the code.

An earlier talk at ICFP mentioned using PHOAS instead of HOAS to
encode expressions.  In HOAS, a lambda expression in the target
language is represented by a function in the source language:

> data ExpE t where
>    ApE :: ExpE (a -> b) -> ExpE a -> ExpE b
>    LamE :: (ExpE a -> ExpE b) -> ExpE (a -> b)

But without a way to inspect the function inside LamE, you can't get
back to the "source code".  You end up adding special constructors for
"Primitive" or "Variable" to let you do something with the resultant
structure, which leads to the expression language containing "unsafe"
constructors which need to be hidden.

PHOAS makes a small change to make many of these things possible
without compromising safety:

> data ExpP v t where
>    VarP :: v t -> ExpP v t
>    ApP :: ExpP v (a -> b) -> ExpP v a -> ExpP v b
>    LamP :: (v a -> ExpP v b) -> ExpP v (a -> b)
>
> newtype Exp t = Exp (forall v. ExpP v t)

Now, by parametricity, if you are constructing an Exp t, the only
useful thing you can do with the variable passed to LamP is give it to
VarP.  This means the code using it is basically the same as the HOAS
code, except a couple of extra "VarP" constructors inserted, but you
gain the ability to inspect inside the lambda and extract the code it
generates!

An couple of examples, from a PHOAS test I wrote up:

1) An evaluator
> eval :: Exp t -> t
> eval (Exp e) = evalP e
>
> newtype Prim a = Prim a
> evalP :: ExpP Prim t -> t
> evalP (VarP (Prim a)) = a
> evalP (ApP e1 e2) = evalPrim e1 $ evalPrim e2
> evalP (LamP f) = evalPrim . f . VarP . Prim

2) using "show" to peek inside functions!

] -- implementation is an exercise for the reader
] -- you'll learn a lot! :)
]
] newtype Var a = Var String
] showExp :: ExpP Var a -> ShowS

ghci> let test = Exp $ Lam $ \a -> Lam $ \b -> Var a
ghci> :t test
test :: Exp (t -> t1 -> t)
ghci> print test
\x y -> x

It seems to me this exact transformation could be useful to express
"variable binding" in embedded languages!

> type family Primitive m a
> type family BoundVar m a
> class PMonad m where
>     preturn :: Primitive m a -> m a
>     pbind :: m a -> (BoundVar m a -> m b) -> m b

Now, this strictly generalizes regular monads:

> newtype Wrap m a = Wrap (m a)
> unwrap (Wrap m) = m
> type instance Primitive (Wrap m) a = a
> type instance BoundVar (Wrap m) a = a
> instance Monad m => PMonad (Wrap m) where
>     preturn x = WM (return x)
>     pbind m f = WM (unwrap m >>= unwrap . f)

So, it seems like the do-notation should work on this type, although
you lose pattern matching ([x] <- getArgs).  And you can use PHOAS
techniques to build up a structure that you can introspect and
optimize.

Does anyone think this is a direction worth pursuing?  It seems to me
like a point where the current syntax of Haskell could mesh well with
the new type-system technology that we keep getting from GHC HQ.

  -- ryan