# Returning abstract types

**URL:** <https://discuss.ocaml.org/t/returning-abstract-types/11171>\
**Category:** Learning\
**Created:** [January 12, 2023, 10:30pm UTC](https://discuss.ocaml.org/t/returning-abstract-types/11171 "2023-01-12T22:30:22Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)\
**Post date:** [January 12, 2023, 10:30pm UTC](https://discuss.ocaml.org/t/returning-abstract-types/11171/1 "2023-01-12T22:30:22Z")

</div>

Lets say I have some GADT `t`:

```ocaml
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`:

```ocaml
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:

```ocaml
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:

```ocaml
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.

---

<div class="post-metadata">

**Author:** ![alan](https://avatars.discourse-cdn.com/v4/letter/a/a87d85/32.png) [@alan](https://discuss.ocaml.org/u/alan)\
**Post date:** [January 12, 2023, 11:04pm UTC](https://discuss.ocaml.org/t/returning-abstract-types/11171/2 "2023-01-12T23:04:07Z")

</div>

> [@zbaylin](#):
>
> `let f (type a) : int -> a t option = function`

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:

```auto
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:

```auto
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:

```auto
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.

---

<div class="post-metadata">

**Author:** ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)\
**Post date:** [January 12, 2023, 11:43pm UTC](https://discuss.ocaml.org/t/returning-abstract-types/11171/3 "2023-01-12T23:43:36Z")

</div>

> 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 🙂.

Thanks!