The first version of this feature is going to look it is specified below. This will probably not be the final form of it.
New keyword lazy which goes on function parameters (after , and before field). Makes the type of the affected parameter equal to external.core.unit.Unit -> A with A being the original type in the source code. Most importantly, when applying a function with a lazy parameter, the argument is not immediately evaluated but rewritten into a thunk, that is a function from unit to the value. Note that outside of the function, that means when you apply it, the type of the argument must be of type A and cannot be of type Unit -> A (this should help type inference, unless mistaken), but inside of it, i.e. in the body of the function as well as the explicit type annotation of the body, it is of type Unit -> A. To evaluate the value, one can of course simply apply it to core.unit.unit, conventionally, however, one uses the function core.unit.force.
Example
;; core.bool:
use external.core.(unit.force bool.(Bool false true))
if (,A: Type) (condition: Bool) (lazy consequent alternate: A): A =
case condition of
true => force consequent
false => force alternate
;; user code:
use external.core.(bool.if nat.(Nat =< -))
result (switch: Nat): Nat =
if (=< switch 100)
0
(- switch 100)
Alternative Designs
similar to the one above but the parameter type needs to Unit -> A not A (which makes it less implicit). Additionally, add the type alias Thunk (A: Type): Type= Unit -> A to the standard library. Signature of if: (,A: Type) -> (condition: Bool) -> (lazy consequent: Thunk A) -> (lazy alternate: Thunk A) -> A
an attribute @lazy on expressions (meta: task: pros & cons)
a special type function à la @blessed lazy: Type -> Type = identity
a special parameterized type @blessed data Lazy (A: Type): Type with a constructor lazy
??
Coercions that should be legal:
(lazy a: A) -> P a to (a: A) -> P a forfeiting laziness becoming strict/eager
(a: A) -> P a to (lazy a: A) -> P a gaining laziness becoming lazy
most importantly, f a to f \_ => a if f of type (lazy A) -> B with a of type A
The first version of this feature is going to look it is specified below. This will probably not be the final form of it.
New keyword
lazywhich goes on function parameters (after,and beforefield). Makes the type of the affected parameter equal toexternal.core.unit.Unit -> AwithAbeing the original type in the source code. Most importantly, when applying a function with a lazy parameter, the argument is not immediately evaluated but rewritten into a thunk, that is a function from unit to the value. Note that outside of the function, that means when you apply it, the type of the argument must be of typeAand cannot be of typeUnit -> A(this should help type inference, unless mistaken), but inside of it, i.e. in the body of the function as well as the explicit type annotation of the body, it is of typeUnit -> A. To evaluate the value, one can of course simply apply it tocore.unit.unit, conventionally, however, one uses the functioncore.unit.force.Example
Alternative Designs
Unit -> AnotA(which makes it less implicit). Additionally, add the type aliasThunk (A: Type): Type= Unit -> Ato the standard library. Signature ofif:(,A: Type) -> (condition: Bool) -> (lazy consequent: Thunk A) -> (lazy alternate: Thunk A) -> A@lazyon expressions (meta: task: pros & cons)@blessed lazy: Type -> Type = identity@blessed data Lazy (A: Type): Typewith a constructorlazyCoercions that should be legal:
(lazy a: A) -> P ato(a: A) -> P aforfeiting laziness becoming strict/eager(a: A) -> P ato(lazy a: A) -> P againing laziness becoming lazyf atof \_ => aiffof type(lazy A) -> Bwithaof typeA