When @O_Olivier started working on implementing algebraic datatypes and records, we realized that it was difficult to use the exist
combinator a dynamicallyknown number of times (for each element of a list, for example). We went into a few iterations to try to solve this issue, and we have a final proposal that we think makes it easier than the current API.
The current PR does not propose any change to the current API, but it exposes the problem by adding a simple clientlanguage feature that requires creating dynamicallymany inference variables: nary products, with Tuple ts
as an introduction form (surface syntax (t1, t2, ...)
), and LetProd(xs, ts, u)
as an elimination form (surface syntax let (x1, x2, ...) = (t1, t2 ..) in u
. The typeinference code for these two constructs is written in CPS style.
Remarks:

Prod(i,t)
is removed from the ML language, because this form does not allow principal type inference for nary tuples (the arity of the tuple is not forced by the syntax, and there is no aritypolymorphic getter type). Currently the branch offers bothProj
andLetProd
on the System F side, because both are easy to typecheck. (We could removeProj
if someone insisted.)  The inference rules for both constructs are written in a "generic" style, where the listtraversal functions take a continuation that expect the list of corresponding inference variables. We later found out that it is easier to write the code in a more "specialized" style where those traversals are specialized to the one continuation needed by the inference rule. Someone could instead argue that it's best to have the simplest possible code instead, and I would be happy to provide the simpler implementation if preferred.
For a concrete example of (2), the Tuple case currently reads as
begin
let rec traverse
(ts : ML.term list)
(k : variable list > 'a co)
: (F.nominal_term list * 'a) co =
match ts with
 [] >
map (fun r > ([], r)) @@
k []
 t::ts >
exist_ @@ fun v >
map (fun (t', (ts', r)) > (t'::ts', r)) @@
hastype t v ^&
traverse ts @@ fun vs >
k (v :: vs)
in
traverse ts @@ fun vs >
w  product vs
end <$$> fun (ts', ()) >
(* The System F term. *)
F.Tuple ts'
the nongeneric version, with the continuation inlined, reads as follows:
 ML.Tuple ts >
let rec loop (acc : variable list) = function
 t::ts >
exist_ @@ fun v >
hastype t v ^& loop (v :: acc) ts
<$$> fun (t', ts') > t'::ts'
 [] >
let vs = List.rev acc in
w  product vs ^^ pure []
in
loop [] ts
<$$> fun ts' > F.Tuple ts'
I don't find this specialized approach very natural or modular, but it does result in simpler code.