Open larsrh opened 12 months ago
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)
I see two ways to do this:
Suc_dest
takes a Nat
and returns an additional bool
to tell if the cast was succesful.Suc_coerce
that takes the role of x.(Suc)
.(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.)
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: