4.0 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
let0
,let1
, andletn
be simplified or combined? Do we really need aCLet
form that binds several names at once? Can the treatment of unreachable type variables be simplified? -
Solving a
CLet
constraint produces a list of pairstevar * scheme
, butletn
keeps only the second component of every pair. Ifletn
is the only entry point, then the result type ofCLet
constraints can be simplified. -
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)
.
Error Handling
-
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.
-
Improve the documentation produced by
make doc
. -
Document the requirement that the function passed to
map
must be pure. Use this hypothesis to remove the useless evaluation ofk1 env
in the definition of^^
.
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.