A documentation comment for [letn].

This commit is contained in:
François Pottier 2022-04-06 21:20:09 +02:00
parent f308420fe3
commit 135246b6f7
1 changed files with 46 additions and 11 deletions

View File

@ -237,14 +237,14 @@ module Make
definition is equivalent to a copy of the constraint abstraction [c1].
The semantic value of this constraint is a tuple of:
- a list [vs] of decoded type variables that may appear in the semantic
- a list [αs] of decoded type variables that may appear in the semantic
value [v1] and therefore should be bound by the user in [v1].
For instance, if the user wishes to build an explicitly-typed
System F term as the result of the elaboration process,
then [v1] will be a System F term,
and the user should construct the abstraction [Λvs.v1],
and the user should construct the abstraction [Λαs.v1],
also a System F term.
The length of the list [vs] cannot be predicted.
The length of the list [αs] cannot be predicted.
The order of its elements is arbitrarily chosen by the solver.
- the decoded scheme assigned to [x] by the solver.
- the semantic value [v1] of the constraint [c1].
@ -255,18 +255,53 @@ module Make
(* c2: *) 'b co ->
(tyvar list * scheme * 'a * 'b) co
(**[letn] is a more general form of the combinator {!let1}. Like {!let1}, it
is a binary combinator: it has a left-hand side [c1] and a right-hand
side [c2]. However, whereas {!let1} binds one type variable [α] in [c1]
and constructs one scheme, which becomes bound to the variable [x] in
[c2], [letn] binds [n] type variables [αs] in [c1] and constructs [n]
schemes, which become bound to the variables [xs] in [c2].
The meaning of the constraint [letn xs c1 c2] can be described as follows.
Let [n] stand for the length of the list [xs].
Let [αs] be a list of fresh flexible variables, of the same length.
Let us write [xi] and [αi] for the [i]-th elements of the lists [xs]
and [αs].
Let us write [αs\αi] for the list [αs] deprived of [αi].
Then,
the constraint [letn xs c1 c2] is logically equivalent to
[let xi = λαi.(αs\αi).c1(αs) in c2].
That is, it is equivalent to the constraint [c2],
where each variable [xi] is bound to the
constraint abstraction [λαi.(αs\αi).c1(αs)].
This constraint abstraction has one parameter,
namely, the type variable [αi].
Every other type variable in the list [αs] is considered
existentially bound in this constraint abstraction.
The semantic value of this constraint is a tuple of:
- a list [αs] of decoded type variables that may appear in the semantic
value [v1] (see {!let1}).
- a list of decoded schemes, in correspondence with the list [xs].
- the semantic value [v1] of the constraint [c1].
- the semantic value [v2] of the constraint [c2].
The combinator [letn] is typically useful when performing type inference
for a construct such as ML's [let p = e1 in e2], where [p] is a pattern.
This construct performs Hindley-Milner generalization and binds several
variables at once, namely the variables defined by the pattern [p]. The
combinator [letn] allows performing generalization and constructing a
scheme for each of the variables defined by [p]. *)
val letn:
(* xs: *) tevar list ->
(* c1: *) (variable list -> 'a co) ->
(* c2: *) 'b co ->
(tyvar list * scheme list * 'a * 'b) co
(* [let0 c] has the same meaning as [c], but, like [let1], produces a list [vs]
of the type variables that may appear in the result of [c]. *)
val let0: 'a co -> (tyvar list * 'a) co
(* [letn xs c1 c2] binds [n] term variables [xs] to [n] constraint abstractions
in the constraint [c2]. Here, [c1] is a function of [n] fresh type variables
[vs] to a constraint. The [i]-th term variable, [x_i], ends up bound to the
constraint abstraction of the [i]-th type variable in [c_1], which one could
write [\lambda v_i.c_1]. *)
val letn: tevar list -> (variable list -> 'a co) -> 'b co ->
(tyvar list * scheme list * 'a * 'b) co
(* [letr1 alphas x (fun alphavs v -> c1) c2] binds the scheme variable [x]
to the constraint abstraction [fun v -> c1] in the contstraint [c2],
where [c1] is also abstracted over a list of rigid variables, one for