Publications

Quotient Polymorphism (pdf)

Brandon Hewer and Graham Hutton. Submitted for publication, February 2025.

Quotient types increase the power of type systems by allowing types to include equational properties. However, two key issues arise: code being duplicated, and valid code being rejected. Specifically, function definitions often need to be repeated for each quotient of a type, and valid functions may be rejected if they include subterms that do not respect the quotient. This article addresses these reusability and expressivity issues by introducing the notion of quotient polymorphism. We implement this idea in Quotient Haskell, and demonstrate its benefits for practical programming, type checking performance, and quotient inference.

Quotient Haskell: lightweight quotient types for all (paper)

Brandon Hewer and Graham Hutton. Proceedings of the ACM on Programming Languages, volume 8, Issue POPL, Article 27, January 2024.

Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.

Subtyping Without Reduction (paper)

Brandon Hewer and Graham Hutton. Proceedings of the 14th International Conference on Mathematics of Program Construction, LNCS volume 13544, September 2022.

Subtypes are useful and ubiquitous, allowing important properties of data to be captured directly in types. However, the standard encoding of subtypes gives no control over when the reduction of subtyping proofs takes place, which can significantly impact the performance of type-checking. In this article, we show how operations on a subtype can be represented in a more efficient manner that exhibits no reduction behaviour. We present the general form of the technique in Cubical Agda by exploiting its support by higher-inductive types, and demonstrate the practical use of the technique with a number of examples.

HoTT Operads (pdf)

Brandon Hewer and Graham Hutton. March 2024.

Internalising classes of datatypes has been a longstanding pursuit in type theory. For example, containers capture strictly positive types, while combinatorial species capture finitely labelled structures. To date, however, there has been no similar attempt to internalise classes of operations on datatypes. In this paper we show how the theory of operads, which extend species with a well-behaved notion of composition, provides a natural approach to internalising finitary operations. We present an internalisation of operads in homotopy type theory, which provides a generic framework for capturing and reasoning about operations with particular algebraic properties. All our results are formalised in Cubical Agda.