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?

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?

By Matt M at Sat, 2013-09-28 20:30 | login or register to post comments

Refinement?

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.

By gasche at Mon, 2013-09-30 01:14 | login or register to post comments

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 PExp₀ and for Exp₀ t. We next build up, inductively, the types PExp_i and then Exp_i t. We want to maintain the invariant that Exp_i t is Exp t restricted to expressions of size/depth i. First, we obtain PExp_i, the pre-expressions at depth i such that eval is well-typed on them -- no junk allowed (unlike my last post). So PExp_i 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 Exp_i-1. From the tiny example, a Plus node should have its operands in Exp_i-1 Int.

We complete the inductive step by building Exp_i t from PExp_i. Because we have a well-typed term for eval, we'll know that for e: PExp_i we have a type for eval e -- Int, in our example -- and we basically want to define Exp_i 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?

By Matt M at Mon, 2013-09-30 04:52 | login or register to post comments

Lambda the Ultimate

User login

Navigation