Thu 24 Oct 2024 16:00 - 16:20 at IBR West - Types and Gradual Typing 1 Chair(s): Fabian Muehlboeck

Functions in functional languages have a single elimination form — application — and cannot be compared, hashed, or subjected to other non-application operations. These operations can be approximated via defunctionalization: functions are replaced with first-order data and calls are replaced with invocations of a dispatch function. Operations such as comparison may then be implemented for these first-order data to approximate e.g. deduplication of continuations in algorithms such as unbounded searches. Unfortunately, this encoding is tedious, imposes a maintenance burden, and obfuscates the affected code.

We introduce an alternative in intensional functions, a language feature which supports the definition of non-application operations in terms of a function’s definition site and closure-captured values. First-order data operations may be defined on intensional functions without burdensome code transformation. We give an operational semantics and type system and prove their formal properties. We further define intensional monads, whose Kleisli arrows are intensional functions, enabling monadic values to be similarly subjected to additional operations.

Thu 24 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
Types and Gradual Typing 1OOPSLA 2024 at IBR West
Chair(s): Fabian Muehlboeck Australian National University
16:00
20m
Talk
Intensional Functions
OOPSLA 2024
Zachary Palmer Swarthmore College, Nathaniel Wesley Filardo Microsoft, Ke Wu Johns Hopkins University
DOI
16:20
20m
Talk
Qualifying System F-sub
OOPSLA 2024
Edward Lee University of Waterloo, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, James You University of Waterloo, Kavin Satheeskumar University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen
DOI
16:40
20m
Talk
Refinement Type Refutations
OOPSLA 2024
Robin Webbers Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Ranjit Jhala UCSD
DOI
17:00
20m
Talk
Type Inference Logics
OOPSLA 2024
Denis Carnier KU Leuven, François Pottier Inria, Steven Keuchel Vrije Universiteit Brussel
DOI
17:20
20m
Talk
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs (SIGPLAN)
OOPSLA 2024
Guannan Wei Inria/ENS; Tufts University, Oliver Bračevac EPFL, LAMP, Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
Link to publication