Hello all,
Stefan, the way you described the case composed of separate product and raw (untagged) sum certainly reminds me of the low-level languages we used to work in, but the types and proofs certainly become low-level is well. Macros can hide some of it, but I'm not sure I'd like macros doing the work that should 'rightfully' belong to the compiler... and I don't think ultra-low-level primitives is what you're aiming for with Typer.
So as you concluded here, I think a tagged sum as a primitive could work, but then the rest of the record/product is unspecified, in the style of row(ρ) polymorphism. We know field zero is an int, and the rest is a dependent type based on type-level discrimination of the singleton int type... or is that piece getting back to the low-level stuff?
CL
Stefan Monnier monnier@IRO.UMontreal.CA writes:
I think it is the most generic way to do it. It actually looks like something that someone would write in C to implement a dispatch/visitor with `0` being the RTTI field.
Yes, the way I presented it, it's very generic, indeed. Maybe a bit too much.
I cannot think of a situation where a cast would not be wanted by the user so maybe the switch could be simplified by making the cast implicit.
The idea was that the dispatch doesn't need to know about "union" or about the use of field 0. But indeed, that's a bit "too generic" for convenience.
Maybe it could be streamlined into a "switch e" which hard-codes the fact that the "tag" is in field 0. Hmm... I guess that could work.
Stefan
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer