Implicit Thunk/Force or Bind/Ret

[maxsnew]

So there's a lot of syntactic overhead currently using CBPV compared to CBN/CBV, which we can think about in terms of the translations into CBPV:

1. In CBN, all variables have type Thunk(b), and force/thunk are implicit: if you use a variable in evaluation position it is forced, and if you use a computation in a value position it is thunked.
2. In CBV, all computations have type Ret(a) and ret/bind are implicit: if you use a variable in a computation position it is returned, and if you use a computation in a variable position, it is binded, using a left-to-right evaluation order.

We could make Zydeco "more CBV" or "more CBN" by default by picking one of these syntactic conventions.
Or we could support all three different syntaxes: CBPVsh, CBVish and CBNish. Note that either way, we would still have the same underlying type system, and we wouldn't get the "usual" CBV and CBN syntax.

For instance in true CBV if you write fn x -> fn y -> add x y it would desugar to have the type U(Int -> F(U(Int -> F(Int)))) but in my "CBVish" proposal it would have type U(Int -> Int -> Ret(Int), and if you wanted the original you would write fn x -> { fn y -> add x y }.

Similarly, in true CBN if you write Pair(1, 2) it would desugar to have the type F(StrictPair(UF(Int), UF(Int))) whereas in our syntax it would be a value of type StrictPair(Int, Int) and if you want the original you would write ret Pair(ret 1, ret 2), where StrictPair is defined as

data StrictPair a1 a2 where
| Pair(a1, a2)