# What's a usage pattern for existential type variables?
**URL:** https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538
**Category:** Learning
**Tags:** type-system, existential-types
**Created:** [September 27, 2021, 5:16pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538 "2021-09-27T17:16:41Z")
**Posts on this page:** 7
**Page:** 1
### Author:  [@hyphenrf](https://discuss.ocaml.org/u/hyphenrf)
#### Post date: [September 27, 2021, 5:16pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/1 "2021-09-27T17:16:41Z")
Online, (Scala/Java) and Haskell-specific tutorials on existential types seem to be dominant. Because I wouldn’t get stuck too much on notation, I went with Haskell tutorials, and they all seem to imply that _existentials that are unconstrained are useless_.
The usual example for existentials is information (but not trait) hiding, in which for example you can have a definition like so (with some syntax parallels for those unfamiliar with haskell):
```nohighlight
{-
ocaml: `type gadt = Constr : typexpr`
haskell: `data Gadt where Constr :: typexpr`
-}
data Hidden where
Hide :: Show a => a -> Hidden
{-
ocaml: iter (fun (Hide x) -> ...) [Hide 1; Hide ...]
-}
main :: IO ()
main =
mapM_ (\(Hide x) -> print x) [Hide 1, Hide "a", Hide 4.2]
```
The problem with such implication is that I can’t find a usage for an existential introduced by an OCaml GADT because I don’t know how I’d express the `Show a => a` constraint.
```nohighlight
type hidden = Hide : 'a -> hidden
```
Would simply completely cloak `'a`, and any attempt at interacting with it would produce a type scope escaping error.
That considered, since `Show a => a` is best emulated now with passing a first-class module, that was the vector I was walking in with my existentials experiments, but I have a feeling there’s better, more valid, usage of those type variables that isn’t reliant on constraining.
So my question is, have you ever come across a pattern where an existential type variable is the solution?
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [September 27, 2021, 5:59pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/2 "2021-09-27T17:59:55Z")
Your showable example can be written as:
```ocaml
type showable = Show: 'a * ('a -> string) -> showable
```
And there is fact many similar way to constraint existential types, either using type constructors:
if you have an `'a. 'a t`, you may still be able to write useful functions, or coupling various producers or consumers of the existential types.
The `showable` example is a little artificial here but that are many examples where existential types are useful for:
- representing internal types.
- hiding some type information at an abstraction barrier.
I can offer one examples that combines the two to implement a zipper through mutually recursive trees.
Starting from a simplified data structure
```ocaml
type a_tree =
| Leaf of int
| Node_A of b_tree * b_tree
and b_tree =
| Leaf of float
| Node_B of a_tree * a_tree
```
Then zipper over a binary tree would be simply:
```ocaml
type dir = Left | Right
type zipper = { value: tree; path: (dir * tree) list }
```
but here our problem is that we have alternatively `a_tree` and `b_tree`. We can use existential types to keep a similar representation as the simpler zipper described above. The first step is to describe a step in the data structure as
```ocaml
type ('a,'b) step =
| A: dir * b_tree -> (b_tree,a_tree) step
| B: dir * a_tree -> (a_tree,b_tree) step
```
Then we can connect the step using an existential types to describe that if we have a path from
nodes of type `top` to a node of type `bottom`, we don’t necessarily know the intermediary types
```auto
type ('bottom,'top) path =
| []: ('top,'top) path
| (::):
('bottom , 'previous_bottom) step * ('previous_bottom,'top) path ->
('bottom,'top) path
```
Then a zipper is simply:
```ocaml
type ('bottom,'top) zipper = { value: 'bottom; path:('bottom,'top) path }
```
However, sometime we don’t care if we don’t know where we are in the tree, thus we may need to erase the `bottom` information from the zipper:
```ocaml
type 'top any_zipper = Any: ('bottom, 'top) zipper -> 'top any_zipper
```
and we can still use this `any_zipper` type to write an `up` function for instance:
```ocaml
let up (type top) (Any z: top any_zipper) =
match z.path with
| [] -> Any z
| A (Left,r) :: rest ->
Any { path=rest; value = Node_A(z.value,r) }
| B (Left,r) :: rest ->
Any { path=rest; value = Node_B(z.value,r) }
| A (Right,l) :: rest ->
Any { path=rest; value = Node_A(l, z.value) }
| B (Right,l) :: rest ->
Any { path=rest; value = Node_B(l, z.value) }
```
---
### Author:  [@hyphenrf](https://discuss.ocaml.org/u/hyphenrf)
#### Post date: [September 27, 2021, 6:28pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/3 "2021-09-27T18:28:20Z")
thanks for the detailed example ✨
gonna take my time to process it and wire the types together
---
### Author:  [@hyphenrf](https://discuss.ocaml.org/u/hyphenrf)
#### Post date: [September 27, 2021, 6:31pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/4 "2021-09-27T18:31:39Z")
> [@octachron](#):
>
> And there is fact many similar way to constraint existential types, either using type constructors:
> if you have an `'a. 'a t` , you may still be able to write useful functions, or coupling various producers or consumers of the existential types.
similar ways as in we put the type of the consumer right in the constructor, like you did with `showable`?
> [@octachron](#):
>
> if you have an `'a. 'a t` , you may still be able to write useful functions
like in a record?
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [September 27, 2021, 6:45pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/5 "2021-09-27T18:45:05Z")
Any time you have useful functions of type `'a. 'a t -> ..`, you can quantify existentially that type parameter and still retain some functionality. For instance, I can compute a length for an `any_list`:
```ocaml
type any_list = Any_list : 'a list -> any_list
let len (Any_list l) = List.length l
```
then there is also the possibility to use type witnesses to recover the quantified type at a later date:
```auto
type 'a num_ty =
| Int: int num
| Float: float num
type num = Num: 'a num_ty * 'a -> num
type num_array = Narray: 'a num_ty * 'a array -> num_array
let sum (Narray (witness, array)) = match witness with
| Int -> Num(Int, Array.fold_left (+) 0 array)
| Float -> Num(Float, Array.fold_left (+.) 0. array)
```
---
### Author:  [@jjb](https://discuss.ocaml.org/u/jjb)
#### Post date: [September 27, 2021, 8:20pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/6 "2021-09-27T20:20:36Z")
@octachron’s examples are very good. For variety, here is a small example of a slightly different flavor that we use in ocamlformat to wrap Cmdliner: (from [here](https://github.com/ocaml-ppx/ocamlformat/blob/main/vendor/ocamlformat-stdlib/cmdliner_ext.ml))
```ocaml
include Cmdliner
(** existential package of a Term and a setter for a ref to receive the
parsed value *)
type arg = Arg : 'a Term.t * ('a -> unit) -> arg
(** convert a list of arg packages to a term for the tuple of all the arg
terms, and apply it to a function that sets all the receiver refs *)
let tuple args =
let pair (Arg (trm_x, set_x)) (Arg (trm_y, set_y)) =
let trm_xy = Term.(const (fun a b -> (a, b)) $ trm_x $ trm_y) in
let set_xy (a, b) = set_x a ; set_y b in
Arg (trm_xy, set_xy)
in
let init = Arg (Term.const (), fun () -> ()) in
let (Arg (trm, set)) = Base.List.fold_right ~f:pair args ~init in
Term.app (Term.const set) trm
let args : arg list ref = ref []
let mk ~default arg =
let var = ref default in
let set x = var := x in
args := Arg (arg, set) :: !args ;
var
let parse info validate =
Term.eval (Term.(ret (const validate $ tuple !args)), info)
```
The idea here is similar to an “any list”, where an existential around a pair of an `'a Cmdliner.Term.t` representing a command-line argument yielding an `'a` value, and a function of type `'a -> unit` to set a ref to the parsed value. Then a list of such packages can be built using `mk` and then converted with `tuple` to a single `Cmdliner.Term` for the list as a tuple.
I don’t think this example needs anything more from the type system, but is an almost minimal example of packaging a value with the interesting operations over it into an existentially-typed value.
---
### Author:  [@orbitz](https://discuss.ocaml.org/u/orbitz)
#### Post date: [September 28, 2021, 12:18pm UTC](https://discuss.ocaml.org/t/whats-a-usage-pattern-for-existential-type-variables/8538/7 "2021-09-28T12:18:18Z")
I have made my own futures library and one of the features is futures are connected to each other creating a dependency tree. This is done so that you can do `Future.abort fut` and it will abort that future and everything connected to it. I accomplish this by each future storing a list of those futures that depend on it. But those futures do not necessarily have the same type. So I hide the type in an existential so I can still perform actions on the future that do not depend on the type.
Note, I stole this from @dbuenzli 's futures library which I used to start mine.
Here is the code from my library:
```ocaml
(* The concrete type of a future. Future's are mutable, but once they are
determined they become immutable. A future has a state which starts as
undetermined, can become determined or an alias. An alias is a future that
needs to exist because some unknown computation will eventually become its
value, and once that computation is found out, we set the future to an
alias to that future. *)
type 'a u = { mutable state : 'a state }
and 'a state =
[ 'a Abb_intf.Future.Set.t
| `Undet of 'a undet
| `Alias of 'a u
]
(* An undetermined has an optional function, which is some work to be
executed, watchers are executed when this undetermined future becomes
determined, deps are futures that are not required to be executed before
this future is determined but in some meaningful way connected to it, the
abort function is what to do if this future is aborted, and finally num_ops
is how many operations have been performed on this future. The definition
of an "operation" is kind of vague but basically it corresponds to mutating
this undetermined future in some way. *)
and 'a undet = {
mutable f : (State.t -> State.t) option;
mutable watchers : 'a Watcher.t list;
mutable deps : dep list;
abort : abort;
mutable num_ops : int;
}
(* A dependency can be any future and it will not have the same type as this
future, so we have to hide the actual type in an existential so we can
reference any future as a dependency. *)
and dep = Dep : 'a u -> dep
```