J Garrett Morris


I study the foundations of programming: how we construct programs and how we reason about them. My thesis is that advances in type systems empower programmers to create better-written, better-understood programs:

These advances form a virtuous cycle. More precise types enable better abstractions, while expressive abstractions make precise type systems easy to use.

I am always looking for good students. If you have a background in functional programming, an interest in the theory and implementation of type systems in modern functional languages, and want to work with me at UI, please get in touch.

In Fall 2020, I joined the Department of Computer Science at the University of Iowa as an assistant professor. I work in the Computational Logic Center with Aaron Stump, and Cesare Tinelli. Before my current post, I was a researcher in the Laboratory for Foundations of Computer Science at the University of Edinburgh. I worked with Phil Wadler and Sam Lindley on the ABCD project, which studies the role of session types in safe concurrent and distributed programming, and contributed to the design and implementation of linear types and session types for the Links programming language. I received my Ph.D. from the computer science department at Portland State University, advised by Mark P. Jones. As part of the High Assurance Systems Programming project, I contributed to the design of the Habit programming language, particularly its class system, and to the development of the Habit compiler, particularly its typechecking and desugaring components.

Flip ahead to my teaching, publications, grants, or contact information.


At the University of Iowa

CS:5850 (Semantics): Spring 2022

CS:4980 (Functional algorithms): Spring 2021

CS:3820 (Programming languages): Fall 2020, Fall 2021, Fall 2022

At the University of Kansas

EECS 210 (Discrete mathematics): Spring 2020

EECS 662 (Programming languages): Fall 2017, Spring 2019, Spring 2020

EECS 665 (Compilers): Spring 2018

EECS 762 (Semantics): Fall 2018, Fall 2019


Apoorv Ingle, Alex Hubers, and J. Garrett Morris. "Partial Type Constructors in Practice". Haskell '21.

Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higher-order abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design

The published version is available in PDF.

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. "Separating Sessions Smoothly". CONCUR '21.

This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions.

Mark Jones, J. Garrett Morris, and Richard Eisenberg. "Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc". Proc. ACM Program. Lang., 4, POPL (January 2020).

Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.

The published version is available in PDF or via the ACM DL.

Wen Kokke, J. Garrett Morris, and Philip Wadler. "Towards Races in Linear Logic". COORDINATION '19.

Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude non- determinism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel com- position from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCPND , which extends HCP with a novel account of non- determinism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as non- deterministic choice, while preserving HCP's meta-theoretic properties, including deadlock freedom.

The author's version is available in PDF.

J. Garrett Morris and James McKinna. "Abstracting Extensible Data Types; Or, Rows By Any Other Name." Proc. ACM Program. Lang., 3, POPL (January 2019).

We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic λ-calculus.

The published version is available in PDF.

Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. "Exceptional Asynchronous Session Types: Session Types without Tiers." Proc. ACM Program. Lang., 3, POPL (January 2019).

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications—especially distributed applications—where failure is pervasive.

We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating.

We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully.

As published [PDF], and the extended version [PDF].

Jack Williams, J. Garrett Morris and Philip Wadler. "The Root Cause of Blame: Contracts for Intersection and Union Types". Proc. ACM Prog. Lang. 2, OOPSLA (October 2018).

Gradual typing has emerged as the tonic for programmers wanting a mixture of static and dynamic typing, hoping to achieve the best of both. Sound gradual typing is the most potent brew, providing static type- checking and dynamic assertions. Contracts provide a lightweight form of gradual typing as they do not provide static checking but can be implemented as a library, rather than demanding language level support.

Intersection and union types are well suited to dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types, or the context of the operator, unlike existing work.

We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if, when monitored against that type in any context, never elicits positive blame. A continuation negatively satisfies a type if, when monitored against that type using any value, never elicits negative blame.

We supplement our definition of satisfaction with a serious of monitoring properties that satisfying values and continuations should have. Each type has a positive property for values and a negative property for continuations, ensuring that contracts reflect the types they represent.

The conference version is available in PDF.

J. Garrett Morris and Richard A. Eisenberg. "Constrained Type Families". Proc. ACM Prog. Lang. 1, ICFP, Article 42 (September 2017).

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

The conference version [PDF] and extended edition [PDF] are available. Note that these contain updated affiliation information, and so should be preferred to the ACM digital library version.

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. "Mixed Messages: Measuring Conformance and Non-Interference in TypeScript". 31st European Conference on Object-Oriented Programming, {ECOOP} 2017, LIPIcs 74, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.

TypeScript participates in the recent trend among programming languages to support gradual typing. The DefinitelyTyped Repository for TypeScript supplies type definitions for over 2000 popular JavaScript libraries. However, there is no guarantee that implementations conform to their corresponding declarations.

We present a practical evaluation of gradual typing for TypeScript. We have developed a tool, based on the polymorphic blame calculus, for monitoring JavaScript libraries and TypeScript clients against the TypeScript definition. We apply our tool, TypeScript TNG, to those libraries in the DefinitelyTyped Repository which had adequate test code to use. Of the 122 libraries we checked, 59 had cases where either the library or its tests failed to conform to the declaration.

Gradual typing should satisfy non-interference. Monitoring a program should never change its behaviour except, to raise a type error should a value not conform to its declared type. However, our experience also suggests serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. Of the 122 libraries we checked, 22 had cases where the library or its tests violated non-interference.

Available in PDF.

J. Garrett Morris. "The Best of Both Worlds: Linear Functional Programming Without Compromise". In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016.

We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.

The extended edition is available in PDF. Note that this version fixes several inadvertent omissions and typographical errors, and so should be preferred to the conference version. The conference version is available from the ACM DL.

Sam Lindley and J. Garrett Morris. "Talking Bananas: Structural Recursion for Session Types". In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016.

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.

We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.

Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.

Available in PDF or from the ACM DL.

Sam Lindley and J. Garrett Morris. "Embedding Session Types in Haskell". In Proceedings of the 9th International Symposium on Haskell (Haskell 2016), Nara, Japan, 2016.

We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of the linear λ-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of the session typing discipline. We give two interpretations of our embedding, one in terms of GHC's built-in concurrency and another in terms of purely functional continuations. Our safety guarantees, including deadlock freedom, are assured statically and introduce no additional runtime overhead.

Paper available in PDF or from the ACM DL. See the source code on Github.

Robert Atkey, Sam Lindley, and J. Garrett Morris. "Conflation Confers Concurrency". In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. LNCS 9600.

Session types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble π-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (⊗ and ⅋) allows processes to share multiple channels; conflating the additives (⊕ and &) provides nondeterminism; and conflating the exponentials (! and ?) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion.

Available from Springer or in PDF.

J. Garrett Morris. "Variations on Variants". In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, Vancouver, BC.

Extensible variants improve the modularity and expressiveness of programming languages: they allow program functionality to be decomposed into independent blocks, and allow seamless extension of existing code with both new cases of existing data types and new operations over those data types.

This paper considers three approaches to providing extensible variants in Haskell. Row typing is a long understood mechanism for typing extensible records and variants, but its adoption would require extension of Haskell's core type system. Alternatively, we might hope to encode extensible variants in terms of existing mechanisms, such as type classes. We describe an encoding of extensible variants using instance chains, a proposed extension of the class system. Unlike many previous encodings of extensible variants, ours does not require the definition of a new type class for each function that consumes variants. Finally, we translate our encoding to use closed type families, an existing feature of GHC. Doing so demonstrates the interpretation of instances chains and functional dependencies in closed type families.

One concern with encodings like ours is how completely they match the encoded system. We compare the expressiveness of our encodings with each other and with systems based on row types. We find that, while equivalent terms are typable in each system, both encodings require explicit type annotations to resolve ambiguities in typing not present in row type systems, and the type family implementation retains more constraints in principal types than does the instance chain implementation. We propose a general mechanism to guide the instantiation of ambiguous type variables, show that it eliminates the need for type annotations in our encodings, and discuss conditions under which it preserves coherence.

Paper available from the ACM DL or in PDF. Sample code available here.

Sam Lindley and J. Garrett Morris. "A Semantics for Propositions as Sessions". ESOP 2015.

Session types provide a static guarantee that concurrent programs respect communication protocols. Recently, Caires, Pfenning, and Toninho, and Wadler, have developed a correspondence between propositions of linear logic and session typed π-calculus processes. We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language. We begin by presenting a variant of Wadler's session-typed core functional language, GV. We give a small-step operational semantics for GV. We develop a suitable notion of deadlock, based on existing approaches for capturing deadlock in π-calculus, and show that all well-typed GV programs are deadlock-free, deterministic, and terminating. We relate GV to linear logic by giving translations between GV and CP, a process calculus with a type system and semantics based on classical linear logic. We prove that both directions of our translation preserve reduction; previous translations from GV to CP, in contrast, failed to preserve β-reduction. Furthermore, to demonstrate the modularity of our approach, we define two extensions of GV which preserve deadlock-freedom, determinism, and termination.

Available from Springer or in PDF.

J. Garrett Morris. "A Simple Semantics of Haskell Overloading". In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Gothenburg, Sweden.

As originally proposed, type classes provide overloading and ad-hoc definition, but can still be understood (and implemented) in terms of strictly parametric calculi. This is not true of subsequent extensions of type classes. Functional dependencies and equality constraints allow the satisfiability of predicates to refine typing; this means that the interpretations of equivalent qualified types may not be interconvertible. Overlapping instances and instance chains allow predicates to be satisfied without determining the implementations of their associated class methods, introducing truly non-parametric behavior. We propose a new approach to the semantics of type classes, interpreting polymorphic expressions by the behavior of each of their ground instances, but without requiring that those behaviors be parametrically determined. We argue that this approach both matches the intuitive meanings of qualified types and accurately models the behavior of programs.

Available from the ACM DL or in PDF.

Sam Lindley and J. Garrett Morris. "Sessions as Propositions". In PLACES 2014.

Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.

Available from arXiv or in PDF.

J. Garrett Morris. Type Classes and Instance Chains: A Relational Approach. PhD thesis, Portland State University, 2013.

Type classes, first proposed during the design of the Haskell programming language, extend standard type systems to support overloaded functions. Since their introduction, type classes have been used to address a range of problems, from typing ordering and arithmetic operators to describing heterogeneous lists and limited subtyping. However, while type class programming is useful for a variety of practical problems, its wider use is limited by the inexpressiveness and hidden complexity of current mechanisms. We propose two improvements to existing class systems. First, we introduce several novel language features, instance chains and explicit failure, that increase the expressiveness of type classes while providing more direct expression of current idioms. To validate these features, we have built an implementation of these features, demonstrating their use in a practical setting and their integration with type reconstruction for a Hindley-Milner type system. Second, we define a set-based semantics for type classes that provides a sound basis for reasoning about type class systems, their implementations, and the meanings of programs that use them.

Available in PDF.

J. Garrett Morris and Mark P. Jones. "Instance Chains: Type Class Programming Without Overlapping Instances." In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, Maryland. 2010.

Type classes have found a wide variety of uses in Haskell programs, from simple overloading of operators (such as equality or ordering) to complex invariants used to implement type-safe heterogeneous lists or limited subtyping. Unfortunately, many of the richer uses of type classes require extensions to the class system that have been incompletely described in the research literature and are not universally accepted within the Haskell community.

This paper describes a new type class system, implemented in a prototype tool called ilab, that simplifies and enhances Haskell-style type-class programming. In ilab, we replace overlapping instances with a new feature, instance chains, allowing explicit alternation and failure in instance declarations. We describe a technique for ascribing semantics to type class systems, relating classes, instances, and class constraints (such as kind signatures or functional dependencies) directly to a set-theoretic model of relations on types. Finally, we give a semantics for ilab and describe its implementation.

Available from the ACM DL or in PDF.

J. Garrett Morris. "Experience Report: Using Hackage to Inform Language Design." In Proceedings of the 3rd ACM Symposium on Haskell (Haskell '10), Baltimore, Maryland.

Hackage, an online repository of Haskell applications and libraries, provides a hub for programmers to both release code to and use code from the larger Haskell community. We suggest that Hackage can also serve as a valuable resource for language designers: by providing a large collection of code written by different programmers and in different styles, it allows language designers to see not just how features could be used theoretically, but how they are (and are not) used in practice.

We were able to make such a use of Hackage during the design of the class system for a new Haskell-like programming language. In this paper, we sketch our language design problem, and how we used Hackage to help answer it. We describe our methodology in some detail, including both ways that it was and was not effective, and summarize our results.

Available from the ACM DL or in PDF.

Some of these papers are copyright ACM. These are the author's versions of the work. They are posted here by permission of ACM for your personal use. Not for redistribution. Please see each paper for the location of the definitive version.

sponsored projects

"CAREER: Extensibility in Theory and Practice", Principle Investigator. National Science Foundation. 2021–2026.

Modern software engineering relies on large ecosystems of independent software components and libraries. This poses two challenges for the design of programming languages and language tooling, both of which are addressed by this project. First, languages must support developing independent components, including identifying and abstracting reusable components from existing applications. Second, languages must provide expressive specification mechanisms to ensure that components are used correctly and that components do not have unintended interactions. The project's novelties are new programming language features for modular specification and implementation of program data and behavior, at all level of the software stack from user-facing applications to operating system components and hardware support. The project's impacts are improvements in both software reliability and programmer productivity, as the project enables language tooling to automatically help programmers identify and correctly use software components and libraries.

The project has two primary themes. The first is modularity and reuse in high-level functional programs. The project develops extensible types for data and computational effects, supporting high-level abstractions including overloading, generic programming, and extensible effect handlers. The second is modularity and reuse in low-level and systems programs. The project develops extensible bit-level specifications of data structures and their layout, targeting applications including operating system kernels and hardware interfaces. Each of these themes will only have impact if the resulting language features have comparable performance with existing approaches. The project uses linear typing and compile-type specialization to offset runtime costs traditionally associated with generic and extensible programming techniques.

This is NSF award #2044815; progress will be recounted here.


Electronic mail: garrett-morris@uiowa.edu
DBLP: J. Garrett Morris
Google scholar: PZIdxNgAAAAJ
OrcID: 0000-0002-3992-1080