Notes on polymorphic and extensible enums

[lpil]

http://2ality.com/2018/01/polymorphic-variants-reasonml.html

I like the extendibility here, I could imagine extendable error unions to be very useful. Perhaps having an explicit extension syntax would be good alternative to fully polymorphic variants.

enum MyError extends LibraryError =
  | ExtraError
  | AnotherError

[rizo]

You example is closer to extensible variants than to the polymorphic ones. The latter don’t need to be declared at all. Also, here’s an interesting article about error handling with polymorphic variants: http://keleshev.com/composable-error-handling-in-ocaml

[lpil]

For sure! I've been thinking about them and the most useful scenario I could think of was extension of error variants. If this is the main use then it could perhaps be simpler to have only extensible variants as in my example.

I'm not very familiar with either system I'm practice so it's not something I can have much of an opinion on yet.

[lpil]

Not entirely sure I agree with the article above as with regular variants you can have one case contain the parent error. It's a bit more boilerplate but it is possible.

I'm leaning towards being rather conservative when it comes to features, so I'm not sure I have a good reason for either of these features just yet.

[OvermindDL1]

Just as a note, in OCaml polymorphic variants are added on-demand to a global extensible variant map, so it is all the same thing there.

[lpil]

As explained in the comment above the pseudocode is showing extensible variants, not polymorphic ones.

This issue is just a short note to myself and isn't expected to make sense to other readers. I'll rename it to make it clearer.

[rizo]

@lpil Polymorphic variants are really useful in OCaml in combination with GADTs, which you must implement.

This is what happens when you make your WIP projects public! 😄

[lpil]

@lpil Polymorphic variants are really useful in OCaml in combination with GADTs, which you must implement.

Do you have an example of their use here? I have very little experience of GADTs (and no idea how they would be implemented).

This is what happens when you make your WIP projects public! 😄

I would go private but I'm a sucker for those stars!

[OvermindDL1]

Do you have an example of their use here? I have very little experience of GADTs (and no idea how they would be implemented).

The Traditional Example is a calculator (G)ADT, here seems to be a good example article on why GADT's are useful with this precise example: https://mads-hartmann.com/ocaml/2015/01/05/gadt-ocaml.html

Personally GADT's are absolutely required for me to be able to close over unknown types as there is no other way to represent such code in an HM-style typed system and I tend to use them at least once in every project.

[OvermindDL1]

The OCaml manual also has an example usage and reason of GADT's in it's listing as well: http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#s%3Agadts

[rizo]

I'm actually using GADTs with polymorphic variants in a project I'm currently working on. It's an MQTT client library. In the MQTT protocol you have two types of packets: client and server packets, but there might exist an intersection between them (some client packets can also be server packets, etc).

Here's a simplified example:

module Packet = struct
  (* Defines the packets that only clients can produce. *)
  type client = [
    | `Connect of connect_data
    | `Publish of publish_data
    | `Puback of puback_data
    (* ... *)
  ]

  (* Defines the packets that only servers can produce. *)
  type server = [
    | `Connack of connack_data
    | `Publish of publish_data  (* also appears in client *)
    | `Puback of puback_data    (* ditto *)
    (* ... *)
  ]

  (* All packet types united. *)
  type t = [ client | server ]

  (* The fun bit. Kind _does not_ hold a packet payload.
     It simply indicates what packet kind you want to work with. *)
  type 'packet kind =
    | Client : client kind
    | Server : server kind
    | Any : t kind
    | Connect : connack_data kind
    | Publish : publish_data kind
    (* ... *)

  (* The users can request to decode a packet from a particular subset. *)
  let decode : type packet . kind: packet kind -> char -> packet = ...
end

(* Now you can narrow your decoding to the particular place in which you
   accept certain subsets of packets. Eg: after connecting a client you know
   that you will expect a connack packet back from the server.
   You don't need to pattern match on the value and check, produce errors. *)
let p1: Packet.client = Packet.decode ~kind:Packet.Client data
let p2: Packet.server = Packet.decode ~kind:Packet.Server data
let p3: Packet.publish = Packet.decode ~kind:Packet.Publish data
let p4: Packet.t = Packet.decode ~kind:Packet.Any data

Note that the same function Packet.decode magically produces packets of completely different types. That happens because you generalised the function forall packet types and informed the type checker what would be a return type for a particular kind variant.

For simplicity the decoding function will raise an exception in this example in case of errors.

Disclaimer: this description probably isn't 100% accurate, etc.

[rizo]

Also note that using a GADT in this case avoids unnecessary allocations for packets that violate the protocol. Typically you would decode the full packet and then realise that you weren't actually expecting that one. In this case you explicitly request the kind you need, failing early.

[rizo]

I'm sorry for derailing your issue into mysterious territories :)

[lpil]

This is all great, thanks <3