How to convert a list to a product?

Learning
, ,
1

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.

2 
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
3

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
4

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.

5

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