Back to Search
Start Over
Generative type abstraction and type-level computation
- Source :
- POPL
- Publication Year :
- 2011
- Publisher :
- ACM, 2011.
-
Abstract
- Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.
Details
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
- Accession number :
- edsair.doi.dedup.....cf0d81595c69690c8b3b88556da7908f