[GHC] #8288: add idris style EDSL support for deep embedding lambdas

[GHC]

#8288: add idris style EDSL support for deep embedding lambdas
-------------------------------------+-------------------------------------
              Reporter:  carter      |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:  7.10.1
              Priority:  normal      |          Version:  7.6.3
             Component:  Compiler    |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Project (more
  Unknown/Multiple                   |  than a week)
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by rodlogic):

 Found [http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf
 this] in section 11.
 {{{
 11 Syntax Extensions
 IDRIS supports the implementation of Embedded Domain Specific Languages
 (EDSLs) in several ways [4]. One way, as we have already seen, is through
 extending do notation. Another important way is to allow extension of the
 core syntax. In this section we describe two ways of extending the syntax:
 syntax rules and dsl notation.
 11.1 syntax rules
 We have seen if...then...else expressions, but these are not built in.
 Instead, we can define a function
 in the prelude as follows (we have already seen this function in Section
 3.7:
    boolCase : (x:Bool) -> Lazy a -> Lazy a -> a;
    boolCase True  t e = t;
    boolCase False t e = e;
 and then extend the core syntax with a syntax declaration:
 syntax "if" [test] "then" [t] "else" [e] = boolCase test t e;
 The left hand side of a syntax declaration describes the syntax rule, and
 the right hand side describes its expansion. The syntax rule itself
 consists of:
 • Keywords — here, if, then and else, which must be valid identifiers
 • Non-terminals — included in square brackets, [test], [t] and [e] here,
 which stand for arbitrary expressions. To avoid parsing ambiguities, these
 expressions cannot use syntax extensions at the top level (though they can
 be used in parentheses).
 • Names — included in braces, which stand for names which may be bound on
 the right hand side.
 • Symbols — included in quotations marks, e.g. ":=". This can also be used
 to include reserved words
 in syntax rules, such as "let" or "in".
 The limitations on the form of a syntax rule are that it must include at
 least one symbol or keyword, and there must be no repeated variables
 standing for non-terminals. Any expression can be used, but if there are
 two non-terminals in a row in a rule, only simple expressions may be used
 (that is, variables, constants, or bracketed expressions). Rules can use
 previously defined rules, but may not be recursive. The following syntax
 extensions would therefore be valid:
 syntax [var] ":=" [val] = Assign var val;
 syntax [test] "?" [t] ":" [e] =iftestthentelsee; syntax "select" [x]
 "from" [t] "where" [w] = SelectWhere x t w; syntax "select" [x] "from" [t]
 = Select x t;
 Syntax macros can be further restricted to apply only in patterns (i.e.,
 only on the left hand side of a pattern match clause) or only in terms
 (i.e. everywhere but the left hand side of a pattern match clause) by
 being marked as pattern or term syntax rules. For example, we might define
 an interval as follows, with a static check that the lower bound is below
 the upper bound using so:
 data Interval : Type where
 MkInterval : (lower : Float) -> (upper : Float) ->
                    so (lower < upper) -> Interval
 We can define a syntax which, in patterns, always matches oh for the proof
 argument, and in terms requires a proof term to be provided:
 44
 pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
 term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
 In terms, the syntax [x...y] will generate a proof obligation bounds_lemma
 (possibly renamed). Finally, syntax rules may be used to introduce
 alternative binding forms. For example, a for loop binds
 a variable on each iteration:
 syntax "for" {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
 main : IO ()
 main = do for x in [1..10]:
                  putStrLn ("Number " ++ show x)
              putStrLn "Done!"
 Note that we have used the {x} form to state that x represents a bound
 variable, substituted on the right hand side. We have also put "in" in
 quotation marks since it is already a reserved word.
 11.2 dsl notation
 The well-typed interpreter in Section 6 is a simple example of a common
 programming pattern with dependent types. Namely: describe an object
 language and its type system with dependent types to guarantee that only
 well-typed programs can be represented, then program using that
 representation. Using this approach we can, for example, write programs
 for serialising binary data [1] or running concurrent processes safely
 [2].
 Unfortunately, the form of object language programs makes it rather hard
 to program this way in practice. Recall the factorial program in Expr for
 example:
    fact : Expr G (TyFun TyInt TyInt)
    fact = Lam (If (Op (==) (Var stop) (Val 0))
                   (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
                                   (Var stop)))
 Since this is a particularly useful pattern, IDRIS provides syntax
 overloading [4] to make it easier to program in such object languages:
 dsl expr
 lambda = Lam variable = Var index_first = stop index_next = pop
 A dsl block describes how each syntactic construct is represented in an
 object language. Here, in the expr language, any IDRIS lambda is
 translated to a Lam constructor; any variable is translated to the Var
 constructor, using pop and stop to construct the de Bruijn index (i.e., to
 count how many bindings since the variable itself was bound). It is also
 possible to overload let in this way. We can now write fact as follows:
    fact : Expr G (TyFun TyInt TyInt)
    fact = expr (\x => If (Op (==) x (Val 0))
 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
 In this new version, expr declares that the next expression will be
 overloaded. We can take this further,
 using idiom brackets, by declaring:
    (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
    (<$>) = \f, a => App f a
    pure : Expr G a -> Expr G a
    pure = id
 45
 Note that there is no need for these to be part of an instance of
 Applicative, since idiom bracket notation translates directly to the names
 <$> and pure, and ad-hoc type-directed overloading is allowed. We can now
 say:
    fact : Expr G (TyFun TyInt TyInt)
    fact = expr (\x => If (Op (==) x (Val 0))
                          (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
 With some more ad-hoc overloading and type class instances, and a new
 syntax rule, we can even go as far as:
 syntax "IF" [x] "THEN" [t] "ELSE" [e] = If x t e fact : Expr G (TyFun
 TyInt TyInt)
    fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8288#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler