I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable.

What about type inference ?

Whether type checking and type inference of Agda is undecidable ?

I'm interested not only in type checking but type inference also.

  • 2
    $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$
    – Raphael
    Apr 1 '16 at 7:19
  • 2
    $\begingroup$ 1. Your question is very broad. It sounds like you are asking for a survey of an entire area (decidability for a whole bunch of languages. I suggest you edit your question to narrow it down -- e.g., to ask about a single type system or language, and a single task (either type checking or type inference; pick one). 2. What research have you done? There's lots of literature on this. 3. Obviously type inference is at least as hard as type checking. $\endgroup$
    – D.W.
    Apr 1 '16 at 8:43
  • 1
    $\begingroup$ Conor McBride says: "Typechecking in Agda is decidable unless you switch off positivity/termination/universe checking". $\endgroup$ Apr 1 '16 at 12:37
  • $\begingroup$ See this question: cs.stackexchange.com/questions/12691/… $\endgroup$
    – cody
    Apr 2 '16 at 15:32

Your Answer

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

Browse other questions tagged or ask your own question.