Re: [Haskell-cafe] Monadic bind with associated types + PHOAS?
Hi Ryan, On 19 Nov 2008, at 04:39, Ryan Ingram wrote: 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. There's a perfectly legitimate way to incorporate free variables in your expression data type, without sacrificing type safety. You just need to parametrise your expression type by the context: data Exp g t where App :: Exp g (a - b) - Exp g a - Exp g b Lam :: (Exp g a - Exp g b) - Exp g (a - b) Var :: Var g a - Exp g a data Var g a where Top :: Var (a,g) a Pop :: Var a g - Var a (b, g) I wouldn't call this unsafe (or at least no more unsafe than HOAS). Note that in particular Exp Empty a correspond to closed terms, where Empty denotes the empty type. Secondly, you can always turn a HOAS Exp into non-HOAS expression. Essentially, you map applications to applications, etc. The only interesting case deal with lambda abstractions - there you need to generate a fresh variable name, apply the function to the fresh variable, and continue traversing the resulting expression. You might be interested in a tutorial Andres Loeh, Conor McBride, and I wrote about implementing a dependently typed lambda calculus: http://www.cs.nott.ac.uk/~wss/Publications/Tutorial.pdf The quote function in Figure 7 gives the code. Does anyone think this is a direction worth pursuing? I'm not convinced yet. The problem is that there's no best way to handle binding. HOAS is great for some things (you don't have to write substitution), but annoying for others (optimisations or showing code). From your message, I couldn't understand why you want to use monads/do-notation to handle binding. Care to elaborate? All the best, Wouter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic bind with associated types + PHOAS?
On Wed, Nov 19, 2008 at 1:04 AM, Wouter Swierstra [EMAIL PROTECTED] wrote: I'm not convinced yet. The problem is that there's no best way to handle binding. HOAS is great for some things (you don't have to write substitution), but annoying for others (optimisations or showing code). PHOAS solves showing code quite nicely, in my opinion. I haven't tried to write a real optimizer using it yet. It's probably better to convert to a better intermediate representation and then back when you're done. The nice thing about HOAS, in my opinion, is not that it's a good representation of a language; rather it is that the syntax for *writing* it in your code is much nicer than the explicit variable references needed otherwise, because you have lifted part of the syntax into the host language. From your message, I couldn't understand why you want to use monads/do-notation to handle binding. Care to elaborate? Sure; I guess I should explain the motivation a bit. I really like the syntax for do-notation. And I really like how great Haskell is as writing embedded languages, a lot of which comes from the programmable semicolon that monadic bind gives you. But there's no equivalent programmable variable bind, or programmable function application; both are generalizations of do-notation that would be useful for embedded languages. So I have been thinking about what makes variable binding special. What is it that we get from a variable bind? How can we create a structure that allows one to program control the results of the binding values to variables? This has many uses in embedded languages: 1) We can observe sharing; solving this in DSLs in Haskell usually leads to really ugly syntax. 2) We can write interpretation functions that can examine all possible execution paths; this is basically introspection on functions. This lets us do whole program optimization or other transformations on the result of the monadic code. (2) is usually solved via arrows, although arr makes a true solution quite difficult. I don't know of an elegant solution for (1) at all. Do you have any ideas along these lines? -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monadic bind with associated types + PHOAS?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monadic bind with associated types + PHOAS?
Ryan Ingram wrote: 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: If one uses a tagless final representation, one benefits from the conveniences of the higher-order abstract syntax and yet gains the ability to show terms, count the number of constructors and even partially evaluate them (i.e., optimize). For the example, please see http://okmij.org/ftp/tagless-final/Incope.hs (in particular, see Semantics2 for the partial evaluator that does not use GADT). We can easily add an interpreter that does a CPS transform, thus letting us embed a CBV object language in a Haskell without any use of monad or the change of syntax of the object language. We can easily extend the language to add state (as we have done in the OCaml part of the project). http://okmij.org/ftp/tagless-final/README.txt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
