Timeline for Does dependent type checkers need to store lambda parameter type in their core language?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 19 at 16:46 | vote | accept | ice1000 | ||
| Jun 3, 2019 at 1:16 | vote | accept | ice1000 | ||
| Jun 3, 2019 at 1:17 | |||||
| Jun 2, 2019 at 21:08 | comment | added | Joey Eremondi | @ice1000 "This falsifies..." No it doesn't, because Idris's type system is defined by its core language. An expression is well typed if it elaborates to a well typed core term. You want your core language to be simple and facilitate easy checking, which is why they include the types in the core but not in the surface language, where they get the types from annotations. It's about separation of concerns: getting types from context is done in elaboration, so that when the core is typechecked, all the necessary information is already there. | |
| Jun 2, 2019 at 5:27 | comment | added | ice1000 | I should update the question -- this sounds like something necessary for people who are not familiar with these languages to understand my question. | |
| Jun 2, 2019 at 5:26 | comment | added | ice1000 | But Idris does not have type annotation for lambdas syntactically, just like Agda/MiniAgda/MiniTT. They're only different in their core language representation. This falsifies "it makes your type system syntax directed in a very simple way". | |
| Jun 2, 2019 at 3:57 | history | answered | Joey Eremondi | CC BY-SA 4.0 |