GADTs meet subtyping

I was looking for work on GADTs in the presence of subtyping and found this 2013 paper GADTs meet subtyping of Gabriel Scherer and Didier Rémy.

Abstract. While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.

The running example of the paper is (can you guess?) an expression type. One thing that I was looking for specifically that I didn't find addressed in the paper is how to interpret e.g. even exp, where even is a subtype of int (in a more dependently typed language). Any thoughts on this or another other aspect of the paper?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Should eval and expr be defined together?

One technique that looks like it could be used as an alternative to GADTs for expressions, that naturally handles subtypes, is to first define pexpr to be a simple algebraic type of pre-terms that include all term constructors without regard to the well typedness of their interpretation (junk included). And next define eval and expr recursively together, such that 'a expr consists of the terms in pexpr that eval to an 'a. Has anyone played with this setup?


I'm not sure exactly how you would define such an `'a expr`. Are you assuming you have refinement types, or arbitrary dependent types? Even in that case, I would expect this approach to also need a "typing" function that return the type of the `pexpr` (in a sense the GADT declaration precomputes this).

It would probably help if you provided a pseudocode for your approach in a really simple case with few constructors.

Yes, refinement

Yeah, refinement types are enough for what I'm asking about. Here's a bit more detail that in the process changes the story slightly from my (more) hand wavey version above. A tiny example that captures the problem is (in a Haskellish syntax):

data Exp t 
    Lit : Int -> Exp Int
    Plus : Exp Int -> Exp Int -> Exp Int

eval : Exp t -> t
eval = ...

We start with empty sets for PExp0 and for Exp0 t. We next build up, inductively, the types PExpi and then Expi t. We want to maintain the invariant that Expi t is Exp t restricted to expressions of size/depth i. First, we obtain PExpi, the pre-expressions at depth i such that eval is well-typed on them -- no junk allowed (unlike my last post). So PExpi includes all expressions at a given depth that are suitable inputs to eval, without regard to its output. We enforce that condition by appropriate recursion on Expi-1. From the tiny example, a Plus node should have its operands in Expi-1 Int.

We complete the inductive step by building Expi t from PExpi. Because we have a well-typed term for eval, we'll know that for e: PExpi we have a type for eval e -- Int, in our example -- and we basically want to define Expi t to be the subset such that (eval e): t. That's a little delicate. Can you write that down in Coq, making use of our type for eval e? (I'm working with a logic that I think would allow this -- you can ask if all values Leibniz equal to eval e are also members of t). Another way to go about it would probably be to switch to modeling types as a base type and a predicate refinement.

Is there any work that you know of on GADTs and refinement types?