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