Safer use of datatypes

[larsrh]

Currently, datatypes are generated as a set of structs that represent the constructors. The datatype itself is generated as any.

Because of how Go's structs and interfaces work, there is really not much of a better approach here.

But we can try to make the "outer shell" a bit safer, and, say, prevent someone passing a number to a function expecting a list.

We could change the way datatypes are generated as follows:

type Nat struct {
  value nat;
}
type nat any;
type Zero struct { };
type Suc struct { A Nat; };
func Suc_dest(p Suc)(Nat) {
  case return q.A;
}
func Mk_zero()(Nat) {
  return Nat{nat(Zero{})};
}
func Mk_suc(A Nat)(Nat) {
  return Nat{nat(Suc{A})};
}

[stuebinm]

So I see this as being two parts: firstly, we have separate constructors. this is pretty easy to implement, but also doesn't gain us much — type checking on these functions is not "safer" in any way than just initialising the structs. The second is in having an extra wrapper around the type, which is significantly harder, mostly because of how we currently implement pattern matches:

func Plus_nat (x0 Nata, n Nata) Nata {
  {
    q, m := x0.(Suc);
    if m {
      ma := Suc_dest(q);
      ...

the q,m := x0.(Suc) assertion no longer works with the above, since pattern matches outside the type's package can't access the (now wrapped) field anymore. So we'd need another wrapper around that … i'm not sure how much more complicated that'd make things, but will have a look.

(and while we're not prioritizing performance in this translation, i'm unsure about the potential impact of having yet another wrapper type, i.e. another pointer indirection. i don't know if the go compiler optimises them away, in any case)

[larsrh]

I see two ways to do this:

1. Suc_dest takes a Nat and returns an additional bool to tell if the cast was succesful.
2. We introduce another function Suc_coerce that takes the role of x.(Suc).

[larsrh]

(and while we're not prioritizing performance in this translation, i'm unsure about the potential impact of having yet another wrapper type, i.e. another pointer indirection. i don't know if the go compiler optimises them away, in any case)

I think the only way to find out would be to measure, but then we would need to come up with a reasonable benchmark first. (Such a benchmark may be useful in any case.)