Allow multiple uses of recursive datatypes

[colin-mcd]

Let

data Nat = Zero | Succ Nat;

define add : Nat -> Nat -> Nat =
  \ m. \ n. case n of
    | Z -> m
    | S n' -> S (add m n');

Given these, one might wish to define a mult function:

define mult : Nat -> Nat -> Nat =
  \ m. \ n. case n of
    | Z -> S Z
    | S n' -> add m (mult m n');

However, given that—IIUC—we currently restrict local vars with recursive datatypes from being used multiple times (just like we do with functions), add m (mult m n)' raises an error for its two uses of m. But if you first define

define copy : Nat -> Nat * Nat =
  \ n : Nat. case n of
    | Zero -> (Zero, Zero)
    | Succ n' -> let (n1, n2) = nats n' in (S n1, S n2);

then you can define mult as

define mult : Nat -> Nat -> Nat =
  \ m. \ n. case n of
    | Z -> S Z
    | S n' -> let (m1, m2) = copy m in add m1 (mult m2 n');

Computing a copy function behind-the-scenes would be pretty easy—more or less just make a naive fixpoint, but pair all values—so why don't we do this automatically and allow add m (mult m n')?

[davidweichiang]

Sorry I missed this earlier. Theoretically, I can't think of a problem with this. Practically, would you be able to make the copies only when they are needed?

[colin-mcd]

Yeah, I don't think that would be too hard. The only consideration I can think of is if you had the terms add n n and add (add n n) n, would we want to make the three values like let (n1, n23) = copy n in let (n2, n3) = copy n23 in add (add n1 n2) n3, or create a custom copy function for each number of copies (i.e. copy2 : Nat -> (Nat * Nat) and copy3 : Nat -> (Nat * Nat * Nat))?