Support for types with constraints

[ejgallego]

Dear ppx_sexp_conv devs,

first, thank you for this great library! Do you think it would be possible to support types using constraint. Example:

type 'a ty =
  | C1 of 'tr * 'tm
  | C2 of 'tm * 'tr
constraint 'a = < e1 : 'tr; e2: 'tm >
[@@deriving sexp]

Currently, it fails with:

Error: The universal type variable 'a cannot be generalized: it is not a variable.

Coq uses such pattern for the internal representation of its tactic language so it'd be great to be able to use ppx_sexp_conv there.

I'm on 113.33.01+4.03. Best regards.

[ejgallego]

This other two related examples also fail to be derived:

type ty2 = < f1 : int; f2 : int >

type ('a, 'b) ty3 =
  | E1 of 'a * 'b
  constraint 'a = 'b

[ghost]

It's a bit of work but it should be possible to support constraints. My only concern is that the generated functions won't be regular. Currently the generated functions have the same arity as the type, but for instance for ty we'd have:

val sexp_of_ty : ('tr -> Sexp.t) -> ('tm -> Sexp.t) -> < e1 : 'tr; e2 : 'tm > ty -> Sexp.t

meaning that you'd have to write [%sexp_of: (int, string) ty] which might be confusing. Another possibility that works right now is to split the type in two:

type ('tr, 'tm) ty_repr =
  | C1 of 'tr * 'tm
  | C2 of 'tm * 'tr
[@@deriving sexp]

type 'a ty = ('tr, 'tm) ty_repr constraint 'a = < e1 : 'tr; e2: 'tm >

The advantage is that it's clear what refers to what when you write [%sexp_of: (int, string) ty_repr].

For objects, I don't see any problem, except that you have to be careful when your methods have side effects...

[ejgallego]

Hello Jérémie,

thanks a lot for your answer. Indeed your splitting proposal is what I manually did, but it was a bit painful given the size of the datatype.

By the way, this is the offending code I was trying to serialize in case you are interested: https://github.com/coq/coq/blob/trunk/intf/tacexpr.mli#L139

[v-gb]

For the first case, apart from what Jeremie suggested, what comes to mind would be using polymorphic variants instead:

type 'a ty =
  | C1 of 'tr * 'tm
  | C2 of 'tm * 'tr
constraint 'a = [ `e1 of 'tr | `e2 of 'tm ]
[@@deriving sexp]

This is still not supported by ppx_sexp_conv, but it looks plausible. The difference with what Jeremie was saying is that the generated functions would have the usual signature, so call sites look normal. Generated code would look like:

let sexp_of_ty sexp_of_'a = function
  | C1 (tr, tm) ->
    (match sexp_of_'a (`e1 tr), sexp_of_'a (`e2 tm) with
    | List [_; sexp1], List [_; sexp2] -> List (Atom "C1" :: sexp1 :: sexp2)
    | _ -> failwith "some error")
  | C2 .. -> ..

And [%sexp_of [e1 of int | e2 of float ] ty] should work fine.

I'm guessing that for ty2, you don't actually want to serialize an object, you just want to name the set of parameters of an other type? Something like this:

type 'a ty = .. constraint 'a = < e1 : ..; e2 : .. >
type ty2 = < e1 : int; e2 : string >
type ... = ty2 ty

? If so, this problem goes away with my proposal above.

I don't understand why you have definitions like ty3, when two type parameters can be collapsed.

[struktured]

Anyone working on this? Here's another example:

type 'a t  = [<`A|`B] as 'a [@@deriving sexp]

Error: Type unsupported for ppx [of_sexp] conversion

[aalekseyev]

I don't think anybody is working on it. Supporting constraints in general with no restrictions or annotations does not seem possible because of the problem Jeremie pointed out. I think the summary of the problem is that at type application there is no syntactic hint to detect that constraints are used (and what constraints are used). This information is necessary in general to pass the sexp conversion functions for the variables "bound" by the constraint.

A hack @sliquister suggested could work for constraints of a certain shape, but this has very surprising runtime behavior and the supported subset of constraints also seems surprising to me.

As it stands, I don't see a good way forward here.