Type Inference for Sound and Complete Flow Typing

[utterances-bot]

Type Inference for Sound and Complete Flow Typing

We design a type inference algorithm for the FT calculus of &qout;Sound and Complete Flow Typing with Unions, Intersections, and Negations&qout; (Pearce 2012), proving that it infers minimal types where they are expressible and infers all minimal user-typable types.

https://ayazhafiz.com/articles/21/type-inference-for-flow-typing

[ayazhafiz]

Lemma 2 is a bit tricky. At the time of writing I had done these proofs by hand, but it would be good to formalize them as Coq (or similar) artifacts. If anyone does this, and/or spots any problem, please let me know.

[metaleap]

Reading the 2012 flow-typing paper currently, in order to go through your inferencer outlined here afterwards. This remark-in-passing on page 5 already has me baffled:

recursive function calls cannot be typed as f is not included when typing t2 — however,
this is of little relevance to the problem being addressed

Is there some standard "de-recursion" rewriting mechanism implicitly being assumed, that one would have to apply as one constructs a flow-calculus / FT "AST" from one's own language's IR / AST?

Ctrl+F "recurs" brings up no further discussion or remarks on this.

[ayazhafiz]

@metaleap I believe that statement is saying that given an expression of form f(T1 x)= t2 in t3, the typing rule T-Dec solves the type of t2 without f in the environment, so f cannot be used recursively. If you want f to be recursive, it can be introduced in the environment before solving t2 as an unbound type variable.

[metaleap]

You're probably right that that's what was meant. Merci! Will report how it goes when I get there =)

[metaleap]

What really confounds me about all this flow-typing stuff I've found on "Whiley" and by Pearce, ranging from 2011-2018, is that the otherwise perfectly complete type system of never,any,tuple,int,or,and,not has no notion of a function type and never mentions closures. I guess it took me too long to notice.. too bad, deal breaker for my purposes..

"Why don't more languages use flow-typing?" — here's another answer for your existing blog post with that title. 😁 how would one adopt this for a dynamic language with a Scheme-like core and aiming for "full inference, zero annotations" (script-lang like)? I keep pondering this and am not yet currently seeing it.

Know of any good papers tackling this? With function types, annotation-free full inference, the full never,any,and,or,not gamut and flow-driven sub-typing eg. in type-testing/-casing consequents (which is where the intersection / negation types find a purpose afaict =). Or am I looking for The Holy Grail inadvertently and the field isn't there yet? Coming at this from a lang-dev impulse rather than a pure research&study impetus tbh..

[ayazhafiz]

I believe function types are not too hard to extend if you have the rest of the type system... function types behave like other types, except that the input argument is contravariant in the subtype relation and covariant in the return type.

I'm not sure of papers that describe exactly what you're looking for. In general full type inference with all of those characteristics may impossible, because the semi-unification problem (i.e. a system of inequalities { a<=b, ..., y<=z }) is undecidable in general. So you would always have to build a theory that restricts to a system of unifications that is decidable.

You may be interested in set-theoretic types, specifically the work of Castagna. https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf is a good introduction.

If you describe in a bit more detail your requirements I may be able to provide some more suggestion. Feel free to also email me.

[metaleap]

Hey many thanks, will be looking into that paper next!

If you describe in a bit more detail your requirements I may be able to provide some more suggestion.

Hm if you're curious, glad to elaborate a bit =) say one has a "dynamic language core", essentially a not-standards-conforming Lisp/Scheme-like (with a non-Lisp surface syntax, but that's irrelevant) and wants to have "static-like typing" inferred at least like TypeScript manages for even unannotated JS (TS being however based seemingly on not some calculus and a paper but accumulated-over-time ad-hoc analyses that defy formalization — for one like me certainly), mostly for IDE purposes (and any future transpilation/compilation purposes) and without requiring (or even ever supporting) any type annotations — implying only structural, not nominal, types. (And fully ignoring userland concoctions like Lisp's CLOS, "defstruct" macros and such.)

What would have to be inferred? Atomic prim types (int/float/string), lists (where a heterogenic one would amount to a unioned elem type I guess) which then trivially also covers tuples/records/dicts as simple adaptations, func types incl. the usual parametric polymorphism / generics scenarios (\x.x), and of course the typing of vars themselves (ie the params, globals and locals). Plus cond branches can return differently-typed results where you may have a union of those result types at the join point (the cont after the cond) but more specific types inferred for inside-each-branch's-consequent for conds that are (or imply) type-tests. Plus you have mutation. Here ideally the "latest" mutation decides a most specific type "until" the "next" mutation of that var, rather than all existing mutations of a variable combining into an always-current broader union type for it that'd have to be destructured before use — if feasible (kinda where I see the flow analysis stuff coming in).

Would be interested if any other papers/approaches come to mind. Already dug into various "retrofitted type systems for" [JS|Python|Ruby] but there's always a snag, either type annotations required partially or fully, local-only inference, no lambdas, no mutations... never the complete package as far as I have found yet.

Is it undecidable in the above-outlined combination of needs? You'd know better than me, I think — if you believe so, don't hesitate to tell =)

[ayazhafiz]

Do you care for subtyping? If not, consider a Hindley-Milner unification-based type system. You can emulate the feel of subtyping with row polymorphism (https://en.wikipedia.org/wiki/Row_polymorphism). Happy to expand more as necessary.

Otherwise I would consider developing your own system without trying to emulate those of typescript/mypy/etc. Mutation does make everything harder; in general mutation requires invariance, though maybe you can change that in special cases with flow typing.

[metaleap]

Do you care for subtyping?

I kinda did, at least in the sense of duck typing for (structurally-typed ie anonymous) objects/records (ie a func expecting a {l:List<Any>} also accepts a {foo:Whatever,l:List<Int>} value — this also extends then to tuples where a func expecting a (Int,Bool) also accepts an (Int,Bool,Str)), but rows would cover all that in a HM setup, I gather?

Still mutation isn't considered in the OG HM so I'll have to research which of the various HM-with-some-or-other-form-of-mutability approaches will be most applicable / least hampered. Doable, just I was on this non-HM track lately as I stumbled upon FT and your writings on it =)

I wondered: most HM "tutorial-style implementations/walkthroughs" rely on equality constraints with a notion of "there could be other constraints here but for now, just use type equality". Now an "isSubtype constraint" would be problematic for unification I gather, because not commutative unlike eq. But what other constraints are even typically ever considered there...

[ayazhafiz]

HM only considers equality, there is no ordering relation like in subtyping. The way you would model a function f : (Int, Bool) -> Unit accepting a "supertype" like (Int, Bool, Str) is to make it polymorphic in the row of the first argument - that is, f is typed forall r. (Int, Bool)r -> Unit, where r signifies that the tuple can contain any additional fields.

Mutation is fine, it just forces strict equivalence. You cannot mutate polymorphically (even in a subtype fashion).

[metaleap]

Something neat, thanks to your earlier pointer to Castagna's '22 set-theoretic types paper, I found a newer one by him-et-al Polymorphic Type Inference for Dynamic Languages (they seemingly let their certs expire, so it's a daring link) that promises to achieve polymorphic inference a whole lot more successfully/encompassingly than was previously achieved and in the presence of and utilization of set-theoretic / logical types, including (middle of page 5 first hints at that) achieving a subtyping instead of equality handling in an algorithm-W-inspired type-reconstruction mechanism — had to quickly share that find, might interest you and it's pretty recent =)

The Limitations section is sobering tho 😵‍💫

[ayazhafiz]

Yeah, it's a great paper. Thanks!

…

On Tue, Aug 13, 2024 at 4:43 AM Phil Schumann ***@***.***> wrote: Something neat, thanks to your earlier pointer to Castagna's '22 set-theoretic types paper, I found a newer one by him-et-al Polymorphic Type Inference for Dynamic Languages <https://www.pps.jussieu.fr/~gc/papers/dynlang.pdf> that promises to achieve polymorphic inference a whole lot more successfully/encompassingly than was previously achieved and in the presence of and utilization of set-theoretic / logical types, including (middle of page 5 hints at that) achieving a subtyping instead of equality handling in an algorithm-W-inspired type-reconstruction mechanism — had to quickly share that find, might interest you and it's pretty recent =) — Reply to this email directly, view it on GitHub <#1 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AE6GL6TGMPBSXWF2XYTRG7LZRHIN7AVCNFSM6AAAAABMAQQKDKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEOBVHAZDOOBYGM> . You are receiving this because you commented.Message ID: ***@***.***>