Design syntax and type inference rules for staging.

[johnynek]

as part of #193 we need to have a syntax and type inference rules.

Here is a strawman:

def times3(i: Int) -> Code[Int]:
  ${3.times(i)}

six = times3(2)!

Inside of a ${ } we can have a Declaration that converts to an Expr which will have type Int in this example. The type of ${ } will be Code[a] where a is the type of the inside expression.

A ! is a suffix operator which has type: Code[a] -> a, but that function is fun at compile time but may error (fail to compile). We can error if we try to run, but the code can't statically see everything needed, e.g.:

def bad(x): times3(x)!

We can't run this because where bad is bound, x is unknown, so we can't evaluate.

[johnynek]

There is some syntactic similarity between the above syntax and the #426

In this code, you can imagine that " is the escaping into the string-language. and ${foo} unescapes to put the expression language into the string language.

But, with the staging ${foo} lifts the expression language into a Code[a] value, and foo! does the splicing of code values into expression values.

It would be nice to have either very similar or very different syntaxes. Since for code splicing, we want it to be very clean, it seems a bit ugly to have to do ${foo} to splice in code. It also looks bad if you do staging inside interpolation: ${${foo}} would be legal, the outer one doing string interpolation and the inner one doing code splicing.

I think this suggests, since ${foo} looks similar to Scala, Kotlin and Python, we should use that for string splicing and make code escapes be something other than ${foo(x)}.

Here are some alternate code escaping syntax proposals:

def pow(x, n: BinNat) -> Code[Int]:
  recur n:
    BinNatZero: [[ 1 ]]
    BinNatOdd(n):
      [[
        xh = pow(x, n)!
        x2 = xh.times_BinNat(xh)
        x.times(x2)
      ]]
   BinNatEven(n):
      [[
        xh = pow(x, n)!
        xh.times_BinNat(xh)
      ]]

Other ideas: $[ foo ] [| foo |] [> foo <]