A Monadic Framework for Name Resolution in Multi-phased Type Checkers

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

17 Downloads (Pure)

Abstract

An important aspect of type checking is name resolution — i.e., determining the types of names by resolving them to a matching declaration. For most languages, we can give typing rules that define name resolution in a way that abstracts from what order different units of code should be checked in. However, implementations of type checkers in practice typically use multiple phases to ensure that declarations of resolvable names are available before names are resolved. This gives rise to a gap between typing rules that abstract from order of type checking and multi-phased type checkers that rely on explicit ordering.

This paper introduces techniques that reduce this gap. First, we introduce a monadic interface for phased name resolution which detects and rejects type checking runs with name resolution phasing errors where names were wrongly resolved because some declarations were not available when they were supposed to be. Second, building on recent work by Gibbons et al., we use applicative functors to compositionally map abstract syntax trees onto (phased) monadic computations that represent typing constraints. These techniques reduce the gap between type checker implementations and typing rules in the sense that (1) both are given by compositional mappings over abstract syntax trees, and (2) type checker cases consist of computations that roughly correspond to typing rule premises, except these are composed using monadic combinators. We demonstrate our approach by implementing type checkers for Mini-ML with Damas-Hindley-Milner type inference, and LM, a toy module language with a challenging import resolution policy.
Original languageEnglish
Title of host publicationGPCE 2023: Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery (ACM)
Pages14-28
Number of pages15
ISBN (Print)979-8-4007-0406-2
DOIs
Publication statusPublished - 2023
EventACM SIGPLAN International Conference on Generative Programming: Concepts & Experiences - Hotel Cascais Miragem, Cascais, Portugal
Duration: 22 Oct 202323 Oct 2023
Conference number: 22
https://2023.splashcon.org/home/gpce-2023

Conference

ConferenceACM SIGPLAN International Conference on Generative Programming: Concepts & Experiences
Abbreviated titleGPCE
Country/TerritoryPortugal
CityCascais
Period22/10/2323/10/23
Internet address

Keywords

  • scope graph
  • stable name resolution
  • applicative functor composition
  • type checker
  • phasing

Fingerprint

Dive into the research topics of 'A Monadic Framework for Name Resolution in Multi-phased Type Checkers'. Together they form a unique fingerprint.

Cite this