3
$\begingroup$

I'm looking for resources on (partial) type inference for dependent types.

For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that makes some choices and infers non-principal types.

I'm also not sure how to integrate type inference into constraint-based type checking.

Are there any papers on this?

| cite | improve this question | |
$\endgroup$
2
$\begingroup$

I recommend to look at (1) first, which might be the canonical early work on this problem and lead to the ATS programming language. (2) is a recent work on the same problem.

As to using constraints for type inference, (3) is probably the canonical reference.

  1. H. Xi, F. Pfenning, Dependent Types in Practical Programming.
  2. T. Terauchi, Dependent Types from Counterexamples.
  3. F. Pottier, D. Remy, The Essence of ML Type Inference.
| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.