Generative Type Abstraction and Type-level Computation

I haven’t had lunch with Simon for awhile (it’s hard since he’s in Cambridge and only visits main campus occasionally) but he publishes papers at an amazing pace, and every time his language, Haskell, and the world gets a lot smarter. Here he introduces the concept of “roles” to aid in the problems that occur with type-level computation.

Generative Type Abstraction and Type-level Computation (Extended Version), by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Steve Zdancewic:

Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

Lambda The Ultimate describes the environment in which the paper finds itself and provides larger context:

In fact, this isn’t the first time coercion lifting has caused trouble. In capability security terminology, coercion lifting is a “rights amplification” operation, and there are previously known examples of seemingly innocuous coercion lifting across an abstraction/implementation boundary resulting in Confused Deputies. There’s no discussion of this connection in the paper, and the paper cannot solve the problem discussed at that link, which exposes an much deeper issue than confusing parametric/non-parametric contexts.