Hi guys,
Wondering if you might have an idea:
In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case".
It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler.
While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large.
I'd like to find another option and was thinking of something along the following lines:
- provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int".
then the Either type could look like
Either a b = union (Singleton(1), a) (Singleton(2), b)
and
case e | Left x => ... | Right y => ...
would turn into
switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ...
Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union.
The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well.
Does anyone here have another approach to suggest?
Stefan
Afficher les réponses par date
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.
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.
Haskell, Coq and Agda all have algebraic datatypes. How do they do it ?
Because Stefan’s solution is not very user-friendly if we have to write the Either datatype like that. Plus if a macro can do the conversion, so should the compiler before generating intermediate code. We also have to think about the macros. What would a programmer expect when receiving code with a “case” in it. The simple algebraic datatype version or the more complex like in Stefan’s email ?
Vincent
On Jan 31, 2017, at 5:45 PM, Pierre Delaunay pierre.delaunay.tr@gmail.com wrote:
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.
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.
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer
Haskell, Coq and Agda all have algebraic datatypes. How do they do it ?
I'm pretty sure they have a mix of: - don't treat modules as datatypes - special case the single-alternative datatype (aka "record").
Because Stefan’s solution is not very user-friendly if we have to write the Either datatype like that.
You'd use a macro to hide the boilerplate.
Plus if a macro can do the conversion, so should the compiler before generating intermediate code.
Not sure what you mean.
We also have to think about the macros. What would a programmer expect when receiving code with a “case” in it.
Same here.
Stefan
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
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
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.
Actually, I do want to move as much of the compilers's work to libraries (sometimes via macros), and I'd be happy if that gives access to very low-level operations.
I think the problem is whether it will be workable in practice (the cost of constructing/manipulating all those extra proofs could be prohibitive).
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?
Indeed, maybe a middle point where we hard code the "switch on field-0 which is an int". That still allows funny things such as take a tuple from one union type and use it as-is in another union type.
Stefan
Stefan Monnier monnier@iro.umontreal.ca wrote more than a year ago:
Wondering if you might have an idea:
In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case".
It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler.
While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large.
I just pushed a new branch "report/itd" where I'm working on an article that tries to provide a partial answer. It doesn't try to address point 3 and keeps tags (which I call "labels") abstract (I'm not sure it should be addressed at this level).
I intend to submit it to CPP'2019 two weeks from now (Oct 18). Anybody interested is welcome to join. The main contribution is supposed to be first a proof of equivalence of "CC + tuples + tags + union + eq-type + recursion" and "CC + inductive types" (where those inductive types follow the design of Gimenez's "case + guarded recursion") and second a proof that the intended low-level semantics (where `case` doesn't do anything more than C's `switch`) is valid.
Formalizing CC in something like Coq is pretty hard, so clearly these proof will be paper proofs (and won't be in the paper, except maybe for some highlights).
Stefan
-
Christopher League -
Pierre Delaunay -
Stefan Monnier -
Stefan Monnier
-
Vincent Archambault-Bouffard