Questions about erasures

[higherorderco]

Questions about erasures

[Eloitor]

Okay, thanks for your answer.

I assumed that erasures made the data unavailable, now I see that this is not the case and you can use it only in erased positions.

Following your example,

f(x: Bool): Bool
  case x
  | true => false
  | false => true

copy_f : Copy(Bool -> Bool, f)
    copy(__ f, equal(__), copy_f)

useCopyf(cpyf: Copy(Bool -> Bool, f)): Pair(Bool -> Bool, Bool -> Bool)
  case cpyf
  | copy => case cpyf.cpy as ff
  | copy => pair(__ cpyf.val , ff.val)

main useCopyf(copy_f)

This type-checked correctly.

[VictorTaelin]

Two questions:

1. Why exactly erasure prevents something from being copiable?

2. How do you copy something like a Bool -> Bool function? As far as I know, we can make a copy for any first-order type like bools, lists, and most common datatypes, but not for functions.

About your questions:

1. Intuitively (as in, I'm not sure) I think any algebraic datatype without functions is copiable. The way we've been thinking in making this part of the language is by automatically deriving a copy : A -> Pair(A,A) function for any algebraic datatype (i.e., in the same way we could derive show, read instances).

2. I don't know, that's a great question.

3. It is to prevent affecting the runtime performance by something that should have zero cost, such as imposing type-level restrictions to a type. If you don't plan to run it, you just can use Sigma.

About copy, here is an alternate way to make affine copies:

// Allows copying a value many times in an affine setup
T Copy<T> (x: T)
| copy(
  x   : T;
  val : T,
  eql : Equal(T,val,x),
  cpy : Copy(T,x)
  ) : Copy(T,x)

That allows you to copy a copyable value as many times as you want without leaving the affine subset. For example, here is a function that returns an infinite list of copies of a copyable value:

// Copies a value infinitely many times
copies(n: Nat; cpy: Copy(Nat, n)) : List(Sigma(Nat, (x) => x == n))
  case cpy
  + equal(Nat; n;) as e0 : Equal(Nat, cpy.x, n)
  + equal(Nat; n;) as e1 : Equal(Nat, cpy.x, n)
  | copy =>
    let ceql = cpy.eql :: rewrite Equal(Nat, cpy.val, .) with e0
    let head = sigma(_ (x) => x == n; cpy.val, ceql)
    let tail = main(n; cpy.cpy :: rewrite Copy(Nat, .) with e1)
    cons(_ head, tail)

And here is a Copy instance for true:

copy_true : Copy(Bool, true)
  copy(__ true, equal(__), copy_true)