ICFP 2021 (series) / TyDe 2021 (series) / Workshop on Type-Driven Development 2021 /
A Simpler Encoding of Indexed Types
In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it’s particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.
Sun 22 AugDisplayed time zone: Seoul change
Sun 22 Aug
Displayed time zone: Seoul change
23:30 - 01:00 | |||
23:30 30mTalk | Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory (Extended Abstract) TyDe Media Attached File Attached | ||
00:00 30mTalk | A Simpler Encoding of Indexed Types TyDe Tesla Zhang The Pennsylvania State University Link to publication DOI Pre-print Media Attached | ||
00:30 30mTalk | Optics for Generic Declarative Server APIs (Extended Abstract) TyDe Andre Videla University Of Strathclyde Media Attached File Attached |