Hello, we have polymorphic variants and we also have GADTs. Is there such a thing as a polymorphic generalized variant? Would such a thing even make sense?
p1. I have a hunch that type inference would be hairy and probably depend on explicit type annotations. Maybe somebody with more type theory under their belt could answer.
p2. I don’t see much need for them given that extensible variants can be GADT.
Thank you for your answer. Can you demonstrate how extensible variants can be GADT?
I just now realized this is in the Learning category, and I should have offered to show that without being prompted. Sorry. Here’s a transcript of a session I just did in utop that hopefully explains how you can do it:
─( 23:48:15 )─< command 0 >─
utop # type _ t = ..;;
type _ t = ..
─( 23:48:15 )─< command 1 >─
utop # type _ t += String: string -> string t;;
type _ t += String : string -> string t
─( 23:48:30 )─< command 2 >─
utop # type _ t += Int: int -> int t;;
type _ t += Int : int -> int t
─( 23:48:47 )─< command 3 >─
utop # String "example";;
- : string t = String "example"
─( 23:48:56 )─< command 4 >─
utop # Int 23;;
- : int t = Int 23
Here, type 'a t is an extensible GADT, currently with two constructors, String and Int. Does that help clarify? Oh, and welcome to OCaml Discuss, @MarcCoquand!
3 Likes
Neat, that clarifies it. Thank you!