Recent searches
Search options
Does anyone have suggestions for reducing redundant code between infer/check phases of bidirectional type checking? One suggestion I've seen is to merge the two by replacing inference with checking against an updateable type slot that's initially empty, but I've found that I often prefer the more functional (and more verbose) style to this.
@zwarich I've mostly done closer to the second thing you mention but there's a nice-enough picture of it in terms of subtyping/subsumption. Instead of framing it in that imperative way with an "initially empty" type slot, you can treat the expected type parameter to elaborate() as a subtyping constraint, so "no expected type" corresponds to expected_type = any/top. Not much point if your type poset is otherwise flat but if you're doing bidirectional typing you often have some other subtyping.
@pervognsen Bidirectional typing works so well with coercive subtyping (just insert coercions on direction change) that I usually end up doing that rather than introducing full subsumptive subtyping. However, I like your idea. Even in the otherwise flat case having both ends of the lattice seems like a technical improvement over the other obvious approach of just using Option[Type].
@zwarich my implementation of a bidirectional type system doesn't have much redundant code (there is one place where the code is similar enough to consider if i should deduplicate it, but on a closer look it's quite different).
What is redundant in yours?
@zwarich if you have metavariables, one of the most effective ways of dealing with bidirectional type checking is
first, splitting all the terms into 3 groups (types are only checked for well-formedness, all other terms either are checked or inferred);
then, if you need to infer a type for a checked term, you instead check against a type shape instantiated with metavariables;
if you need to check an inferred term, you infer its type and then check that it's convertible to the expected type.
@zwarich i don't have metavariables (yet?), so i make do with only checking inferred terms, and have a single checked term that can be also inferred, which in my type system wouldn't benefit from code sharing
@wienski Yeah, the underlying flaw in my case is probably having too many terms that can be both checked and inferred. I like implicit/relative datatype constructors, so you can just do `.Variant(...)` for a sum or `{ field: value, ... }` for a product. These are convenient syntax, but they break the standard directionality conventions, and also cause more breakage downstream.
@zwarich these particular cases can be solved with inferring corresponding structural types that can be then converted in the check phase to their nominal counterparts
or with metavariables and unification
I wonder if some sort of Rete graph kinda thing would be useful here. Encode the inference and check rules as productions, have production rules poop out contradictions when detected.
(I should point out you’ve forgotten more about this sort of thing than I’ll ever know, so take anything I write as at best naive rubber ducking…)