Make if lazy

[mariari]

Currently if is defined like

  if : {A : Type} → Bool → A → A → A;
  if true a _ ≔ a;
  if false _ b ≔ b;

and since the language is not lazy, this means both a and b will be evaluated.

This could be fixed by making if a "macro" or a "special form" in which it has lazy semantics. Likewise || and && should have the same properties (though || and && are special cases of if and thus not "special forms").

Further functions like:

ifOrd : {A : Type} → Ordering -> A → A → A → A;
ifOrd LT lt eq gt ≔ lt;
ifOrd EQ lt eq gt ≔ eq;
ifOrd GT lt eq gt ≔ gt;

should be deprecated, or a macro system should be had if this kind of abstraction is wanted. Or Alternatively a thunk version should be had if such form is wanted but no macro is had.

ifOrd : {A : Type} → Ordering -> (Unit -> A) → (Unit -> A) → (Unit -> A) → A;
ifOrd LT lt eq gt ≔ lt unit;
ifOrd EQ lt eq gt ≔ eq unit;
ifOrd GT lt eq gt ≔ gt unit;

[janmasrovira]

We want to investigate the possibility to support both call-by-value and call-by-name. However, it is not clear yet if we'll focus on this soon or not.

[mariari]

That seems quite ambitious, from what I understand Haskell has a lot of machinery (STG machine) in the compilation to make call-by-name fast. Thus it'll probably have a non noticeable affect on the binary size and speed and complexity of writing the compiler? A simpler approach is to either have special forms like that, or have a basic macro system that you can tell to auto box functions in lambda

inductive Unit {
  unit : Unit;
};

inductive Thunk (A : Type) {
  box : (Unit → A) → Thunk A;
};

call : Thunk A → A;
call (box thunk) ≔ thunk unit;

if-func : {A : Type} → Bool → (Thunk A) → (Thunk A) → A;
if-func true a _ ≔ call a;
if-func false _ b ≔ call b;

macro if : {A : Type} → Bool → A → A → A;
macro if x y z = `(if-func x (box ,y) (box ,z))

This approach still has costs if you don't make if special (I.E. implement something akin to the if above), namely the boxing of the arguments in if meaning an allocation is costed upon the calling of if which is something that would ideally be avoided. This allocation is that of a closure, as you may want to refer to other values where the code is called meaning in code like

-① : ℕ → ℕ;
-① (suc x) ≔ x;
-① zero    ≔ zero;

terminating
tak : ℕ → ℕ → ℕ → ℕ;
tak x y z ≔
  if (isLT (compare y x))
     (tak (tak (-① x) y z)
          (tak (-① y) z x)
          (tak (-① z) x y))
     z;

you'll be allocating 2 closures: the then clause would have x y and z in it's environment, the else clause would have z in it's environment when compile down.

For exact overhead view #1174, which lays out the closures explicitly in code.

[lukaszcz]

Indeed, closures are the way to implement laziness in an eager functional programming language. The OCaml compiler does exactly that under the hood. This works fine if you're eager most of the time and need laziness only occasionally. Though then one definitely needs "if", "&&", "||", etc., as special syntactic constructs (i.e., keywords in the language grammar) which are compiled separately.

Whether we need a macro system is a longer and separate discussion. It seems that macros help in implementing "if" only if either you already have a way of indicating that something is lazy or you use them to "box" the arguments in a closure. For an eager language you need a special syntax for "if" which avoids the closures.

Btw, I consider this a bug. "if" has to be lazy.