Document Open Access Logo

Semantic Subtyping for Non-Strict Languages

Authors Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, Elena Zucca

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2018.4.pdf
  • Filesize: 0.57 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
Keywords
  • Semantic subtyping
  • non-strict semantics
  • call-by-need
  • union types
  • intersection types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.

Cite As Get BibTex

Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca. Semantic Subtyping for Non-Strict Languages. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2018.4

Author Details

Tommaso Petrucciani
  • DIBRIS, Università di Genova, Italy
  • IRIF, Université Paris Diderot, France
Giuseppe Castagna
  • CNRS, IRIF, Université Paris Diderot, France
Davide Ancona
  • DIBRIS, Università di Genova, Italy
Elena Zucca
  • DIBRIS, Università di Genova, Italy

References

  1. Davide Ancona and Andrea Corradi. Semantic subtyping for imperative object-oriented languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 568-587. ACM, 2016. URL: https://doi.org/10.1145/2983990.2983992.
  2. Zena M. Ariola and Matthias Felleisen. The call-by-need lambda calculus. Journal of Functional Programming, 7(3):265–301, 1997. Google Scholar
  3. Zena M. Ariola, John Maraist, Martin Odersky, Matthias Felleisen, and Philip Wadler. A call-by-need lambda calculus. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pages 233-246. ACM, 1995. URL: https://doi.org/10.1145/199448.199507.
  4. Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. CDuce: an XML-centric general-purpose language. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, ICFP '03, pages 51-63. ACM, 2003. URL: https://doi.org/10.1145/944705.944711.
  5. Véronique Benzaken, Giuseppe Castagna, Kim Nguyen, and Jérôme Siméon. Static and dynamic semantics of NoSQL languages. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 101-114. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429083.
  6. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. Semantic Subtyping with an SMT Solver. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 105-116. ACM, 2010. Google Scholar
  7. Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, Volume 1, Issue 2, 2005. URL: https://doi.org/10.2168/LMCS-1(2:1)2005.
  8. Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP '05, pages 198-199. ACM, 2005. URL: https://doi.org/10.1145/1069774.1069793.
  9. Giuseppe Castagna, Hyeonseung Im, Kim Nguyen, and Véronique Benzaken. A core calculus for XQuery 3.0. In Programming Languages and Systems, pages 232-256. Springer, 2015. Google Scholar
  10. Giuseppe Castagna and Victor Lanvin. Gradual typing with union and intersection types. Proceedings of the ACM on Programming Languages, 1(ICFP):41:1-41:28, 2017. URL: https://doi.org/10.1145/3110285.
  11. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types. Part 2: local type inference and type reconstruction. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 289-302. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676991.
  12. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. Polymorphic functions with set-theoretic types. Part 1: syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 5-17. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535840.
  13. Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyen. Set-theoretic types for polymorphic variants. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 378-391. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951928.
  14. Giuseppe Castagna and Zhiwu Xu. Set-theoretic foundation of parametric polymorphism and subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 94-106. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034788.
  15. Robert L. Constable and Scott Fraser Smith. Partial objects in constructive type theory. In IEEE Symposium on Logic in Computer Science (LICS), pages 183-193, 1987. Google Scholar
  16. Ornela Dardha, Daniele Gorla, and Daniele Varacca. Semantic subtyping for objects and classes. In Formal Techniques for Distributed Systems, pages 66-82. Springer, 2013. Google Scholar
  17. Eelco Dolstra and Andres Löh. NixOS: a purely functional Linux distribution. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, pages 367-378. ACM, 2008. URL: https://doi.org/10.1145/1411204.1411255.
  18. Joshua Dunfield. A unified system of type refinements. PhD thesis, Carnegie Mellon University, 2007. Google Scholar
  19. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Foundations of Software Science and Computation Structures, pages 250-266. Springer, 2003. Google Scholar
  20. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4):19:1-19:64, 2008. URL: https://doi.org/10.1145/1391289.1391293.
  21. John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. Journal of Functional Programming, 8(3):275–317, 1998. Google Scholar
  22. T. Petrucciani, G. Castagna, D. Ancona, and E. Zucca. Semantic subtyping for non-strict languages. Extended version. https://arxiv.org/abs/1810.05555, 2018.
  23. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 269-282. ACM, 2014. Google Scholar
  24. Jérôme Vouillon. Subtyping Union Types. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, pages 415-429. Springer, 2004. Google Scholar
  25. Jérôme Vouillon and Paul-André Melliès. Semantic Types: A Fresh Look at the Ideal Model for Types. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '04, pages 52-63. ACM, 2004. URL: https://doi.org/10.1145/964001.964006.
  26. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
  27. Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. Julia subtyping: A rational reconstruction. Proceedings of the ACM on Programming Languages, 2(OOPSLA):113:1-113:27, 2018. URL: https://doi.org/10.1145/3276483.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact