POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Thu 23 Jan 2025 15:20 - 15:40 at Marco Polo - Types 1 Chair(s): Stephanie Weirich

We present MoCaml, a new path-based type system for a fully fledged ML-module language that avoids the signature avoidance problem. This is achieved by introducing floating fields, which acts as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as zippers on module signatures, and can be seen as a lightweight extension on existing signatures. Floating fields allows to delay the resolution of signature avoidance as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give a simple equivalence criterion for the simplification of floating components without loss of type-sharing. We present a principled strategy that implements this criterion and performs much better than OCaml. Remaining floating fields, instead of polluting the code, partially disappear at functor applications and fully disappear at signature ascription, including toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, either to be explicitly resolved by the user, or kept until link time. The correctness of the type system is proved by elaboration into M𝜔 , which has itself been proved sound by translation to F𝜔 . The language include module type definitions that are kept and returned in inferred types, as long as possible. MoCaml has been designed to be a specification of an improvement over OCaml with transparent ascription, a better solution to signature avoidance, while staying close to the source language and to its implementation.

Thu 23 Jan

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

15:00 - 16:20
Types 1POPL at Marco Polo
Chair(s): Stephanie Weirich University of Pennsylvania
15:00
20m
Talk
A Dependent Type Theory for Meta-programming with Intensional Analysis
POPL
Jason Z.S. Hu Amazon Web Services, USA, Brigitte Pientka McGill University
15:20
20m
Talk
Avoiding signature avoidance in ML modules with zippers
POPL
15:40
20m
Talk
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL
Shengyi Jiang , Chen Cui University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
16:00
20m
Talk
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
POPL
Taro Sekiyama National Institute of Informatics; SOKENDAI, Hiroshi Unno Tohoku University