Given a variant, is it possible to write a type signature for a list of tuples of that variant where each pair must be the same specific variant?

Learning
1

So suppose I have a variant like:

type setting = B of bool | I of int

Then we can write a list of tuples, like:

let settings : (setting * setting) list = [(B true, B false); (I 3, I 4)]

However, the (setting * setting) list type signature allows you to write lists like:

[(B true, I 4); (I 3, B false)]

Is there any way to restrict this list so it only allows tuples of the same specific variant? Of course I can just define another variant specific to tuples, like:

type setting_tuple = BB of bool * bool | II of int * int

However, I want to make various further compound structures over setting so it would be nice to only have to define one variant.

2

This is one of the things you can do with GADTs:

type _ setting = B : bool -> bool setting | I : int -> int setting
type 'a setting_tuple = 'a setting * 'a setting

Then every value of 'a setting_tuple will either be of the form (B b1, B b2) or (I i1, I i2).

Cheers,
Nicolas

4 Likes
3

Thanks! One issue, when I write this code:

type _ setting = B : bool -> bool setting | I : int -> int setting

type 'a setting_tuple = 'a setting * 'a setting

let settings : 'a setting_tuple list = [
  (I 3, I 4);
  (B true, B false);
]

I get this error on the second element of the list:

This constructor has type bool setting but an expression was expected of type
int setting
Type bool is not compatible with type int

Why is that?

4

In short: (I 3, I 4) has type int setting_tuple and (B true, B false) has type bool setting_tuple and these two types are not compatible so they cannot be put in the same list.

You can use an existential “wrapper” to do that, though:

type tuple = T : 'a setting_tuple -> tuple
let settings : tuple list = [
  T (I 3, I 4);
  T (B true, B false);
]

Cheers,
Nicolas

5

A separate variant would be the sensible solution here yes.

What you’re really asking for is a way to construct several of these where the constructors contain some wrapper type around their actual arguments (currently a pair). You can express this with a module functor

module MakeSetting(Container : sig type 'a t end) = struct 
    type t =
         | B of bool Container.t
         | I of int Container.t
end

(* `PlainSetting.t` is exactly your `setting` type *)
module PlainSetting = MakeSetting(struct type 'a t = 'a end)

(* `PairSetting.t` is exactly your `setting_tuple` type *)
module PairSetting = MakeSetting(struct type 'a t = ('a * 'a) end)
1 Like