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

[Ryan Ingram]

On Wed, Nov 19, 2008 at 1:04 AM, Wouter Swierstra <wss at cs.nott.ac.uk> 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