-
Gradual Ty** for Effect Handlers
Authors:
Max S. New,
Eric Giovannini,
Daniel R. Licata
Abstract:
We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect ty**. This serves as a simple model of the integration of an effect ty** discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual m…
▽ More
We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect ty**. This serves as a simple model of the integration of an effect ty** discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual migration from unchecked to checked effect ty** in the style of Typed Racket.
The surface language GrEff is given semantics by elaboration to a core language Core GrEff. We equip Core GrEff with an inequational theory for reasoning about the semantic error ordering and desired program equivalences for programming with effects and handlers. We derive an operational semantics for the language from the equations provable in the theory. We then show that the theory is sound by constructing an operational logical relations model to prove the graduality theorem. This extends prior work on embedding-projection pair models of gradual ty** to handle effect ty** and subty**.
△ Less
Submitted 4 April, 2023;
originally announced April 2023.
-
A Formal Logic for Formal Category Theory (Extended Version)
Authors:
Max S. New,
Daniel R. Licata
Abstract:
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and…
▽ More
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category-theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model in virtual equipments, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.
△ Less
Submitted 18 February, 2023; v1 submitted 16 October, 2022;
originally announced October 2022.
-
Proceedings Ninth Workshop on Mathematically Structured Functional Programming
Authors:
Jeremy Gibbons,
Max S. New
Abstract:
This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022). The meeting took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of Software (ETAPS 2022). The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type…
▽ More
This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022). The meeting took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of Software (ETAPS 2022). The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. As the range of papers presented in this year's workshop shows, this continues to be a fruitful interface.
△ Less
Submitted 19 June, 2022;
originally announced June 2022.
-
Proceedings Eighth Workshop on Mathematically Structured Functional Programming
Authors:
Max S. New,
Sam Lindley
Abstract:
This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in Dublin, Ireland on the 25th of April as a satellite event of the European Joint Conferences on Theory & Practice of Software (ETAPS 2020).
Due to the COVID-19 pandemic, ETAPS 2020, and consequently MSFP 2020, has been p…
▽ More
This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in Dublin, Ireland on the 25th of April as a satellite event of the European Joint Conferences on Theory & Practice of Software (ETAPS 2020).
Due to the COVID-19 pandemic, ETAPS 2020, and consequently MSFP 2020, has been postponed to a date yet to be determined.
The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. This year's papers cover a variety of topics ranging from array programming to dependent types to effects.
△ Less
Submitted 30 April, 2020;
originally announced April 2020.
-
Gradual Type Theory (Extended Version)
Authors:
Max S. New,
Daniel R. Licata,
Amal Ahmed
Abstract:
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactoring…
▽ More
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, and is often neglected in the metatheory of gradual languages.
In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levy's call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. We then prove theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the $βη$ laws hold for a connective, then casts between that connective must be equivalent to the lazy cast semantics. Contrapositively, this shows that eager cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure and dually, gradual downcasts are strict. We show the consistency and applicability of our theory by proving that an implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual ty**. The model is parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.
△ Less
Submitted 6 November, 2018;
originally announced November 2018.
-
Graduality from Embedding-projection Pairs (Extended Version)
Authors:
Max S. New,
Amal Ahmed
Abstract:
Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland's (dynamic) gradual guarantee, which says that giving components of a program more precise types only adds runtime type checking, and does not otherwise change behavior. In this paper, we g…
▽ More
Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland's (dynamic) gradual guarantee, which says that giving components of a program more precise types only adds runtime type checking, and does not otherwise change behavior. In this paper, we give a semantic reformulation of the gradual guarantee called graduality. We change the name to promote the analogy that graduality is to gradual ty** what parametricity is to polymorphism. Each gives a local-to-global, syntactic-to-semantic reasoning principle that is formulated in terms of a kind of observational approximation.
Utilizing the analogy, we develop a novel logical relation for proving graduality. We show that embedding-projection pairs (ep pairs) are to graduality what relations are to parametricity. We argue that casts between two types where one is "more dynamic" (less precise) than the other necessarily form an ep pair, and we use this to cleanly prove the graduality cases for casts from the ep-pair property. To construct ep pairs, we give an analysis of the type dynamism relation (also known as type precision or naive subty**) that interprets the rules for type dynamism as compositional constructions on ep pairs, analogous to the coercion interpretation of subty**.
△ Less
Submitted 8 July, 2018;
originally announced July 2018.
-
Call-by-name Gradual Type Theory
Authors:
Max S. New,
Daniel R. Licata
Abstract:
We present gradual type theory, a logic and type theory for call-by-name gradual ty**. We define the central constructions of gradual ty** (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the "gradual guarantee" theorem of gradual ty**. Combine…
▽ More
We present gradual type theory, a logic and type theory for call-by-name gradual ty**. We define the central constructions of gradual ty** (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the "gradual guarantee" theorem of gradual ty**. Combined with the ordinary extensionality ($η$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisen's definitions of contracts, and use it to build some concrete domain-theoretic models of gradual ty**.
△ Less
Submitted 29 January, 2020; v1 submitted 31 January, 2018;
originally announced February 2018.
-
FabULous Interoperability for ML and a Linear Language
Authors:
Gabriel Scherer,
Max New,
Nick Rioux,
Amal Ahmed
Abstract:
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users fam…
▽ More
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages.
We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system.
To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.
△ Less
Submitted 12 April, 2018; v1 submitted 16 July, 2017;
originally announced July 2017.
