[CN] Currently no good feature for accessing fields of datatypes

[elaustell]

If I have an instance l of a CN datatype, such as seq, and I want to access one of its members, such as its head, currently the only way of doing this with a "getter" function with match cases. For example,

function (i32) hd (datatype seq l) {
  match l {
    Seq_Nil {} => { 0i32 }
    Seq_Cons {head : h, tail : _} => { h }
  }
}

While this is a fine workaround for a seq of type int, where we can return 0i32 for the head of an empty list, this method breaks down for datatypes of other datatypes. For example, consider the following datatype:

datatype foo {
  foo_Nil {},
  foo_Cons {struct Bar head, datatype foo tail}
}

Now if I want to access the head of an instance of type foo, I can't write a "getter" method:

function (struct Bar) hd (datatype foo l) {
  match l {
    foo_Nil {} => { ??? }
    foo_Cons {head : h, tail : _} => { h }
  }
}

Since I need to return a struct, there is nothing I can return in this method for the Nil case. As far as I can tell, CN does not allow for the instantiation of a struct in ghost code. Additionally, there is no NULL term in CN that could be returned here. I believe something that could solve this problem would be a . operator for member access. Then users could call something like l.head without having to worry about these match cases.

TLDR: Please implement foo.bar for member access of datatypes.

[cp526]

CN has an expression default that would work here: for a given CN basetype bt, the expression default<bt> is a CN value at that basetype. This is an expression for which CN can prove nothing other than default<bt> == default<bt>.

So the following should work:

function (struct Bar) hd (datatype foo l) {
  match l {
    foo_Nil {} => { default<struct Bar> }
    foo_Cons {head : h, tail : _} => { h }
  }
}

(I believe default is not yet documented in the CN tutorial.)

Having accessors, such as the foo.bar you're suggesting, would be more C-like, but a bit more awkward to handle in the typesystem. Plus it makes the "partiality" of specifications such as the one above more implicit, thus easier to overlook.

[dc-mak]

Sometimes I wonder if having just one default value could potentially lead to spurious and unintended equalities.