Brent Yorgey c982e81790 Delay type (#223) ... Make explicit in the type system when evaluation of a computation should be delayed. This gives the user fine-grained control over selective laziness (for example, once we have sum types and recursive types, one could use this to define lazy infinite data structures). It also allows us to guarantee that certain commands such as `build` and `reprogram` delay evaluation of their arguments, and lets the user e.g. define their own modified versions of `build` without compromising those guarantees. - Delay is indicated by curly braces both at the value and type levels, that is, if `t : ty` then `{t} : {ty}`. - `force : {ty} -> ty` is now exposed in the surface language. - Change from a CEK machine to a CESK machine. Recursive `let` and `def` delay via allocating a cell in the store. For now, there is no other way to allocate anything in the store, but see discussion at #150 for some possible future directions. - change the types of `build` and `reprogram` to require a delayed program, e.g. `build : string -> {cmd a} -> cmd string` - `if` and `try` also require delayed arguments. - don't elaborate Build and Reprogram with extra Delay wrappers since one is now required by the type - Division by zero, negative exponents, and bad comparisons now throw exceptions. Closes #150. Closes #226.		2021-10-25 13:28:41 +00:00
..
Benchmark.hs	Delay type (#223)	2021-10-25 13:28:41 +00:00