You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

189 lines
7.5 KiB

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

ML 2020 Paper #62 Reviews and Comments
Paper #62 Quantified Applicatives API design for type-inference
Review #62A
Overall merit
4. Accept
Reviewer expertise
4. Expert
Paper summary
This paper analyzes properties and structure of a program representing
a type inference algorithm implemented with Pottier's declarative type
inference framework, points out some difficulties in writing code in
monadic style, and proposes a refinement of Pottier's Inferno API.
Comments for author
Different from Hindley-style type inference problem, which has a
simple inductive algorithm to compute a principal typing, a type
reconstruction problem for a language with Minler's polymorphic let
construct is notoriously difficult. A conventional algorithm
needs to keep track of solution substitutions and applying them each time
before obtaining a (partial) solution of a subterm. In practice, the
situation is more complicated due to the need of passing various
other attributes such as abstraction-level (lambda nesting level) for
efficiently representing the set of free type variables relative to
a partially computed type assignment.
Pottier presents a framework to improve this situation by defining
applicative combinators, and have developed Inferno library. Instead
of inductively reconstructing typed terms, the framework represents
a solution term as a pair (encoded as "T co" type constructor)
consisting of a constraint and a solution extraction function. This
achieves declaratively composing sub-solutions to obtain the desired
solution, e.g a type-annotated term.
The paper presents an informal description of the Pottier framework,
analyses the general program structure of a type reconstruction
algorithm, and discusses the problem of writing and reading those
program code. Although the Pottier framework allows to compose
solutions, the programmer needs to pass around solution extractors in
CPS style to obtain a final typed term at the end. This is the major
source of the difficulty in using Inferno. Based on these
observations, the paper proposes to refine a Infero "exisist"
combinator of the functionality:
exists : (var -> 'r co) -> (ty * 'r co)
exists : (var * (ty co) -> 'r co) -> 'r co.
where ty co represents the witness type to be obtained at the end of
computation. This regiment appears to be sound and also make sense.
Although the presented contribution is light-weight and does not
contain much significant new results, I find the proposal nice and
clean, and it would provide some programming insight to those who work
on type reconstruction or more generally some problem involving global
constraint solving. The paper is generally well written; I enjoyed
reading the discussion and analysis of problems of Inferno.
I therefore regard this as a possible contribution to the ML workshop.
Review #62B
Overall merit
5. Strong accept
Reviewer expertise
3. Knowledgeable
Paper summary
The paper provides an elegant solution for binding an arbitrary number
of scoped variables in a typed OCaml eDSL that has an applicative
structure. The solution is applied to Inferno, an OCaml library for
encoding constraint-based problems in the applicative style, but the
solution could be adopted by other projects, especially if they are
constrained by the applicative structure.
The problem that showcases the limitation of the current approach is
the inference/elaboration term that requires an arbitrary number of
inference variables. While it is possible to encode such a term in the
meta-language using the continuation-passing style, the resulting code
lacks readability and is error-prone since the places where the new
variables are introduced and where they are bound to the meta-language
variables are separated in code and do not have obvious connections.
The proposed solution is to provide an inference variable to the
scoped term, but make it modal to preserve the applicative structure
of the term. This enables binding of the inference variable to the
meta-language variable in the place of creation, albeit that the
inference variable is a packed term that has to be unpacked.
Comments for author
A very nicely put article that was a pleasure to read. A small caveat
is that you're using the binding operators for the proposed API
vs. monadic style for the old API. Not only it is a little bit unfair
for the old API, but it also makes it hard to perform the side-by-side
comparison, as we have to compare code that is written from left to
right with the code that is written from right to left. It would be
nice if they could be synchronized, by writing both in the same style.
To be honest, I am not really convinced that using binding operators
contributes to readability here, in fact, sticking to the old monadic
style, we can write something like this,
exists @@ fun v ty ->
traverse us @@ fun vs us' ->
k (v::vs,
hastype u v @@ fun u' ->
variable ty @@ fun ty ->
variable us' @@ fun us ->
(u',ty) :: us')
which will also enable us to uncurry the `exists` function, i.e., to
give it type,
(Infer.variable -> F.ty co -> r co) -> r co
Also, as a suggestion, the modal variable could be hidden by an extra
abstraction layer, e.g.,
type modal (* = Infer.variable co *)
val variable : modal -> (Infer.variable -> 'r co) -> 'r co
This will help with silly `let+ x = x` bindings and enable further
extensions of modal variables (e.g., for adding some static properties
to modal variables, which can be queried without unpacking it).
Review #62C
Overall merit
3. Weak accept
Reviewer expertise
3. Knowledgeable
Paper summary
This paper describes a new abstraction for the Inferno type inference
library. The Inferno library offers an applicative interface for
generating and solving constraints for type inference. The basic
primitives of the library include a function for creating fresh
existential variables which takes a callback to scope the
variable. However, while this API works for structural recursions over
the syntax tree, it is problematic when a list of evars must be
created (eg, for an n-ary tuple type). To support this, a new
interface with a `'a binder` modality is introduced, and some examples
of its use are given.
Comments for author
* Honestly, I found the proposal difficult to understand, since the
paper claimed that the `'a binder` type constructor was a modality,
but did not try to explain what kind of modality it was -- some
typing rules giving the judgemental forms for the `binder` modality,
and explaining when modal variables can be used or not would have
been very helpful to me. There were a few hints about this
* One thing this looked like was "destination-passing style" --
instead of returning an output, it looks like you are passing the
container into which an answer should be written. This makes me
wonder if some kind of linearity condition would be helpful. Or,
possibly, does the monotonicity of type inference mean that you want
multiple parts of the program to write into the same `'a co`,
updating it unification-style as evaluation proceeds?