Consider the following definition of heterogeneous lists:
type 'a t = | ( :: ) : 'hd * 'tl t -> ('hd * 'tl) t |  : unit t
We get the following types:
let x : (int * (string * unit)) t = [ 1; "one" ]
This can get extremely ugly with very large lists
Ugly real life example from our codebase
type writable_columns = Timmy.Time.t Crud.Writable_column.optional * (Timmy.Week.t Crud.Writable_column.optional * (Timmy.Time.t Crud.Writable_column.optional * (Routine_schemas.Integration.Id.t Crud.Writable_column.optional * (string Crud.Writable_column.optional * (Schematic.Json.t Crud.Writable_column.optional * (Routine_schemas.Id.t Crud.Writable_column.optional * (Timmy.Date.t Crud.Writable_column.optional * (bool Crud.Writable_column.required * (Routine_schemas.Task_recurrent.Id.t Crud.Writable_column.optional * (Timmy.Date.t Crud.Writable_column.optional * (string Crud.Writable_column.required * (Uri.t Crud.Writable_column.optional * unit))))))))))))
Since the parameter of our GADT type is mute, we can make this much better by replacing
'hd * 'tl with
'hd -> 'tl; since
-> is right-associative, parentheses become useless and indentation much better:
type writable_columns = Timmy.Time.t Crud.Writable_column.optional -> Timmy.Week.t Crud.Writable_column.optional -> Timmy.Time.t Crud.Writable_column.optional -> Routine_schemas.Integration.Id.t Crud.Writable_column.optional -> string Crud.Writable_column.optional -> Schematic.Json.t Crud.Writable_column.optional -> Routine_schemas.Id.t Crud.Writable_column.optional -> Timmy.Date.t Crud.Writable_column.optional -> bool Crud.Writable_column.required -> Routine_schemas.Task_recurrent.Id.t Crud.Writable_column.optional -> Timmy.Date.t Crud.Writable_column.optional -> string Crud.Writable_column.required -> Uri.t Crud.Writable_column.optional -> unit
This works, however, as long as this type is indeed mute. We need to be able to convert these lists to nested pairs, for instance to feed them to caqti which understandably consumes nested pairs. With
'hd * 'tl this is straightforwad:
let rec to_pairs : type a. a t -> a = function | a :: b -> (a, to_pairs next b) |  -> () let _ : (int * (string * unit)) = to_pairs [ 1; "one" ]
'hd -> 'tl however, it seems much hairier to me. The best solution I could come up with introduces a witness type that essentially proves to the typer that both lists have the same length:
type (_, _) convert = | Cons : ('b, 'c) convert -> ('a -> 'b, 'a * 'c) convert | Null : (unit, unit) convert let rec to_pairs : type a b. (a, b) convert -> a t -> b = fun convert l -> match (convert, l) with | Cons next, a :: b -> (a, to_pairs next b) | Null,  -> ()
This however makes conversion to pairs more complex and quite redundant:
let _ : (int * (string * unit)) = to_pairs (Cons (Cons Null)) [ 1; "one" ]
This is hardly satisfying to me as the syntax issue was just shifted to
to_pairs, on top of having a runtime cost for something that is purely static. I’m under the impression there is no sound way to type this, which is quite frustrating since it looks purely syntactical.
One could argue that the simplest solution would be to just bite the bullets and accept this
'hd * 'tl nesting and not throw a fit for pure lexical reasons, but there are also cases where I would like to derive actual functions (à la Printf) from such lists, and thus have this problem the other way around.
Any insight appreciated !