This website is out of date, please refer to the site on github.

Notes on Abstract and Existential Types

Posted on September 29, 2014
Tags: haskell, types, notes

I’m part of a paper reading club at CMU. Last week we talked about a classic paper, Abstract Types have Existential Type. The concept described in this paper is interesting and straightforward. Sadly some of the notions and comparisons made in the paper are starting to show their age. I thought it might be fun to give a tldr using Haskell.

The basic idea is that when we have an type with an abstract implementation some functions upon it, it’s really an existential type.

Some Haskell Code

To exemplify this let’s define an abstract type (in Haskell)

    module Stack (Stack, empty, push, pop) where
    newtype Stack a = Stack [a]

    empty :: Stack a
    empty = Stack []

    push :: a -> Stack a -> Stack a
    push a (Stack xs) = Stack (a : xs)

    pop :: Stack a -> Maybe a
    pop (Stack []) = Nothing
    pop (Stack (x : xs)) = Just x

    shift :: Stack a -> Maybe (Stack a)
    shift (Stack []) = Nothing
    shift (Stack (x : xs)) = Just (Stack xs)

Now we could import this module and use its operations:

    import Stack

    main = do
      let s = push 1 . push 2 . push 3 $ empty
      print (pop s)

What we couldn’t do however, is pattern match on stacks to take advantage of its internal structure. We can only build new operations out of combinations of the exposed API. The classy terminology would be to say that Stack is abstract.

This is all well and good, but what does it mean type theoretically? If we want to represent Haskell as a typed calculus it’d be a shame to have to include Haskell’s (under powered) module system to talk about abstract types.

After all, we’re not really thinking about modules as so much as hiding some details. That sounds like something our type system should be able to handle without having to rope in modules. By isolating the concept of abstraction in our type system, we might be able to more deeply understand and reason about code that uses abstract types.

This is in fact quite possible, let’s rephrase our definition of Stack

    module Stack (Stack, StackOps(..), ops) where

    newtype Stack a = Stack [a]

    data StackOps a = StackOps { empty :: Stack a
                               , push  :: a -> Stack a -> Stack a
                               , pop   :: Stack a -> Maybe a
                               , shift :: Stack a -> Maybe (Stack a) }
    ops :: StackOps
    ops = ...

Now that we’ve lumped all of our operations into one record, our module is really only exports a type name, and a record of data. We could take a step further still,

    module Stack (Stack, StackOps(..), ops) where

    newtype Stack a = Stack [a]

    data StackOps s a = StackOps { empty :: s a
                                 , push  :: a -> s a -> s a
                                 , pop   :: s a -> Maybe a
                                 , shift :: s a -> Maybe (s a) }
    ops :: StackOps Stack
    ops = ...

Now the only thing that needs to know the internals of Stack. It seems like we could really just smush the definition into ops, why should the rest of the file see our private definition.

    module Stack (StackOps(..), ops) where

    data StackOps s a = StackOps { empty :: s a
                                 , push  :: a -> s a -> s a
                                 , pop   :: s a -> Maybe a
                                 , shift :: s a -> Maybe (s a) }
    ops :: StackOps ???
    ops = ...

Now what should we fill in ??? with? It’s some type, but it’s meant to be chosen by the callee, not the caller. Does that sound familiar? Existential types to the rescue!

    {-# LANGUAGE PolyKinds, KindSignatures, ExistentialQuantification #-}
    module Stack where

    data Packed (f :: k -> k' -> *) a = forall s. Pack (f s a)

    data StackOps s a = StackOps { empty :: s a
                                 , push  :: a -> s a -> s a
                                 , pop   :: s a -> Maybe a
                                 , shift :: s a -> Maybe (s a) }
    ops :: Packed StackOps
    ops = Pack ...

The key difference here is Packed. It lets us take a type function and instantiate it with some type variable and hide our choice from the user. This means that we can even drop the whole newtype from the implementation of ops

    ops :: Packed StackOps
    ops = Pack $ StackOps { empty = []
                          , push  = (:)
                          , pop   = fmap fst . uncons
                          , shift = fmap snd . uncons }
      where uncons [] = Nothing
            uncons (x : xs) = Just (x, xs)

Now that we’ve eliminated the Stack definition from the top level, we can actually just drop the notion that this is in a separate module.

One thing that strikes me as unpleasant is how Packed is defined, we must jump through some hoops to support StackOps being polymorphic in two arguments, not just one.

We could get around this with higher rank polymorphism and making the fields more polymorphic while making the type less so. We could also just wish for type level lambdas or something. Even some of the recent type level lens stuff could be aimed at making a general case definition of Packed.

From the client side this definition isn’t actually so unpleasant to use either.

    {-# LANGUAGE RecordWildCards #-}

    someAdds :: Packed Stack Int -> Maybe Int
    someAdds (Pack Stack{..}) = pop (push 1 empty)

With record wild cards, there’s very little boilerplate to introduce our record into scope. Now we might wonder about using a specific instance rather than abstracting over all possible instantiations.

    someAdds :: Packed Stack Int -> Maybe Int
    someAdds =
      let (Pack Stack{..}) = ops in
        pop (push 1 empty)

The resulting error message is amusing :)

Now we might wonder if we gain anything concrete from this. Did all those language extensions actually do something useful?

Well one mechanical transformation we can make is that we can change our existential type into a CPS-ed higher rank type.

    unpackPacked :: (forall s. f s a -> r) -> Packed f a -> r
    unpackPacked cont (Pack f) = cont f

    someAdds' :: Stack s Int -> Maybe Int
    someAdds' Stack{..} = pop (push 1 empty)

    someAdds :: Packed Stack Int -> Maybe Int
    someAdds = unpackPacked someAdds'

Now we’ve factored out the unpacking of existentials into a function called unpack. This takes a continuation which is parametric in the existential variable, s.

Now our body of someAdds becomes someAdds, but notice something very interesting here, now s is a normal universally quantified type variable. This means we can apply some nice properties we already have used, eg parametricity.

This is a nice effect of translating things to core constructs, all the tools we already have figured out can suddenly be applied.

Wrap Up

Now that we’ve gone through transforming our abstract types in existential ones you can final appreciate at least one more thing: the subtitle on Bob Harper’s blog. You can’t say you didn’t learn something useful :)

I wanted to keep this post short and sweet. In doing this I’m going to some of the more interesting questions we could ask. For the curious reader, I leave you with these

Cheers.

comments powered by Disqus