~bfiedler/typing-is-hard#12: 
Decidability of Idris type-checking

The word "surprisingly" would require further explanation. While most (all?) dependent type systems have undecidable inference, they generally have decidable type-checking as long as they do not feature non-terminating terms (see e.g. Martin-Löf type theory, and the calculus of constructions).

Status
RESOLVED FIXED
Submitter
~lnde3
Assigned to
No-one
Submitted
9 months ago
Updated
4 months ago
Labels
No labels applied.

~bfiedler REPORTED FIXED 4 months ago

Thanks for your thoughts. I've detailed the reason why I find it surprising (namely naïve implementations of dependent types have undeciable type-checking).

Register here or Log in to comment, or comment via email.