Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sj\"oberg (University of Pennsylvania), Chris Casinghino, (University of Pennsylvania), Ki Yung Ahn (Portland State University), Nathan, Collins (Portland State University), Harley D. Eades III (University of, Iowa), Peng Fu (University of Iowa)
TL;DR
This paper introduces a dependently typed core language that combines nontermination, irrelevance, and heterogeneous equality under call-by-value evaluation, addressing their complex interactions for type safety.
Contribution
It presents a novel language design integrating nontermination, erasure, and heterogeneous equality, which has not been previously explored together.
Findings
Language supports nontermination and irrelevance simultaneously
Type safety is maintained through careful erasure of terminating expressions
Heterogeneous, erased propositional equality is effectively handled
Abstract
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.