NDLI: Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)

Please wait, while we are loading the content...

When is a functional program not a functional program?

Modern languages for modern parallel computing (invited lecture, abstract only)

Monadic encapsulation in ML

You can design microprocessors too (invited lecture, abstract only): putting TRS's to work

Objects, classes and modules in Objective Caml (invited lecture, abstract only)

Trampolined style

From fast exponentiation to square matrices: an adventure in types

Tracing piece by piece: affordable debugging for lazy functional languages

Atomic heap transactions and fine-grain interrupts

On embedding a microarchitectural design language within Haskell

Recursion and dynamic data-structures in bounded space: towards embedded ML programming

A simple proof technique for certain parametricity results

Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)

Type fixpoints: iteration vs. recursion

Calling hell from heaven and heaven from hell

Interlanguage working without tears: blending SML with Java

Programming languages as operating systems (or revenge of the son of the lisp machine)

Haskell and XML: generic combinators or type-based translation?

Type inference with rank 1 polymorphism for type-directed compilation of ML

Type dispatch for named hierarchical types

Representing Java classes in a typed intermediate language

Principals in programming languages: a syntactic proof technique

Static interpretation of modules

Transparent modules with fully syntatic signatures

Flexible type analysis

Typer inference builds a short cut to deforestation

Verification of Erlang programs using abstract interpretation and model checking

Specialization of inductively sequential functional logic programs

Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)

Content Provider	ACM Digital Library
Author	Wells, J. B. Turbak, Franklyn A. Mairson, Harry G. Kfoury, Assaf J.
Abstract	We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ1 Λ τ2 to be used in some places at type τ1 and in other places at type τ2. A finite-rank intersection type system bounds how deeply the Λ can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorphism of System F and its extensions, while typing many more programs than the Hindley-Milner type system found in ML and Haskell.While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let K(0, n) = n and K(t + 1, n) = $2^{K(t,n)};$ we prove that recognizing the pure λ-terms of size n that are typable at rank k is complete for DTIME[K(k−1, n)]. We then consider the problem of deciding whether two λ-terms typable at rank k have the same normal form, generalizing a well-known result of Statman from simple types to finite-rank intersection types. We show that the equivalence problem is DTIME[K(K(k − 1, n), 2)]-complete. This relationship between the complexity of typability and expressiveness is identical in wellknown decidable type systems such as simple types and Hindley-Milner types, but seems to fail for System F and its generalizations. The correspondence gives rise to a conjecture that if Τ is a predicative type system where typability has complexity t(n) and expressiveness has complexity e(n), then t(n) = Ω(log* e(n)).
Starting Page	90
Ending Page	101
Page Count	12
File Format	PDF
ISBN	1581131119
DOI	10.1145/317636.317788
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1999-09-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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