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 = [ (…

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) ] ;; Bu…

@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 tupl…

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…

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?

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 I…

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

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 …

Packing GADT constructors in iterable data structure

Learning

alexfedoseev October 10, 2018, 10:36am 7

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

Topic		Replies	Views
"Parsing" terms into a well-typed representation: a GADT puzzle Learning gadt	4	2680	October 30, 2021
[GADT] iterate over heterogeneous list Learning	4	394	October 17, 2024
Type of function returning GADT Learning gadt	2	946	May 20, 2020
Tutorial on GADTs Learning blog , gadt , tutorial	28	4073	October 12, 2025
Heterogeneous list using GADTs? Learning	1	1410	July 8, 2019

Packing GADT constructors in iterable data structure

Related topics