Re: ocaml-dns- quick ocaml question

[Raphael Proust <raphlalou@xxxxxxxxx>]

On Mon, Jun 18, 2012 at 8:43 PM, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:
> So cstruct shouldnt be a constraint; it's trivial to retarget to polymorphic 
> variants. There is a very slight performance hit, but I don't think that 
> matters.
>
> GADTs: I don't see how they help here; did you have anything in mind Raphael, 
> or was it a general "new shiny feature"? :-)

It's a new shiny featureâ that can be used to enforce some sub-typing
invariants.

The Ocsigen project plans to rewrite their polymorphic-variant based phantom
types using GADTs. The way to do it is to put a phantom type and
constrain its value in the branches of the variant.


Considering

>>> type q
>>> type rr
>>> type 'a t =
>>> | Foo : 'a t
>>> | Bar : int -> 'a t
>>> | Baz : float -> q t (* This branch forces the ['a] to be instantiated with
>>> Â Â Â Â Â Â Â Â Â Â Â Â [q], thus preventing anyuse with functions requiring
>>> Â Â Â Â Â Â Â Â Â Â Â Â [rr t]
>>> Â Â Â Â Â Â Â Â Â Â Â *)

You can constrain a function to accept only values of type [rr t] or [q t] or
both ['a t].

The example in
http://caml.inria.fr/pub/distrib/ocaml-4.00/ocaml-4.00beta-refman.html#htoc113
is nice:

type _ term =
  | Int : int -> int term
  | Add : (int -> int -> int) term
  | App : ('b -> 'a) term * 'b term -> 'a term
let get_int : int term -> int = function
  | Int n    -> n
  | App(_,_) -> 0


Thus, in the foo-bar-baz example, one could code:

let process_query : q t -> unit = function
  | Foo -> ..
  | Bar i -> ..
  | Baz f -> ..
let process_reply : rr t -> unit = function
  | Foo -> ..
  | Bar i -> ..
  (* adding a Baz match would be an error here, as [rr t] and [q t] are
     incompatible *)




-- 
_______
Raphael