Question: Will Sixten support specifying erasure like Idris 2?

[L-as]

Are you planning to support specifying erasure, e.g. like (0 _ : x = y) -> x -> y.

[ollef]

I'm not sure. It seems to be more complicated in Sixten because values that are only used in types can not always be erased (when they contribute to type size calculations at runtime).

Either way, propositional equality is of size zero, so the equality proof doesn't need to be passed to your function because it doesn't really exist at runtime.

[L-as]

I'm currently trying to make a red-black tree in Idris, and it's very helpful to know that you can mark data as erased, so that you are sure it's only used for proofs. An excerpt:

data Color = Red | Black

data GoodTree :
  {height : Nat} ->
  {color : Color} ->
  {kt : Type} ->
  {kord : LawfulOrd kt} ->
  {keys : List kt} ->
  {vt : kt -> Type} -> Type
where
  Empty : GoodTree {height = 0, color = Black, keys = []}
  RedNode :
    {0 kord : LawfulOrd kt} ->
    (k : kt) ->
    {0 kp : In (k ==) keys} ->
    vt k ->
    GoodTree {height, color = Black, kt, kord, keys = filter (k >) keys, vt} ->
    GoodTree {height, color = Black, kt, kord, keys = filter (k <) keys, vt} ->
    GoodTree {height, color = Red, kt, kord, keys, vt}
  BlackNode :
    {0 kord : LawfulOrd kt} ->
    (k : kt) ->
    {0 kp : In (k ==) keys} ->
    vt k ->
    GoodTree {height, kt, kord, keys = filter (k >) keys, vt} ->
    GoodTree {height, kt, kord, keys = filter (k <) keys, vt} ->
    GoodTree {height = S height, color = Black, kt, kord, keys, vt}

The correctness of the tree depends on the Ord implementation, but we do not want to carry around the Ord implementation in the tree. There are also proofs of the fact that the key is in some list of keys, which have the following structure:

data In : (a -> Bool) -> List a -> Type where
  MkIn : (x : a) -> (f x = True) -> (xs : List a) -> In f (x :: xs)
  MkInCons : (x : a) -> (xs : List a) -> In f xs -> In f (x :: xs)

Without the 0, in Idris these would add a lot of extra unnecessary data to the tree. How would you achieve the same in Sixten without allowing specifying erasure?

[ollef]

Yeah, I don't have a good answer to this question at the moment. It seems like it would still be useful to have some sort of user specified erasure in Sixten despite e.g. zero sized data.