Forward type definitions

notes/meetings/2019-09-05/notes.txt

@@ -0,0 +1,122 @@
+Gabriel: my main proposal is, for the "rebuild the type-checker from
+scratch" part, to create a repository on top of Inferno¹ that
+implements a ML language (MidML, MoyenML?). We start from the nano-ML
+example used in Inferno itself (as a typical example of Inferno client
+program). We add important features from the OCaml type system, one
+after the other, which requires adding new features to Inferno
+itself -- as clear and general as possible to express the desired ML
+type-inference features. This is useful to get a clean theory (of the
+ML feature, of the inference support for it), looking at interactions
+with other features, with a reference implementation that keeps
+growing. And for some of those features we can publish papers.
+
+The notes below include at the end a list of features to which we
+could think of during the discussion -- a decomposition of OCaml's
+type system in smaller.
+
+¹ Inferno is François Pottier's type-inference library. I (Gabriel)
+would recommend reading its implementation -- I did it from the
+high-level layers to the low-level layers. It is hosted on François's
+favorite open-source closed-development platform:
+https://gitlab.inria.fr/fpottier/inferno .
+
+----
+
+# Global approach
+
+We should do "incremental" and "from scratch" ("big bang") in
+parallel, with communication between both.
+
+
+Incrémental
+
+- Start from the TODO list and Thomas' and Leo's ideas
+
+  Jacques: I'm less interested in that part.
+
+  Gabriel: but we will ask you to review what people have done.
+
+  Jacques: I was mostly speaking of the refactoring. Conceptual
+  changes (like adding scopes) are more interesting to me.
+
+  Gabriel: I think sometimes conceptual changes emerge
+  from refactoring, when done carefully.
+
+
+Big-bang
+
+- Use Inferno + MoyenML as an experimental vehicle to study the essence
+  of OCaml type-system features, layer by layer.
+
+  How to bridge the gap between MoyenML-gone-big and OCaml? One
+  possibly, if required (it's not pretty), would be to replace the
+  lowest layers of Inferno (Union-Find, levels/generalization etc.) by
+  the OCaml type representation and its manipulation code
+  (atype/btype/ctype).
+
+  (Didier: the interface of Inferno is nice, but in the implementation
+  I'm not convinced by the very-effectful approach of François. Maybe
+  we don't want that on the long term, it may not scale to more
+  advanced constraints.)
+
+Core language: what's an explicitly-typed representation that the
+OCaml type-inference engine could produce as result?
+
+  Jacques: about that, I was thinking of using CIC (Calculus of
+  Inductive Constructions), to represent the values of OCaml's
+  intermediate representation with dependent types. -- use Gallina as
+  intermediate representation.
+
+
+## Feature map to add to Inferno + MidML
+
+### Term language
+
+- [data]: algebraic datatypes
+  + pattern-matching
+
+- type abbreviations
+
+- label overloading (constructors and fields)
+  (depends on [data])
+
+  Gabriel: http://gallium.inria.fr/~scherer/topics/delayed-constraints-for-disambiguation.txt
+
+- scoped type variables
+
+- first-class polymorphism
+
+- GADTs
+  (depends on [data])
+
+- structural rows
+  (objects, polymorphic variants)
+
+- checking .mli
+  (the inclusion check between type declarations)
+
+- value restriction?
+  + partial generalization
+  + relaxed value restriction (variance)
+
+### Error report (entry later added by DR)
+
+- minimal error report needed
+
+- explore other solutions
+  + Nathanael proposal: report unification errors in terms of typing
+    constraints from the soruce. 
+
+### Propagation of source typing annotations (later added by DR)
+
+- Preprocessing step?
+
+- During constraint generation?
+
+- Other: new form of constraints? 
+
+### Modules
+
+- modules
+- first-class modules
+

notes/meetings/2019-09-16/notes.txt

@@ -0,0 +1,60 @@
+Discussion of the "high road" (Xavier's term):
+* rebuilding something like OCaml (possibly simpler, cleaner)
+  from scratch, starting from Inferno.
+
+Discussion of the "low road":
+* refactoring the existing type-checker
+* problem: the reviewing load will be high (especially for Jacques)
+* Jacques says it's ok to discuss the high-level ideas,
+  but painful/impossible to review the code itself
+* Xavier wants discussion on high-level ideas, more than one the code
+
+Didier asks whether the two roads are supposed to meet eventually.
+
+Jacques says that Thomas Refis is the one who is currently working most
+on the "low road" (the type-checker). E.g. Thomas has clarified the notion
+of "scope", etc. Also, Leo White has done some work on the type-checking
+of objects and classes (not yet reviewed and merged; it was discussed in
+March 2019 but the requested follow-up work was not done).
+
+François asks whether it would be worthwhile to work on strengthening
+the test suite.
+* Xavier mentions fuzzing;
+  it could be very useful if the type-checker contains assertions
+* Florian & Sébastien had an Outreachy intern (Oxana)
+  who worked on checking the coverage of the test suite.
+  It would be good to continue and finalize this work.
+  (Gabriel had an Outreachy intern (Ulugbek) working on quickchecking
+   the compiler by randomly generating well-typed programs. Could also
+   be of interest.)
+
+Didier asks whether the code should be commented (either inside the code,
+or in a separate file containing explanations). Damien notes that some PRs
+begin with a long explanation. But it is not visible in a cloned repository!
+
+Sébastien asks where we should invest our energy and expertise. (Who should
+work on what?) E.g. Sébastien might be interested in working on refactoring
+the type-checker.
+
+What are our forces?
+* Gabriel Radanne
+* Leo White?
+* Thomas Refis??? (will be doing a PhD with Didier, hence *scientific work*)
+* Sébastien could have some time after March 2020
+
+Someone mentions the technology that allows rapidly rebuilding all opam packages so as to test a change. Do we master it? Florian knows about "opam-check" (Damien's tool); works, but not yet parallel. (It should be!)  Armaël & Gabriel have worked on another approach (also on top of opam) which is parallel. Still experimental, to be finished. And what about the OCaml Labs tools? Damien notes that many opam packages have broken dependencies, which complicates things. (Would it be easy to automatically check that no dependencies are missing in a package description?) (Damien notes that it would be useful to know which modules are installed by which packages.)
+
+Didier asks to what extent it is permitted to change the type system (intentionally). E.g. we might wish to change the treatment of first-class polymorphism. (Didier has the "high road" in mind.) There seems to be
+consensus that in the high road it is permitted & desirable to do so.
+
+Some discussion of -principal, which is needed to infer principal types in the presence of first-class polymorphism, but is costly because it imposes copying instead of sharing.
+
+Sébastien notes the need to organize another meeting, including developers outside Inria, and to keep everyone in the loop. Need to do so soon, and decide (during that meeting) who will be working on each road.
+
+Some discussion of the idea of introducing one or more explicitly-typed intermediate languages. (Integrate the work by Pierrick Couderc?) It or they should be easy to type-check; the code of the checker should be close to a declarative specification. Jacques would like this language to be formally defined in Coq. Armaël notes that one could even have a type-checker for it implemented in Coq. (Analogous to what the F* people did?) Jacques and Xavier would like to do a proof of type soundness (preferably for a low-level calculus). A model of OCaml types in Iris could be interesting. Xavier wants types to have meaning. (This is the "high high road".)
+
+TODO:
+  Send a proposal for an open meeting.
+  Scheduled together with a regular developers meeting?
+  (Include Pierrick + Gabriel.)
+  Propose a 2-day meeting. Starting late, finishing early. Research + dev.

notes/meetings/2019-10-07/inferno-roadmap.txt

@@ -0,0 +1,127 @@
+An Inferno roadmap (also known as "the high road").
+I will also commit a version of this to the Inferno repository.
+-- FP
+
+### Universal quantification in constraints
+
+### Type annotations
+
+This includes "scoped type variables", that is, the ability (or necessity?)
+to explicitly bind type variables.
+
+It should be possible to bind a type variable either existentially or universally.
+
+As a side product, we get the ability of comparing an inferred type
+with a declared type.
+
+### Algebraic data types and pattern-matching
+
+### GADTs
+
+Need to reason under local equations between types.
+Need to detect ambivalent types.
+In the presence of modules and abstract types,
+  need a notion of "compatibility" (an approximation of equality).
+
+### Type abbreviations
+
+Toplevel or local?
+Recursive?
+The subject of Carine Morel's recent internship.
+
+### Principality, sharing
+
+Understand how type information is shared internally and is propagated.
+Related to GADTs, first-class polymorphism, type abbreviations.
+
+### Propagation of type information (synchronization)
+
+Can it be viewed as a preprocessing step?
+Can it be performed at the same time as constraint generation?
+Do we need new forms of constraints?
+  (somehow allowing feedback from constraint resolution
+   into constraint generation)
+What is the role of type annotations in this setting?
+
+### Overloading of data constructors and field labels
+
+See Gabriel's proposal:
+  http://gallium.inria.fr/~scherer/topics/delayed-constraints-for-disambiguation.txt
+Related to implicit arguments.
+Related to name resolution.
+Related to synchronization.
+
+### Name resolution
+
+Make it easier for tools (smart editor, refactoring tool)
+  to understand the binding structure of the code.
+
+### First-class polymorphism
+
+For records and objects. Do we want to redesign this feature?
+  Can we avoid the syntactic overhead of boxing them in a record?
+
+### Rows
+
+With applications to objects and polymorphic variants and effects.
+  (Currently, objects and variants use local constraints.)
+
+### Core language subtyping
+
+Implicit, explicit, what form?
+  Are coercions erased? (yes)
+Related to rows.
+
+Implicit (pervasive) subtyping would require bi-unification (Stephen's algorithm).
+
+### Value restriction
+
+The relaxed value restriction, based on variance.
+Also, see Jacques's more recent proposal?
+
+### Basic support for linear types, regions, borrows
+
+Based on recent work by Gabriel Radanne and Peter Thiemann.
+
+### Type error reports
+
+Can we produce error reports that are minimal in a certain sense?
+  What is the algorithmic cost?
+
+Can we report multiple errors?
+
+### Incrementality, type-inferencer API
+
+Can we support incremental type inference?
+Can we avoid global state in the implementation?
+  or avoid side effects altogether?
+Should we expose an abstract type of type-inferencer states?
+Recomputing as little as possible when the source code changes.
+
+The "toplevel" (REPL) interface. The debugger.
+  How do they interact with the type-checker?
+
+### Modules
+
+Including first-class modules.
+Should the module language and the core language be separate?
+
+### Implicit arguments
+
+### Labeled and optional arguments
+
+Needs a form of multi-application.
+Related to synchronization (propagation).
+
+### Classes
+
+What kind of support does this require in Inferno?
+
+### Kinds
+
+Do we need some kind of support for kinds?
+How would it impact the solver's API?
+Type application in the syntax of kinds?
+  How are equations between type applications solved?
+Subkinding?
+Should type variables and type constructors be a single category?

notes/meetings/2019-10-07/low-road-notes.txt

@@ -0,0 +1,31 @@
+Gabriel Radanne will start doing more code reviews now.
+
+Reviews: hmm.
+
+  It would be nice if all Inferno-working people could help on code
+  reviews, not only within their subgroups.
+
+ (the idea of in-person presentations for big PRs: Leo is not in
+ favor, unconvinced by the idea of travelling to Paris so often (too
+ many big PRs?))
+
+Low road: the point is that making the code easier to understand
+  is a compiler-distribution feature by itself.
+
+Leo: larger rewrites should get RFCs just as big high-road features.
+
+Testing?
+  - Leo: Jane Street will keep building a branch of their codebase in trunk
+  - opamcheck: if we suspect there is a regression risk, we try to convince
+    Florian to run opamcheck on it
+
+High-road testing? Can we collect important examples of tricky OCaml
+code that relies on sharing in deep ways?
+
+Pierre Chambart: if we had a shared typed IR it would be easier for testing.
+
+Testing: collect examples of things that do not work in the testsuite,
+corresponding to known defects. "known-to-break" testsuite directory?
+
+  Policy: Everytime there is a new bug report with a small repro-test,
+  it should go into this known-defects directory.