research-article

Generative type abstraction and type-level computation

Authors:

Stephanie Weirich,

Dimitrios Vytiniotis,

Simon Peyton Jones,

Steve ZdancewicAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 227 - 240

https://doi.org/10.1145/1925844.1926411

Published: 26 January 2011 Publication History

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.

Supplementary Material

MP4 File (20-mpeg-4.mp4)

Download
453.66 MB

References

[1]

M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing, 10(4):265--289, 2003. ISSN 1236--6064.

Digital Library

[2]

A. Bove, P. Dybjer, and U. Norell. A brief overview of agda -- a functional language with dependent types. In TPHOLs '09: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pages 73--78, Berlin, Heidelberg, 2009. Springer-Verlag.

Digital Library

[3]

V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172--221, 1991.

Digital Library

[4]

M. M. T. Chakravarty, G. Keller, and S. Peyton Jones. Associated type synonyms. In ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pages 241--253, New York, NY, USA, 2005. ACM.

Digital Library

[5]

M. M. T. Chakravarty, G. Keller, S. Peyton Jones, and S. Marlow. Associated types with class. SIGPLAN Not., 40(1):1--13, 2005b. ISSN 0362--1340.

Digital Library

[6]

J.Chapman,P.Evariste Dagand,C.McBride,and P.Morris.The gentleart of levitation. In Proceedings of the Fifteenth ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, MD, USA, September 2010. To appear.

Digital Library

[7]

J. Cheney and R. Hinze. First-class phantom types. CUCIS TR2003--1901, Cornell University, 2003.

[8]

R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-118--82, Department of Computer Science, University of Edinburgh, June 1982.

[9]

R. L. Constable and D. R. Zlatin. The type theory of PL/CV3. ACM Transactions on Programming Languages and Systems, 6(1):94--117, Jan. 1984.

Digital Library

[10]

K. Crary and S. Weirich. Flexible type analysis. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Pro- gramming, pages 233--248, Paris, France, Sept. 1999.

Digital Library

[11]

N. G. de Bruijn. Telescopic mappings in typed lambda calculus. Inf. Comput., 91(2):189--204, 1991. ISSN 0890--5401.

Digital Library

[12]

D. Dreyer. Recursive type generativity. In ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pages 41--53, New York, NY, USA, 2005. ACM.

Digital Library

[13]

P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525--549, 2000.

[14]

C. V. Hall, K. Hammond, S. L. Peyton Jones, and P. L. Wadler. Type classes in Haskell. ACM Transactions on Programming Languages and Systems, 18(2):109--138, Mar. 1996.

Digital Library

[15]

R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 130--141, New York, NY, USA, 1995. ACM. ISBN 0--89791--692--1.

Digital Library

[16]

R. Hinze, J. Jeuring, and A. Loeh. Type-indexed data types. In B. M. Eerke Boiten, editor, Proceedings of the Sixth International Conference on Mathematics of Program Construction (MPC 2002), pages 148--174, Dagstuhl, Germany, July 2002.

Digital Library

[17]

O. Kiselyov, S. Peyton Jones, and C. Shan. Springer, 2010.

[18]

Fun with type functions.

[19]

D. R. Licata and R. Harper. A formulation of dependent ML with explicit equality proofs. Technical Report Carnegie Mellon University-CS-05--178, Carnegie Mellon University Department of Computer Science, 2005.

[20]

P. Martin-Löf. An intuitionistic theory of types: Predicative part. In Proceedings of the Logic Colloquium, 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73--118. North-Holland, 1975.

[21]

R. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997. ISBN 0262631814.

Digital Library

[22]

B. Montagu and D. Rémy.Modeling abstract types in modules with open existential types.In POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 354--365, New York, NY, USA, 2009. ACM.

Digital Library

[23]

G. Neis, D. Dreyer, and A. Rossberg. Non-parametric parametricity. In ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, pages 135--148, New York, NY, USA, 2009. ACM. ISBN 978--1--60558--332--7.

Digital Library

[24]

S. Peyton Jones et al. The Haskell 98 language and libraries: The revised report. Journal of Functional Programming, 13(1):0--255, Jan 2003. http://www.haskell.org/definition/.

Digital Library

[25]

S. L. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In International Confer- ence on Functional Programming (ICFP), Portland, OR, USA, Sept. 2006.

Digital Library

[26]

B. C. Pierce, editor. Advanced Topics in Types and Programming Lan-guages. MIT Press, 2005.

Digital Library

[27]

A. Rossberg. Dynamic translucency with abstraction kinds and higher-order coercions. Electr. Notes Theor. Comput. Sci., 218:313--336, 2008.

Digital Library

[28]

A. Rossberg. Generativity and dynamic opacity for abstract types. In PPDP '03: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, pages 241--252, NewYork,NY,USA,2003.ACM.ISBN1--58113--705--2.

Digital Library

[29]

C. V. Russo. Non-dependent types for Standard ML modules. In PPDP '99: Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, pages 80--97, London, UK, 1999. Springer-Verlag. ISBN 3--540--66540--4.

Digital Library

[30]

T. Schrijvers, S. Peyton Jones, M. Chakravarty, and M. Sulzmann. Type checking with open type functions. In ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 51--62, New York, NY, USA, 2008. ACM.

Digital Library

[31]

Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou. A type system for certified binaries. ACM Trans. Program. Lang. Syst., 27(1):1--45, 2005.

Digital Library

[32]

M. Sulzmann, M. M. T. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. In TLDI '07: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pages 53--66, New York, NY, USA, 2007. ACM.

Digital Library

[33]

The Coq Team. Coq. URL http://coq.inria.fr.

[34]

D. Vytiniotis, G. Washburn, and S. Weirich. An open and shut typecase. I.

[35]

ACM SIGPLAN Workshop in Types in Language Design and Implementation, Long Beach, CA, USA, Jan. 2005.

[36]

H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In POPL, pages 224--235, 2003.

Digital Library

Cited By

Zhou LWan QOliveira B(2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689718
Breitner JEisenberg RPeyton Jones SWeirich S(2014)Safe zero-cost coercions for HaskellACM SIGPLAN Notices10.1145/2692915.262814149:9(189-202)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628141
Blanvillain OBrachthäuser JKjaer MOdersky M(2022)Type-level programming with match typesProceedings of the ACM on Programming Languages10.1145/34986986:POPL(1-24)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498698
Show More Cited By

Index Terms

Generative type abstraction and type-level computation
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Generative type abstraction and type-level computation
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
Type invariants for Haskell
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification

Multi-parameter type classes, functional dependencies, and recently GADTs and open type families open up opportunities to use complex type-level programming to let GHC's type checker verify various properties of your programs. But type-level code is ...
Type Class Instances for Type-Level Lambdas in Haskell
TFP 2015: Revised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 9547

Haskell 2010 lacks flexibility in creating instances of type classes for type constructors with multiple type arguments. We would like to make the order of type arguments to a type constructor irrelevant to how type class instances can be specified. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 1

POPL '11

January 2011

624 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1925844

Issue’s Table of Contents

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Published in SIGPLAN Volume 46, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
454
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)3

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhou LWan QOliveira B(2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689718
Breitner JEisenberg RPeyton Jones SWeirich S(2014)Safe zero-cost coercions for HaskellACM SIGPLAN Notices10.1145/2692915.262814149:9(189-202)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628141
Blanvillain OBrachthäuser JKjaer MOdersky M(2022)Type-level programming with match typesProceedings of the ACM on Programming Languages10.1145/34986986:POPL(1-24)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498698
Kiss CField TEisenbach SPeyton Jones S(2019)Higher-order type-level programming in HaskellProceedings of the ACM on Programming Languages10.1145/33417063:ICFP(1-26)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341706
Weirich SChoudhury PVoizard AEisenberg R(2019)A role for dependent types in HaskellProceedings of the ACM on Programming Languages10.1145/33417053:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341705
Christiansen DDiatchki IDockins RHendrix JRavitch T(2019)Dependently typed Haskell in industry (experience report)Proceedings of the ACM on Programming Languages10.1145/33417043:ICFP(1-16)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341704
Kiss CPickering MWu N(2018)Generic deriving of generic traversalsProceedings of the ACM on Programming Languages10.1145/32367802:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236780
Breitner JEisenberg RPeyton Jones SWeirich S(2014)Safe zero-cost coercions for HaskellACM SIGPLAN Notices10.1145/2692915.262814149:9(189-202)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628141
Breitner JEisenberg RPeyton Jones SWeirich SJeuring JChakravarty M(2014)Safe zero-cost coercions for HaskellProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628141(189-202)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2628136.2628141
Cretin JRémy DHenzinger TMiller D(2014)System F with coercion constraintsProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603128(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603128
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents