Precise definitions of promotion and lifting

17 views Asked by At

In the literature on typed functional programming, these terms appear frequently, and their definitions seems to be assumed. I don't seem to be able to find it spelled out formally anywhere.

The first term is promotion. This applies when, for example, creating a little metalanguage. Here (in Haskell) the Integer type is promoted into the Expr type, enabling Expr to represent integers:

data Expr = EInt Integer

That's clear enough, and I can understand how it is similar to the promotion of a char to an int in C. The integer values are essentially unchanged, but they're wearing a new uniform, so to speak.

It's very clear to me that the term lifting applies, for example, in the case of functors. The whole substance of Haskell's Functor typeclass is the ability to lift a function into the functor with fmap.

The problem is that the terms are also used to refer to more complex transformations, e.g. "With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors."

This promotion from data constructors into type constructors makes something less powerful and fancy into something more powerful: it makes data constructors into type constructors etc.

The term lifting can apparently be used in the same way: "GADTs cannot be promoted, because the type equalities in their definition cannot be lifted to kind equalities.".

I'm probably just being pedantic, but I can't see how the basic meanings of the two terms and the fancy type-level meanings are really the same thing, except in a sort of loose sense. So I'm looking for clarification, and ideally a pithy definition of the terms promotion and lifting that makes it clear when it's safe to use them, and just how precise or vague they are.

0

There are 0 answers