User defined binders?
Florian Lorenzen
is there any functional language in which it is possible to define
custom binders -- apart from the Lisp family where its possible via macros?
What I have in mind are user defined (list) comprehensions, e.g.:
[2*x | x <- xs]
in which the variable x is bound in the 2*x part, or monadic notation like
x <- f; g x
meaning f >>= (\x -> g x) in Haskell notation.
Searching the web, I could not find anything.
Hints are very much appreciated, best regards,
Florian
Dan Doel
Coq allows one to write "notation" that will desugar into higher order code
with binders (lambda) in the underlying language. For instance, its
dependent sums:
{ x : A | P x }
can be defined via this mechanism, and desugar into something like:
Sig A (fun x => P x)
From what I recall from the docs, it's one of the syntax processors from
OCaml (in which Coq is implemented) that allows this sort of thing, so it's
possible you can do it in OCaml with its metaprogramming.
And of course, you could implement something like that in GHC with
quasiquoting, ending up with something like, for list comprehensions:
[$list| 2*x | x <- $xs |]
But that would involve parsing the relevant expression, of course (which,
there are ready-built Haskell parsers, but it's not as simple as the Coq
notations).
-- Dan
Dirk Thierbach
> is there any functional language in which it is possible to define
> custom binders -- apart from the Lisp family where its possible via macros?
Haskell with Template Haskell, OCaml with ocamlp, or more generally any
functional language which supports macro-like features in some way.
> What I have in mind are user defined (list) comprehensions, e.g.:
>
> [2*x | x <- xs]
>
> in which the variable x is bound in the 2*x part, or monadic notation like
>
> x <- f; g x
>
> meaning f >>= (\x -> g x) in Haskell notation.
If you're re-using existing Haskell syntactic sugar, you could get away
e.g. with just defining your own monad (depending on what you actually want
to do).
- Dirk