A poor man's ∀


In folklore it is often said that knowing somethings's true name gives a person great power over it. I often find that to be true when dealing with type signatures and type quantifications.

Not always do we want to grant control over the data types we expose, because that can lead to a loss of abstraction. Universal quantification is a powerful toolset for cases like this, and lack of a languages support for it can be painful.

That became an issue for me today when I was working on some code in Rust, where there's no way to express universal quantification. I found a simple and ingenious (albeit restricted) solution that I'd like to share here.

As a simple example, let's try express a type that wraps a profunctor-shaped Conduit and universally quantifies it in the first type parameter. In Haskell, this is straight-forward: type Producer b = forall a. Conduit a b. In Rust, it is not so easy. All type variables that are used in the type declaration have to be part of the resulting type's parameters: type Producer<A, B> = Conduit<A, B>.

Why is this bad? Well, think of Rumpelstiltskin; if you can name the type, you can control it. Since A appears in the signature for Producer, it gives everybody the power to introspect the type and raise constraints against it. We don't want that.

Types and Logic

Luckily, Propositions as Types can help us out here. Specifically, equating the unit type with the concept of triviality and the void type with the concept of impossibility, we can use both for a poor man's universal quantification for types parameters in covariant and contravariant positions.

Making use of the fact that the unit type can be trivially constructed, when a type parameter in a contravariant position is inhabited by it, we can generalize by universally quantifying that type parameter:

∃ (F : Unit -> b) => ∃ (G : ∀a. a -> b)
q :: forall a. Profunctor p => p () b -> p a b
q = lmap $ const ()

Similarly, following ex falso quodlibet, when a type parameter in a covariant position is inhabited by an impossible type, we can generalize by universally quantifying that type parameter.

∃ (F : a -> Void) => ∃ (G : ∀b. a -> b)
q :: forall a. Profunctor p => p a Void -> p a b
q = rmap absurd

(Void and absurd are signatures from Ed Kmett's Data.Void package)

So, how does this help us?

We can now specify our quantification in terms of void and unit, which gives us these signatures which can be exposed from our module:

type Producer<B> = Conduit<(), B>;
type Consumer<A> = Conduit<A, Void>;

And as soon as we want to compose the types, which would normally eliminate the universal quantification, we can simply use the functions described above. Translated into Rust, those are:

fn from_producer<A, B>(p: Producer<B>) -> Conduit<A, B> {
    p.lmap(|_| ())

fn from_consumer<A, B>(c: Consumer<A>) -> Conduit<A, B> {
    c.rmap(|_| unreachable!())
Written on October 7, 2015