


@ 0,0 +1,188 @@





ML 2020 Paper #62 Reviews and Comments





===========================================================================





Paper #62 Quantified Applicatives – API design for typeinference





constraints















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 Hindleystyle 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 abstractionlevel (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 subsolutions to obtain the desired





solution, e.g a typeannotated 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)





to





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 lightweight 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 constraintbased 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





metalanguage using the continuationpassing style, the resulting code





lacks readability and is errorprone since the places where the new





variables are introduced and where they are bound to the metalanguage





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





metalanguage 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 sidebyside





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 nary 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 "destinationpassing 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 unificationstyle as evaluation proceeds?
