NDLI: Efficient type inference using ranked type variables

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

Efficient type inference using ranked type variables

Status report: specifying javascript with ML

Generics for the working ML'er

$ML^{F}$ for everyone (users, implementers, and designers)

Status report: the manticore project

Status report: layered streaming XML processing with modules

Practical generic programming in OCaml

Status report: hot pickles, and how to serve them

Status report: marionnet or "how to implement a virtual network laboratory in six months and be happy"

A persistent union-find data structure

Efficient type inference using ranked type variables

Content Provider	ACM Digital Library
Author	MacQueen, David Kuan, George
Abstract	The Damas-Milner type inference algorithm (commonly known as algorithm W) is at the core of all ML type checkers. Although the algorithm is known to have poor worst-case behavior [8], in practice well-engineered type checkers will run in approximately linear time. To achieve this efficiency, implementations need to improve on algorithm W's method of scanning the complete type environment to determine whether a type variable can be generalized at a let binding. Following a suggestion of Damas, most ML type checkers use an alternative method based on ranking unification variables to track their position in the type environment. Here we formalize two such ranking systems, one based on lambda depth (used in the SML/NJ compiler), and the other based on let depth (used in OCaml, for instance). Each of these systems is formalized both with and without the value restriction, and they are proved correct relative to the classic algorithm W. Our formalizations of the various algorithms use simple abstract machines that are similar to small-step evaluation semantics.
Starting Page	3
Ending Page	14
Page Count	12
File Format	PDF
ISBN	9781595936769
DOI	10.1145/1292535.1292538
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-10-02
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Type inference Standard ml Type checking Algorithm w Functional programming Compilers
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