Typechecking is Undecidable when 'Type' is a Type
A function has a dependent type when the type of its result depends upon the value of its argument. The type of all types is the type of every type, including itself. In a typed l-calculus, these two features synergize in a conceptually clean and uniform way to yield enormous expressive power at ve...
| Автор: | |
|---|---|
| Опубліковано: |
2023
|
| Онлайн доступ: | https://hdl.handle.net/1721.1/149683 |
| _version_ | 1826204502458368000 |
|---|---|
| author | Reinhold, Mark B. |
| author_facet | Reinhold, Mark B. |
| author_sort | Reinhold, Mark B. |
| collection | MIT |
| description | A function has a dependent type when the type of its result depends upon the value of its argument. The type of all types is the type of every type, including itself. In a typed l-calculus, these two features synergize in a conceptually clean and uniform way to yield enormous expressive power at very little apparent cost. By reconstructing and analyzing a paradox due to Girard, we argue that there is no effective typechecking algorithm for such a language. |
| first_indexed | 2024-09-23T12:56:38Z |
| id | mit-1721.1/149683 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T12:56:38Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1496832023-03-30T03:42:17Z Typechecking is Undecidable when 'Type' is a Type Reinhold, Mark B. A function has a dependent type when the type of its result depends upon the value of its argument. The type of all types is the type of every type, including itself. In a typed l-calculus, these two features synergize in a conceptually clean and uniform way to yield enormous expressive power at very little apparent cost. By reconstructing and analyzing a paradox due to Girard, we argue that there is no effective typechecking algorithm for such a language. 2023-03-29T15:16:29Z 2023-03-29T15:16:29Z 1989-12 https://hdl.handle.net/1721.1/149683 21105894 MIT-LCS-TR-458 application/pdf |
| spellingShingle | Reinhold, Mark B. Typechecking is Undecidable when 'Type' is a Type |
| title | Typechecking is Undecidable when 'Type' is a Type |
| title_full | Typechecking is Undecidable when 'Type' is a Type |
| title_fullStr | Typechecking is Undecidable when 'Type' is a Type |
| title_full_unstemmed | Typechecking is Undecidable when 'Type' is a Type |
| title_short | Typechecking is Undecidable when 'Type' is a Type |
| title_sort | typechecking is undecidable when type is a type |
| url | https://hdl.handle.net/1721.1/149683 |
| work_keys_str_mv | AT reinholdmarkb typecheckingisundecidablewhentypeisatype |