Packing GADT constructors in iterable data structure

Learning
1

Hi, I need to pack GADT constructors into some data structure that will allow me to search for specific item and iterate over all items.

Here’s the naive implementation which results in compile time error:

type _ t =
  | S: string t
  | I: int t

let items: type a. (a t * (a -> bool)) list = [
  (S, fun x  -> x = "");
  (I, fun x  -> x = 0);
]

Error:

This has type:
  string t
But somewhere wanted:
  a t

The incompatible parts:
  string
  vs
  a

I’m not tied to list, any iterable/searchable data structure will work.
Is this achievable with GADT?

1 Like
2

You can use a GADT to pack and “hide” the heterogeneous type (i.e., the type that differs between elements):

type _ t =
  | S : string t
  | I : int t

type packed = Pack : 'a t * ('a -> bool) -> packed

let items : packed list =
  [ Pack (S, fun x -> x = "")
  ; Pack (I, fun x -> x = 0)
  ]
;;

But the type declaration you wrote for items in your example means something like “for any type 'a, items is an 'a list”, which is only satisfied by the empty list.

3 Likes
3

@bcc32 Thanks for reply! AFAIU packed is existential wrapper, right? Using it, provided snippet compiles but it doesn’t allow me to do anything w/ wrapped contents, i.e. I can pack data but then no way to unpack it. So it seems it’s not possible to search for specific item, invoke function from tuple etc. Is this correct?

4

Yes, it is an existential wrapper. You would be able to invoke the function if you packed its argument into the GADT as well:

open Printf

type _ t =
  | S : string -> string t
  | I : int -> int t

type packed = Pack : 'a t * ('a -> bool) -> packed

let items : packed list = [ Pack (S "hi", fun x -> x = ""); Pack (I 1, fun x -> x = 0) ]

let () =
  match items |> List.exists (fun (Pack (x, f)) -> f x) with
  | true -> printf "found one\n"
  | false -> printf "nope\n"
;;

But, if you do anything to try to “unmask” the type hidden in that existential, it will fail to compile:

type _ t =
  | S : string t
  | I : int t

type packed = Pack : 'a t * ('a -> bool) -> packed

let items : packed list = [ Pack (S, fun x -> x = ""); Pack (I, fun x -> x = 0) ]

let _ =
  match List.hd items with
  | Pack (S, f) -> f
  | Pack (I, f) -> f
;;

This expression has type $Pack_'a1 -> bool
       but an expression was expected of type unit
2 Likes
5

So, if I have t constructor as input (e.g. S) and I want to search for the first (S, ...) tuple in the list, existential wrapper won’t allow it, correct?

If it’s correct, is there any other way to achieve it?

6

There are various methods of working with existential types. In the case of searching for the first S, string is a concrete type and so all you need is an annotation:

let rec first_s = function
  | [] -> None
  | Pack (S _ as s, f)::_ -> Some (s, (f : string -> bool))
  | _::rest -> first_s rest

It’s also possible to iterate over the contents of the packed. A function argument would usually leak the existential type and fail to compile, but we can avoid this by requiring the function to be polymorphic, which does not result in the type escaping:

type polymorphic_observe = {
  f : 'a. 'a t -> ('a -> bool) -> unit;
} [@@unboxed]

let iter f list =
  List.iter (function Pack (t, g) -> f.f t g) list

You can likewise define map, fold, etc. I find programming in this way to be clumsy and unpleasant, but it is possible.

4 Likes
7

Clumsy and unpleasant indeed. Thanks for the great explanation! I solved my problem by re-designing public API.

8

I cannot run the first snippet. The error message for f x shows

Error: This expression has type $Pack_'a t
but an expression was expected of type $Pack_'a

9

Yeah, it looks like I made a mistake. You’d want something like:

open Printf

type _ t =
  | S : string -> string t
  | I : int -> int t

type packed = Pack : 'a t * ('a -> bool) -> packed

let items : packed list = [ Pack (S "hi", fun x -> x = ""); Pack (I 1, fun x -> x = 0) ]

let () =
  match
    items
    |> List.exists (fun (Pack (x, f)) ->
      match x with
      | S x -> f x
      | I x -> f x)
  with
  | true -> printf "found one\n"
  | false -> printf "nope\n"
;;
1 Like