# How to convert a list to a product?

Given a type witness and the description view of the product type, how to convert from a list of index-free type witness to a product type description?

Here are the details. An indexed type witness is given by the GADT:

``````type _ ty = | Int : int ty
| Bool : bool ty
| List : 'a ty -> 'a list ty
``````

Index-free type witness is given by the GADT:

``````type ty' = E : 'a ty -> ty'
``````

And the type description view of product types is given by the GADT

``````type _ product = | Nil : unit product
| Cons : 'a ty * 'b product -> ('a * 'b) product
``````

How to convert from the type `ty' list` to the type `'b product` ? For example, the list:

``````[E Int ; E Bool ; E (List Int) ]
: ty' list
``````

shall be converted to

``````Cons(Int, Cons(Bool, Cons(List Int, Nil)))
: (int * (bool * (int list * unit))) product
``````

I wrote the first function

`````` let of_list : 'b . ty' list -> 'b product =
function | [] -> Nil
| E h :: t -> Cons(h, of_list t)
``````

and the second function

`````` let of_list : type b . ty' list -> b product =
function | [] -> Nil
| E h :: t -> Cons(h, of_list t)
``````

but in both cases there are type clashes at the return type.

I can see that in the first function `'b product` is specialized to `unit product` by the first branch of pattern matching, and it clashed with the inferred type `('a * 'b) product` of `Cons(h, of_list t)` in the second branch of pattern matching. In the second function I expect the type checker to learn the type equation `b = unit` from the first branch of pattern matching but it doesn’t.

``````let of_list : 'b . ty' list -> 'b product
``````

This type reads “for all type `'b`, given a list of things, return a `'b` product”. Since nothing is constraining the type `'b`, you could unify the result with anything: `(of_list [E Int] : string product)` … which is clearly not possible.

What you actually want to formulate is “given a list of things, there exists a `'b` giving you a `'b` product”. Once you have the right type, the function should be easy to write!

2 Likes

There is two issues there.

First, in the type `ty' -> 'b product` the type `'b` is universally quantified, which is not a valid type. One can check that point with:

``````type empty = |
type impossible = { product: 'a. 'a product }
let impossible_implies_false: impossible -> empty =
fun {product} ->
match (product:char product) with
| _ -> .
``````

Thus the type `ty' -> 'b product` is not the type that you had in mind.

This leads us to the second issue, the type that you are thinking for your function would be something akin to:

``````let of_list (l:ty' list) : product_type(l) = ...
``````

Indeed the type of the returned product depends on the value of `ty' list`. In other words, as written
`of_list` is dependently typed. And, since OCaml is not dependently-typed language, such function cannot be written.

However, it is possible to achieve something similar to what you wanted, if one adds an existential quantification on the return type:

``````
type dyn_product = Dyn: _ product -> dyn_product

let rec of_list: ty' list -> dyn_product = function
| [] -> Dyn Nil
| E a :: q ->
let Dyn q = of_list q in
Dyn (Cons(a,q))
``````
2 Likes

It seems that GADT type variables may have context-sensitive quantification.

Consider the type variable `'a` in

`````` type dyn_t = Dyn : 'a product -> dyn_t
``````

In expression context `'a` is universally quantified, and in pattern context it is existentially quantified.

In expression context, the constructor `Dyn` has type `forall 'a . 'a t -> dyn_t`, meaning that
it can be applied to any value whose type has the form `_ t`, and the result has type `dyn_t`. Here `'a` is universally quantified.

However, when pattern matching againt values of type `dyn_t`, we know that the value has constructor `Dyn` and there exist a type `t` such that `Dyn` is applied to a value of type `t product`. That is, the type `t` is existentially quantified.

Go back to the function

``````let rec of_list : ty' list -> dyn_t =
function | [] -> Dyn Nil
| E h :: t ->
let Dyn tl = of_list t in
Dyn (Cons(h, tl))
``````

In the `E h :: t` branch of pattern matching, the pattern variable `t` is inferred to have type `ty' list`, and `E h` has type `ty'`, and further the pattern variable `h` is inferred to have type `exist a . a ty`. Actually, a fresh locally abstract type `a` is generated and `h` is given the type `a ty`. Then, when typing the right hand side, `of_list t` has type `dyn_t`, and the pattern matching in the let-binding gives the pattern variable `tl` the type `b product` for some fresh locally abstract type `b`, meaning `exist b . (tl : b product)`. Then `Cons(h, tl)` has type `(a * b) product` and the return type is dyn_t due to universal quantification in expression context. The function type checks and is accepted.

The limitation of this approach is that we cannot extract the argument of `Dyn`. For example, executing the top-level command

``````let Dyn va = of_list [E Int; E Bool; E (List Int)];;
``````

we get an error message saying that "existential types are not allowed in top-level bindings. "
Perhaps here we have reached the dependent type limitation of OCaml which cannot be overcome without any dynamic typing technique.

Note that since we have type witness, it is possible to extract the argument of `dyn`, if it is the user that provides the type information:

``````type ('a,'b) eq = Refl: ('a,'a) eq
let rec eq: type a b. a ty -> b ty -> (a,b) eq option = fun x y ->
match x, y with
| Int, Int -> Some Refl
| Bool, Bool -> Some Refl
| List  x, List y ->
begin match eq x y with
| None -> None
| Some Refl -> Some Refl
end
| _ -> None

let extract_ty (type a b) (ty:a ty) (x:b product): a ty option =
match x with
| Nil -> None
| Cons(a, _) ->
match eq a ty with
| Some Refl -> Some a
| None -> None

let extract_ty' ty (Dyn x) = extract_ty ty x
``````
2 Likes