Type of parameterized class is not bound within methods

Learning
, , , ,
1

Defining a local exception or module using the type of the parameterized class is not possible as the type is not bound. See this minimal example:

class ['a] foo =
  object
    method bar : unit =
      (* Neither of these definitions typecheck as 'a is unbound *)
      let exception Exc of 'a in
      let module M = struct type t = 'a end in
      ()
  end

I’ve found two solutions, both not satisfactory. The first is to wrap every function in an explicit (type a), i.e.

class ['a] foo =
  object
    method bar (x : 'a) : unit = (fun (type a) (x : a) ->
        let exception Exc of a in
        let module M = struct type t = a end in
        ()
      ) x
  end

Now we can create local exceptions with the correct type but every variable of type 'a must now be explicitly passed to the function and mutable fields of type 'a cannot be easily read/modified.

The other option (I’ve just thought of and not actually tried) is to wrap every class in a functor which defines the type t which is then used in the class. With this approach we loose basically any advantage of classes as every instantiation requires a functor of the correct type, inheritance becomes more difficult, syntactic overhead etc.

module F = functor (T : sig type t end) -> struct
  class foo =
    object
      method bar : unit =
        let exception Exc of T.t in
        let module M = struct type t = T.t end in
        ()
    end
end

Is there a way around this issue without large overhead? Is there a reason why 'a is not bound when defining exceptions/modules or is this an oversight of the compiler that could be fixed? It seems to me that this should be trivial to support but I guess there is a good reason for this behavior.

2

I don’t have a proper solution, but I am afraid that the first solution that you propose does not express what you want: the type a is abstract in the fun body and the only link between the two types a and 'a is that x is of type a inside the body and of type 'a outside of it. In particular, you will not be able to use in this function other fields or methods of foo with types mentioning 'a as if it was a. Another way to see that 'a and a are not linked is to notice that you can get rid of x and your definition still type-checks:

class ['a] foo =
  object
    method bar : unit = (fun (type a) ->
        let exception Exc of a in
        let module M = struct type t = a end in
        ()
      )
  end

I hope that someone will come with a better solution, but here is a way to express what you expect, I guess: instead of passing to the anonymous function a value x of type 'a, you can pass a witness that 'a and a are equal. Unfortunately, you cannot just destruct the witness (The type constructor a would escape its scope), but you can still use the witness to perform type conversions explicitly. In the following example, I use a Set module on elements of type a to remove the duplicate elements of a 'a list:

type ('a, 'b) eq = Refl : ('a, 'a) eq

class ['a] foo =
  object (self)
    val list = ([] : 'a list)

    method unique : 'a list = (fun (type a) (eq : ('a, a) eq) ->
      let module Set = Set.Make (struct
        type t = a
        let compare = compare
      end) in
      let cast_list (type a b) (Refl : (a, b) eq) : a list -> b list =
        Fun.id in
      Set.elements (Set.of_list (cast_list eq list))
    ) Refl
  end
2 Likes
3

Thanks for introducing me to the idea of type witnesses! I’m aware that my solution does not lead to 'a and a being unified which caused me some problems. Your solution does solve that problem although it is still a bit heavy in regards to syntax.

I hope someone comes along with either a simpler solution or an explanation why this roundabout approach with a witness is necessary. If not, your solution is still a big improvement so thanks for that.

4

Building on @thierry-martinez’s solution:

type (_, _) eq = Refl : ('a, 'a) eq
let right : type a b. (a, b) eq -> a -> b = fun Refl x -> x
let left  : type a b. (a, b) eq -> b -> a = fun Refl x -> x

class ['a] foo =
  object (self)
    method bar (x : 'a) =
      Refl |> fun (type b) eq ->
      let exception E of b in
      try raise (E (right eq x)) with E y -> self#qux (left eq y)

    method qux (x : 'a) = x
  end

It’s still a bit noisy as we have to cast in and out of the type b to use the exception, as we can never unify b with 'a without b escaping its scope. It’s perhaps more clear that Refl doesn’t cause this unification if you consider an alternative representation for left/right:

type ('a, 'b) iso = { right: 'a -> 'b; left: 'b -> 'a }
let refl = { right = (fun x -> x); left = (fun x -> x) }

Anyway, in case you don’t actually need b ~ 'a, here’s a lighter syntax for your first solution with a single required type annotation on the method (which you can extract in a class type):

class ['a] foo =
  object
    method bar : 'a -> 'a = fun (type b) x ->
      let exception E of b in
      try raise (E x) with E y -> y
  end
1 Like
5

A point to keep in mind is that the type parameters of a class are not rigid and can be implicitly constrained inside the body of the class. For instance,

class ['a] c (y:'a) = object
  val x = y
  method m = [] @ x
end

is a valid class where the type variable 'a is contrained to 'a = 'b list.
Classes can also have less type parameters than expected

class d  = object
  inherit ['a] c []
  method y = 1 :: x
end

Thus there is a significant gap between the behavior of the unification type variable like 'a and the behavior of locally abstract types.

2 Likes