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
'a t is an extensible GADT, currently with two constructors,
Int. Does that help clarify? Oh, and welcome to OCaml Discuss, @MarcCoquand!
Neat, that clarifies it. Thank you!