Returning abstract types

Learning
1

Lets say I have some GADT t:

type _ t =
  | Str : string t
  | Int : int t

and I want to write a function that takes some identifier (we’ll use an int) and returns a corresponding value of t:

let f = function
  | 0 -> Some Str
  | 1 -> Some Int
  | _ -> None

The above function doesn’t compile for obvious reasons; the first branch concretizes the return type as string t. Fair enough, but using locally abstract types doesn’t work either:

let f (type a) : int -> a t option = function
  ...

This time the compiler complains that string and int are not equal to type a, which also makes sense.

This also doesn’t work with explicit polymorphism. The one case that I’ve found does work is when using first class modules:

module type Flat_t = sig
  type arg
  val v : arg t
end

let f = function
  | 0 -> Some (module struct type t = string let v = Str end)
  ...

This seems redundant to me as no extra information is added in the module.

I understand why this is the case – I’m just wondering if there’s a more elegant solution to this that doesn’t require the extra indirection of wrapping the values with modules.

1 Like
2

The type of f here is 'a. int -> 'a t option. 'a is a universally quantified type: The caller chooses what 'a, is, and the function must return an 'a t option. Therefore, the following definition is incorrect:

let f (type a) : int -> a t option = function
  | 0 -> Some Str
  | 1 -> Some Int
  | _ -> None

What happens if the caller writes f 0 : int t option? The caller has chosen 'a = int, but the function implementation mandates 'a = string. That’s why this definition is ill-typed.

From the point of view of the caller, 'a is a universal type, meaning the caller can choose anything. Therefore, from the point of view of the implementor, 'a is an existential type: It is a fixed arbitrary type, and the implementor can only work with the information about 'a that the caller has provided. The implementor cannot chose what 'a is.

What if the implementor wants to choose what 'a is? Here, 'a must be an existential type from the perspective of the caller and a universally quantified type from the perspective of the implementor. One should define the following:

type ex = E : 'a t -> ex

The type of E is similar to 'a. 'a t -> ex, except that in OCaml, constructors are not true functions. Here, 'a is a universally quantified type. Therefore, the following function can be typed:

let f = function
  | 0 -> Some (E Str)
  | 1 -> Some (E Int)
  | _ -> None

Then, from the perspective of the caller, which gets back an ex, the type 'a is existential: It is some fixed unknown type that is an argument to the E constructor.

Modules are another way to pack up existential types (or abstract types) together with some data. So, first-class modules are another way to express the function’s type, as you figured out.

5 Likes
3

What happens if the caller writes f 0 : int t option ? The caller has chosen 'a = int , but the function implementation mandates 'a = string . That’s why this definition is ill-typed.

While I agree with this, this is a type error even without abstract types. I guess the question here is what should the type argument to t be, which is why the module method works (the type is Returned_module.t). I didn’t consider this, which I guess is an answer to my question.

I thought about using a wrapper GADT as well, which is more elegant than the modules but still a bit less than I would like. Oh, well – it makes sense :slight_smile:.

Thanks!