Created
May 2, 2024 03:15
-
-
Save graydon/a87edfb3ddda9ff9ec0125f3c79a37cc to your computer and use it in GitHub Desktop.
polymorphic variants in ocaml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* The magic of ocaml polymorphic variants: | |
* | |
* - subsystem A produces an error `NSaServ | |
* - subsystem B checks for error `SaupDOF | |
* - both exist in a world with some extra variant `Common | |
* | |
* the two odd symbols _hash to the same representation_ in ocaml's | |
* implementation of polymorphic variant tagging. | |
*) | |
let a_err : [> `Common ] = `NSaServ;; | |
let b_fn : [> `Common ] -> unit = | |
fun x -> match x with | |
| `Common -> print_string "got commom" | |
| `SaupDOF -> print_string "got SaupDOF" | |
| _ -> () | |
;; | |
(* | |
* Even though both definitions above compile, the function application | |
* below will fail to compile with the message: | |
* | |
* Error: Variant tags `SaupDOF and `NSaServ have the same hash value. | |
* Change one of them. | |
* | |
* I think this is because the type [> `Common] in the source code is | |
* essentially a row type with an invisible type variable representing | |
* the extra variants, and the typechecker expands the type of `a_err` | |
* to [> `Common | `NSaServ], and `b_fn` to [> `Common | `SaupDOF] -> | |
* unit, and then tries to unify arg and param and produces a type | |
* like [> `Common | `SaupDOF | `NSaServ] and then notices that is not | |
* an allowed type at all, because it has an _internal_ collision, and | |
* they decided this was a relatively acceptable rare failure mode to | |
* leave in the language: the only expressions you can form that would | |
* behave ambiguously due to tag-collision get typed at a row-type | |
* that the typechecker can see the collision in, and reject. | |
* | |
* I cannot decide if this is more or less cursed a design choice | |
* than allowing both single ` and ' as prefix sigils with completely | |
* different meaning. | |
*) | |
b_fn a_err ;; |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment