Timeline for What's the difference between Row Polymorphism and Structural Typing?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 24, 2020 at 14:59 | vote | accept | hgs3 | ||
| Sep 20, 2020 at 22:29 | comment | added | Andrej Bauer | Very good. I didn't find effect polymorphism mentioned on the web page. And we're in agreement regarding bad ideas in PL :-) | |
| Sep 20, 2020 at 21:39 | comment | added | Dan Doel |
Yes, it has effect polymorphism. And I think I already mentioned that making Two and Bool structural is not a good thing to do in practice, and they should be declared to be nominal instead. That probably extends to any data type with multiple constructors with the same signature. I picked the example to be short.
|
|
| Sep 20, 2020 at 20:42 | comment | added | Andrej Bauer |
Would you actually recommend identifying False and Zero as good PL design? Cause I sure wouldn't.
|
|
| Sep 20, 2020 at 20:41 | comment | added | Andrej Bauer |
This is kind of tangential, but does Unison have any effect polymorphism? If not, what's the type of iter : ('a -> unit) -> 'a list -> unit? I've been wondering ever since I heard of Unison.
|
|
| Sep 20, 2020 at 18:51 | comment | added | Dan Doel | I actually do work on a language (unison) that would enable you to do my example, basically because it is just two different naming schemes applied to the same data declaration structure, and the system recognizes this. However, you can also declare nominal types, because enum examples like this easily lead to confusion. Also there isn't any subtyping involved; it is just structural in the sense that the exact structure determines the type, rather than the names used. | |
| Sep 20, 2020 at 18:48 | comment | added | Dan Doel |
Well, I'm not talking about e.g. homotopy type theory. I'm talking about a "structural type system" that makes these two types automatically interchangeable. This necessarily involves something kind of ad-hoc, like making False = Zero because they're both the first constructor. Univalence is kind of another angle on what a 'structural' theory could be, but I'm not sure it fits the wiki article linked.
|
|
| Sep 20, 2020 at 8:56 | comment | added | Andrej Bauer |
I wouldn't say that Bool and Two are "actually the same type". At best they are isomorphic, or propositionally equal in a type theory with univalence. An additional problem is that they are equal/isomorphic in two different ways, so you'd immediately break coherence of subtyping. Have you seen any actually subtyping systems that equate the two?
|
|
| Sep 20, 2020 at 0:03 | history | answered | Dan Doel | CC BY-SA 4.0 |