NDLI: Subtyping and intersection types revisited

Content Provider	ACM Digital Library
Author	Pfenning, Frank
Abstract	Church's system of simple types has proven to be remarkably robust: call-by-name, call-by-need, and call-by-value languages, with or without effects, and even logical frameworks can be based on the same typing rules. When type systems become more expressive, this unity fractures. An early example is the value restriction for parametric polymorphism which is necessary for ML but not Haskell; a later manifestation is the lack of distributivity of function types over intersections in call-by-value languages with effects. In this talk we reexamine the logical justification for systems of subtyping and intersection types and then explore the consequences in two different settings: logical frameworks and functional programming. In logical frameworks functions are pure and their definitions observable, but complications could arise from the presence of dependent types. We show that this is not the case, and that we can obtain soundness and completeness theorems for a certain axiomatization of subtyping. We also sketch a connection to the type-theoretic notion of proof irrelevance. In functional programming we investigate how the encapsulation of effects in monads interacts with subtyping and intersection types, providing an updated analysis of the value restriction and related phenomena. While at present this study is far from complete, we believe that its origin in purely logical notions will give rise to a uniform theory that can easily be adapted to specific languages and their operational interpretations.
Starting Page	219
Ending Page	219
Page Count	1
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1291220.1291153
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	42
Issue Number	9
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Subtyping arithmetical types

Elaborating intersection and union types

Disjoint intersection types

Intersection types and computational effects

Tridirectional typechecking

Set-theoretic foundation of parametric polymorphism and subtyping

Polymorphic Functions with Set-Theoretic Types:Part 2: Local Type Inference and Type Reconstruction

Java type inference is broken:can we fix it?

Polymorphic regular tree types and patterns

Subtyping and intersection types revisited

Similar Documents

Subtyping arithmetical types

Elaborating intersection and union types

Disjoint intersection types

Intersection types and computational effects

Tridirectional typechecking

Set-theoretic foundation of parametric polymorphism and subtyping

Polymorphic Functions with Set-Theoretic Types:Part 2: Local Type Inference and Type Reconstruction

Java type inference is broken:can we fix it?

Polymorphic regular tree types and patterns

Subtyping and intersection types revisited