3.5 KiB
TODO
Performance and Software Architecture
- In
Generalization
, it would be possible to mergerank
andgeneric
into a single field. This can wait until the code is stable. (Try it and benchmark.)
Constraint API
-
Remove the
~rectypes
label and use a variant type. -
Offer an n-ary conjunction that produces a list as its semantic value: that is, a
list
combinator of type'a co list -> 'a list co
. Do the same foroption
. These combinators could be defined in terms ofCPure
,CConj
, andCMap
, but I would favor making them primitive, so as to avoid intermediate allocations. -
Simplify the treatment of names in constraints. Treat term variables and type variables in the same way, if possible. Treat all binding sites (
CExist
,CLet
, etc.) in the same way, if possible. Let the user decide whether to pick a fresh name or use a predetermined name. Avoid a design that would require multiple name transformations (i.e., composing multiple environment lookups). -
Can we remove the redundancy between
instance
and `instance_? (See next item.) -
Introduce a combinator
ignore : 'a co -> unit co
that allows the solver to solve a constraint without computing its semantic value. This could be marginally useful, e.g., by allowing Alice to package type inference and elaboration together, as a black box of typeF.term co
, and allowing Bob to pay only the cost of type inference, assuming he does not need elaboration. Also, it could remove the need for a primitiveinstance_
combinator, asinstance_ x ty
would correspond toignore (instance x ty)
. -
Introduce a
forall
combinator so as to make it easy to express∀α.c
.
Error Handling
-
Attach exploitable information to the exception
VariableScopeEscape
. -
Introduce more powerful combinators to handle errors in a programmatic way. Change the type
'a co
to('a, 'b) co
? Introduce aCCatch
construct to allow recovering after an error? (Think about Merlin, where type inference and elaboration are allowed to continue.) In a conjunction, distinguish an error in the left branch (producing just an error) and an error in the right branch (producing a value and an error)? Offer a way of decoding types after an error has occurred. -
Better distinguish between decoding in normal mode (where the decoder discovers generic variables only) and decoding in error mode (where the decoder does not discover any generic variables, but may find flexible and rigid variables). In the latter case, when decoding a variable, offer sensible ways of naming this variable; this may require a reverse lookup in an environment (beware of shadowing).
Documentation
- Document that decoding takes place after the unifier is done; decoding is performed either during elaboration or after the unifier has encountered an error.
Test Suite
-
Improve the coverage of the test suite. Add explicit negative test cases.
-
Run the random tests in parallel. (Parameterize
TestMLRandom
with the number and size of the tests, with therectypes
flag, etc., and run multiple instances in parallel.)
Debugging
- Introduce a dynamic check to ensure that the unifier never runs after the decoder has been invoked.
Sample Client
-
Include ranges in System F terms, and have the type-checker print the relevant range when a type error occurs.
-
The decoders are careful to perform as much sharing as possible, but the conversion of nominal types to de Bruijn types causes this sharing to be lost.