parametric GADT from the outside

Question

GADT allows some form of dynamic typing:

type _ gadt =
  | Int: int -> int gadt
  | Float: float -> float gadt

let f: type a. a gadt -> a = function
  | Int x -> x + 1
  | Float x -> x +. 1.

I'd like to be able to do the same kind of dispatch, but with a parametrized type, with the parameter of the gadt accessible from the outside. If the parameter is universally quantified, or fixed, this is easy:

type (_,_) container = 
  | List: 'a list -> ('a,'a list) container

let f : type a b. (a,b) container -> b = fun (List l) -> l
let g : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l
let h : type b. (int, b) container -> b = fun (List l) ->  1::l

However if there are other form of constraints on the parameter this does not work:

class ['a] ko (x:'a) = object 
    method m : type b. ('a, b) container -> b = fun (List l) -> x::l
end

I get the error: The type constructor a#0 would escape its scope. I guess this is due to outside-in restriction, without fully understanding the domain.

The only solution I found was to use Higher module:

open Higher
module Higher_List = Newtype1 (struct type 'a t = 'a list end)
type ('a,_) container = List: 'a list -> ('a, Higher_List.t) container

class ['a] c (x:'a) = object
    method m : type b. b container -> ('a,b) app = fun (List l) -> Higher_List.inj(x::l)
end

This solution is far from being perfect however: first it is verbose, with inj and prj everywhere, and more importantly, it have a lot of limitation: the 'a parameter can't have constraints, nor variance...

Is anyone aware of a better solution ?

Edit

After some thinking, Drup solution is working, but it must be taken with care ! In my full problem (not the toy program in this question) I need to have access to self in the method definition. So going back to Drup solution, I must pass self to the intermediate function, and to do so, I must give it a type. So I must first declare a class type...

class type ['a] c_type = object
    method m: ('a, 'b) container -> 'b
end

let cons : type a b. a c_type -> a -> (a,b) container  -> b =
    fun self x (List l) -> x::l

class ['a] c (x:'a) = object(self: 'a #c_type)
    method m = cons (self :> 'a c_type) x
end

This won't work however if class c have a constraint on 'a: the type of cons won't be valid, as amust be universally quantified but have a contraint in a c_type. The solution is to write c_type without the constraint on 'a. Note however that this means a lot of rewriting. In many cases, just omitting the constraint is not sufficient to make it disappear: all of its usage must be unconstraint...

So the final solution looks like:

type (_,_) container = 
  | List: 'a list -> ('a,'a list) container

class type ['a] c_type = object
    (* no constraint on 'a, and take care of its usage ! *)
    method m: ('a, 'b) container -> 'b
end

let cons : type a b. a c_type -> a -> (a,b) container  -> b =
    fun self x (List l) -> x::l (* in real code, self is used... *)

class ['a] c (x:'a) = object(self: 'a #c_type)
    constraint 'a = < .. > (* well just for the example *)
    method m = cons (self :> 'a c_type) x
end

Answer 1

Why try complicated when you can do simple ? :)

type (_,_) container =
  | List: 'a list -> ('a,'a list) container

let cons : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l

class ['a] ko (x:'a) = object
    method m : type b. ('a, b) container -> b = cons x
end

This kind of constructions are tricky, since the placement of the locally abstract type is important. In your case, you would like a locally abstract type at the outer layer of the class (for the type a) which is not possible. Making an intermediate, properly abstracted, function usually helps.

Also, do not use higher. It's a proof that you can encode HKT in the module system, not an encouragement to actually do it.