I've been looking at Hindley-Milner type inference for DL2. My initial expectation for DL2 was that macros could make it practical even without type inference. While it is possible to use DL2 without type inference, it wound up being untenable from a user perspective: >polymorphic functions require giving the whole type, including all polymorphic constructors >macros can only slightly help the previous issue, since they have to be included per-function >when using stack-recursive DL2, the looping mechanism requires detailing the type >complicated and verbose types do appear in practice >type abbreviations quickly become excessive The problem is that the general case of full type inference for System F-Omega and therefore for DL2 requires an undecidable form of higher-order unification. The designs of Standard ML and Haskell are strongly influenced by their commitments to their chosen type inference mechanisms. Given this issue, I can't help but think that I made the right choice in not specifying type inference as part of the design of DL2. My current plan for implementing DL2 type inference is to use unification that delays any reduction that it can't immediately resolve. This should yield a set of constraints that is agnostic to any higher-order unification strategy. When first-order unification can't resolve all type variables, it will produce an error message instead of attempting to synthesize an appropriate term. Limiting the terms that can be inferred by avoiding such term synthesis seems like the most reasonable trade-off given the general un-decidability of the problem. The expectation is that the desired type inference will almost never need a term that is synthesized. The Lambda Prolog paper attached seems to describe such an approach in its introduction, so I should probably read it closely.

>>13 Actually, I think I can get decent leverage out of regular first-order Hindley-Milner. If I work more on modules, I won't need existential products for things like type-classes, the result will only need ordinary unification and I can keep everything fast for the prototype. It's a half-solution but one that I know can be easily implemented and will leave things open enough to allow full higher-order type inference. Even in Haskell, most programs don't benefit from the full System F-Omega. If I want to have type-classes with ordinary Hindley-Milner, I can "manually" register the necessary existential products using a separate registry the same way Haskell does. I can use constraint unification to churn through type-class instances after the fact, attempting each appropriate member and backtracking on failure. This reduces the pressure to have "real" type-classes using DL2's existential products directly. Real existentials in the front-end can wait for now.

I was thinking about how to refer to the syntactic elements of DL2. For a while, I've been using "terms" ambiguously and referring to "value-level terms" in the working documentation, and that's confusing, since values already has a particular different meaning. Instead, I think I should use the following convention: - DL2 forms: the basic syntactic elements of DL2 - DL2 terms: a form which has a type, meaning it has a judgment "[: t]" for some type t - DL2 types: a form which has a kind, meaning it has a judgment "[:: k]" for some kind k - DL2 kinds: a form which is a kind, meaning it has the terminal judgment ":::" This cleanly suggests the "term : type : kind" concept, which is a very regular idea and therefore easy to remember. The word "form" is more neutral than "term", and has the connotation of "lexical" rather than "semantic", so is less confusing. This leaves "expression" out on its own. I think the best way to use "expression" is in contrast with "value", and to let them sit as independent of the other terms, with the only relation being that expressions and values are still assumed to be forms or be represented by forms. So in addition to the above conventions: - DL2 value: a closed, valid DL2 form which is normalized according to some appropriate definition of "value normalization", which is potentially specific to a particular DL2 system - DL2 expression: a closed, valid DL2 form, which may or may not be normalized according to "value normalization" This would then allow discussing "term values", "type values", "kind values" alongside "term expressions", "type expressions" and "kind expressions". An example of this usage would be this simple theorem, resulting immediately from the fact that there are no reduction rules for kinds: "All kind expressions are kind values." This also clears up the ugly notion of of "type constructors" common in the literature, by allowing the concept of "type expressions" as an alternative.

While working on DL2's first HM type inference, I wanted to put down some notes on bidirectional typing. Bidirectional typing is a system which combines type inference with type checking. Specifically, it augments type checking with rules for exactly when types can be synthesized or inferred. The hope is to get a simple implementation of type inference which matches the straight-forwardness of type checking. The attached paper goes into the theoretical reasons, but ignores some that might motivate implementers: >checker-inferencer's structure is easy to write and obvious: it is syntax-directed, like many functional programs, and can be written with the natural recursive structure >does not require unification for STLC inference >error messages can be reported exactly where they're discovered >as described below, "bare lambda" is "unlikely" to occur in the function position of an apply, so STLC inference will almost always succeed, requiring only the declarations of the types of each relevant constant The typical approach (according to the paper, "Pfenning Recipe"), is to have constructors check and to have constants, variables and destructors synthesize. In the specific case of "lambda" and "apply", this means that "lambda" is checked and "apply" synthesizes. This strategy then directs the rest of the rules. In the case of apply, synthesis requires that the function's type is synthesized, but once the function type is synthesized the argument only needs to be checked. The types of all variables are known up-front, since lambda can only ever be checked. There's an obvious issue with this approach: what do you do about instances of polymorphic constants? One of the most important uses of type inference in practice is to allow for using polymorphic constants without supplying types. The recipe described does not, on its own, allow for inferring the type arguments to a polymorphic constant, even when restricting to only prefix-polymorphic constants. It's necessary to re-introduce type variables and unification. Of course, once you have type variables and unification, you already have a major component of Hindley-Milner type inference (i.e. "the hard part"). At that point, the obvious question is: "why bother if HM does everything?" I'm a skeptic regarding the approach, but in relation to DL2 there are some interesting aspects. The work on bidirectional typing is a good hint as to what approaches are likely to work for practical type inference. Since DL2 is more similar to GHC's Core than Haskell itself, DL2 can accept many possible type inference mechanisms. Both bidirectional typing and unification-based inference bear similarities to logic programming without non-determinism or with limited non-determinism. Bidirectional typing tends to follow the hints of logic programming, specifically in suggesting that there are multiple modes of type-checking. At no point in the "original" bidirectional typing is it needed to have either non-determinism or unification, but modes from logic programming are still relevant. Meanwhile, unification-based inference takes complete expressions and uses only unification to derive the most general type. Bidirectional typing's error-checking utility is another reason why it's interesting from a DL2 perspective. The restricted format of bidirectional typing means that error-checking is guaranteed to involve local judgments, unless extended with unification. There may or may not be something to take there. When working on DL2's HM-based macro-expander, I thought about how to work with function application. It occurred to me that, if the macro-expander took an input "return type", then it would be possible to synthesize a non-polymorphic function type from just the arguments and without generating a new type variable. This made me think about bidirectional typing and find the above paper. This idea doesn't seem entirely distinct from bidirectional typing, especially the "simultaneous input and output" system described in the attached paper. DL2 macro-expanders also inherently suggest a requirement for locality, which is one of the strengths of bidirectional types. DL2 type-aware macro-expansion may be able to take advantage of incoming type information. It would be possible to supply variable types in binders for "match" and "case" without resorting to unification. The use of simultaneous input and output typing would allow for "un-satisfiable input type" errors, at least. Different type inference scenarios could have different specific macros. Type annotations could be used by users to direct macro behavior, even non-locally. The idea of such a "bi-HM" DL2 is more of a curiosity than an actual long-term plan. It might end up that its only utility is in eliminating unification, or there might be some obscenely clever technique that lets it provide high-quality errors. It might suggest a "combined meta-theory" of type inference that has little utility in practice. Some reasons to think this might not be useful: >should "checked apply" expand its arguments in a different order from "regular apply" just to avoid unification? >would abuse of type information make the system unpredictable at a user level? >could trying to be too clever with error messages make them worse in practice? >does knowing extra type information help much in practice? I'm half-considering trying a variant DL2 macro-expander and set of macros operating primarily according to Pfenning's recipe, and use it as a comparison point for error handling with other macro-expanders, although I'd have to find a decent set of "incorrect programs" to put different systems through their paces.

>>17 While working on DL2, I realized two very good arguments in favor of this "bi-HM" system. First, it can be used to supply binder argument judgments preemptively. This become apparent while working on case, but I believe this would also come up in pattern-matching. The issue was that the case argument types were computed separately from the non-case argument types. Second, when expanding some programs the type is known outright, and it's easier to just generate the code directly rather than rely on the call macro to do it. In this case, it's useful to have a helper variant of the expand function that lets the user supply the (sometimes-partial) type for unification after the fact. I noticed this while working on the DL2 C FFI, specifically for casting C arithmetic types to and from DL2's word type. I realized that most of my existing options weren't very good for that particular case, while immediate generation would be simple with only the option to supply the appropriate type to dl2-expand. Supplying this type directly is also simpler than generating the macro call for a type-check. In other words, I'm likely to end up with a variant of dl2-expand which does take the type directly. I also learned recently that Coq referred to its own type system as using "bidirectional typing" by name: https://rocq-prover.github.io/platform-docs/rocq_theory/explanation_bidirectionality_hints.html That said, it still seems silly in an HM context to use bidirectional typing as Coq's documentation implies. Type variables in HM means that every input type is a potential output type simply by providing a new variable. From this perspective, there's no difference between type inference and type checking. The whole implementation of bidirectional typing in an HM context is simply allowing an input type to be submitted. This also corresponds well with a logic programming interpretation of type-checking rules. The primary reason to separate input and output when using bidirectional typing with HM seems to be to avoid generating and unifying unnecessary type variables. I know that it's possible to optimize this generation and unification using HM-level matching, so that almost every form will have at most one type variable created for this purpose. In particular: >lambda generates at most one variable for each argument and at most one variable for the return and destructs its input variable >apply generates at most one variable for each argument and re-uses the input variable >constructors generate at most one variable for each argument and destruct the input variable >case generates one variable for the choose type, then destructs the result for input variables to each of its bindings, then re-uses the input variable for each of those I think that, in practice, it's likely to be a small overhead most of the time or may be significantly faster, due to unification being skipped by sharing variables rather than unifying them. This is in addition to the potential for better error-checking due to having type information readily available. Based on this, I think I can start recommending the bi-HM approach to type inference.