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