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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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.
Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.