Mutual Definition Message/Intuition

[mariari]

When trying to make my tak benchmark fast I ran into an issue.

module tak;

open import Prelude;
open import Data.Nat;
open import Data.Nat.Ord;
open import Complex;
     import Data.Bool;
open import Data.Ord;

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


inductive Unit {
  unit : Unit;
};

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

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

if : {A : Type} → Data.Bool.Bool → (Thunk A) → (Thunk A) → A;
if Data.Bool.true  then else ≔ call then;
if Data.Bool.false then else ≔ call else;


terminating
tak-then : ℕ → ℕ → ℕ → Unit -> ℕ;
tak-then x y z unit ≔
  (tak (tak (-① x) y z)
       (tak (-① y) z x)
       (tak (-① z) x y));

tak-else : ℕ → Unit → ℕ;
tak-else z unit ≔ z;

terminating
tak : ℕ → ℕ → ℕ → ℕ;
tak x y z ≔
  if-func (isLT (compare y x))
          (box (tak-then x y z))
          (box (tak-else z));

end;

with the following error message

Symbol not in scope: tak

splitting up the function leads into the issue where I need to call tak from tak-then or stage it in a way that is similar to placing jump labels by hand.

module tak;

open import Prelude;
open import Data.Nat;
open import Data.Nat.Ord;
open import Complex;
     import Data.Bool;
open import Data.Ord;

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


inductive Unit {
  unit : Unit;
};

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

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

if : {A : Type} → Data.Bool.Bool → (Thunk A) → (Thunk A) → A;
if Data.Bool.true  then else ≔ call then;
if Data.Bool.false then else ≔ call else;

tak-else : ℕ → Unit → ℕ;
tak-else z unit ≔ z;

terminating
tak-branch : (ℕ → ℕ → ℕ → Unit → ℕ) → ℕ → ℕ → ℕ → ℕ;
tak-branch tak-then x y z ≔
  if (isLT (compare y x))
     (box (tak-then x y z))
     (box (tak-else z));

terminating
tak-then : ℕ → ℕ → ℕ → Unit → ℕ;
tak-then x y z unit ≔
   tak-branch tak-then
              (tak-branch tak-then (-① x) y z)
              (tak-branch tak-then (-① y) z x)
              (tak-branch tak-then (-① z) x y);


terminating
tak : ℕ → ℕ → ℕ → ℕ;
tak ≔ tak-branch tak-then;

end;

where I have to pass in the recursive branch tak-then to tak-branch then setup my tak function to be the curried version of trak-branch basically, doing label jump points by hand.

As a side note, the explicit box call in tak-branch can be replaced to the tak-then and tak-else call once local lambdas are added to the language.

[mariari]

Upon further reading, there is a way to express mutual functions

terminating tak      : ℕ → ℕ → ℕ → ℕ;
terminating tak-then : ℕ → ℕ → ℕ → Unit -> ℕ;
            tak-else : ℕ → Unit → ℕ;

tak-then x y z unit ≔
  (tak (tak (-① x) y z)
       (tak (-① y) z x)
       (tak (-① z) x y));

tak-else z unit ≔ z;

tak x y z ≔
  if (isLT (compare y x))
     (box (tak-then x y z))
     (box (tak-else z));

The above does work, however I was unsure of the convention on how to achieve this. Might be good to have a comment about it, since I think due to how the language ingests terms, the information should be around about the unknown symbol.

[paulcadman]

We'll clarify mutually recursive functions in the documentation.