Epigram
Epigram: Practical programming with dependent types. Find the type error in the following Haskell expression: if null xs then tail xs else xs . You can’t, of course: this program is obviously nonsense unless you’re a typechecker. The trouble is that only certain computations make sense if the null xs test is True, whilst others make sense if it is False. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire conditional. Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn’t do it. Of course, tail [] doesn’t go wrong—well-typed programs don’t go wrong—so we’d better pick a different word for the way they do go. Abstraction and application, tupling and projection: these provide the ‘software engineering’ superstructure for programs, and our familiar type systems ensure that these operations are used compatibly. However, sooner or later, most programs inspect data and make a choice—at that point our familiar type systems fall silent. They simply can’t talk about specific data. All this time, we thought our programming was strongly typed, when it was just our software engineering. In order to do better, we need a static language capable of expressing the significance of particular values in legitimizing some computations rather than others. We should not give up on programming.
Keywords for this software
References in zbMATH (referenced in 22 articles )
Showing results 1 to 20 of 22.
Sorted by year (- Swierstra, Wouter: Heterogeneous binary random-access lists (2020)
- Cockx, Jesper; Devriese, Dominique; Piessens, Frank: Eliminating dependent pattern matching without K (2016)
- Cockx, Jesper; Devriese, Dominique; Piessens, Frank: Unifiers as equivalences: proof-relevant unification of dependently typed data (2016)
- Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
- Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
- Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
- Lawrence, Andrew; Berger, Ulrich; Seisenberger, Monika: Extracting a DPLL algorithm (2012)
- Abel, Andreas; Coquand, Thierry; Pagano, Miguel: A modular type-checking algorithm for type theory with singleton types and proof irrelevance (2011)
- Tesson, Julien; Hashimoto, Hideki; Hu, Zhenjiang; Loulergue, Frédéric; Takeichi, Masato: Program calculation in Coq (2011)
- Löh, Andres; McBride, Conor; Swierstra, Wouter: A tutorial implementation of a dependently typed lambda calculus (2010)
- Abel, Andreas: Typed applicative structures and normalization by evaluation for system (\mathrmF^\omega) (2009)
- Abel, Andreas; Coquand, Thierry; Pagano, Miguel: A modular type-checking algorithm for type theory with singleton types and proof irrelevance (2009)
- Barras, Bruno; Corbineau, Pierre; Grégoire, Benjamin; Herbelin, Hugo; Sacchini, Jorge Luis: A new elimination rule for the calculus of inductive constructions (2009)
- Bove, Ana; Dybjer, Peter: Dependent types at work (2009)
- Morris, Peter; Altenkirch, Thorsten; Ghani, Neil: A universe of strictly positive families (2009)
- Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Verifying a semantic (\beta\eta)-conversion test for Martin-Löf type theory (2008)
- Kaliszyk, Cezary: Web interfaces for proof assistants (2007)
- Sheard, Tim: Type-level computation using narrowing in (\Omega)mega (2007)
- Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo: Recursive coalgebras from comonads (2006)
- Morris, Peter; Altenkirch, Thorsten; McBride, Conor: Exploring the regular tree types (2006)