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