# Slides available.

reasonablypolymorphic.com/existentialization



# The Problem

• We would like to be able to automatically generate quickcheck properties for instances we write
• eg. automatic proofs that every Monad instance is well behaved

# Heterogeneous Lists

• Let's say we are Javascript programmers and we hate types
• We want to make a list that can contain values of any type
• Haskell doesn't let us do this:
[1, 2, 3] :: [Int]   -- ok
[True]    :: [Bool]  -- ok
[1, True] :: ??      -- type error, :(

# Heterogeneous Lists

• This is not all that useful, it turns out.
• But even so, is Haskell such a shit language that we can't express such a thing?

# The Any Type

data Any where
Any :: a -> Any

We can think of Any as a container.

We can stuff whatever we want into it, and get back a value of type Any.

# The Any Type

data Any where
Any :: a -> Any

Any True                    :: Any
Any (show :: Int -> String) :: Any

We've lost track of what type the value inside the Any had.

We say the a is now existential.

As in: we know it exists, but not much else about it.

# RIGID SKOLEMS

What happens if we try to take the value out of the Any?

f (Any a) = a

Any guesses?

# RIGID SKOLEMS

• Couldn't match expected type ‘t’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor: Any :: forall a. a -> Any,



u wot m8

# RIGID SKOLEMS

We can get some insight by looking at what type this thing would have.

f :: Any -> a
f (Any a) = a

# RIGID SKOLEMS

But recall that this is short form for:

f :: forall a. Any -> a
f (Any a) = a

ie. "I can give you back any a you want"

# That's a damn lie

There's a specific a inside the Any.

It might be a Bool or a String or whatever, but it is not "whatever you ask for".

# Too Rigid

You will run into this error all the time when you first start existentializing things.

So that's what this means:

• a (rigid, skolem) variable is a type that is existentially quantified
• you can't leak it out because it doesn't even EXIST outside

# Anyways

This kind of solves our subproblem:

listOfAnything :: [Any]
listOfAnything = [ Any 5
, Any Bool
, Any (show :: Char -> String)
]

But it's not actaully useful because we can never get any of this data out.

# Usefulness

As you might guess, this doesn't mean we can't actually do anything useful with the technique.

Just that it requires more thinking

Let's talk about iterators. Like in Python or whatever.

# Iterators

We want to be able to produce a series of values.

And maybe these values depend on some sort of state

We don't really care what that state is, so long as we can pull values out of it

# A first try

data Iterator s a = Iterator
{ iterState :: s
, iterNext  :: s -> (a, s)
}

This seems to do what we want.

# But it's kinda gross

The state variable leaks.

That means you can't make a list of these things with different pieces of internal state, eg.

# Iterators Take 2

Let's existentialize it!

data Iterator a where
Iterator :: { iterState :: s
, iterNext  :: s -> (a, s)
} -> Iterator a

The thing to notice here is that i don't care what the internal state is

It doesn't leak out of my type signature

# Pump It Real Good

• We can implement a function that uses an Iterator to spit out a s
pump :: Iterator a -> (a, Iterator a)
pump iter = let getNext = iterNext iter
(a, s') = getNext $iterState iter in (a, Iterator s' getNext) This is kind of neat. # Pump It Real Good pump :: Iterator a -> (a, Iterator a) pump iter = let getNext = iterNext iter (a, s') = getNext$ iterState iter
in (a, Iterator s' getNext)

We can think of this as

(iterState, iterNext) :: exists s. (s, s -> (a, s))

GHC doesn't know what this s type variable is, but it knows that iterState and iterNext are talking about the same thing.

# And now for something seemingly completely different.

data Dict (c :: Constraint) where
Dict :: c => Dict c

Notice here that c exists in the type, and so it is not existential.

But this is not any old data type!

# Constructing Dicts

This says we can only construct a Dict c if c is an instance.

eg.

Dict :: Dict (Enum Bool)        -- ok
Dict :: Dict (Show Int)         -- ok

Dict :: Dict (Eq (Int -> Int))  -- bad

Haskell doesn't have equality defined for functions.

# Reified Constraints

What value does this provide us?

It means we can pass constraints along as values -- they're now refied at the value level.

maybeShow :: a -> Maybe (Dict (Show a)) -> String
maybeShow a (Just Dict) = show a
maybeShow _ Nothing     = "i don't know how to show that"

maybeShow True (Just Dict)  -- "True"
maybeShow flip Nothing      -- "i don't know how to show that"

# Generalizing

We can use the same technique to make a more useful any-list

data Showable where
Showable :: Show a => a -> Showable

showList :: [Showable] -> [String]
showList = fmap (λ(Showable a) -> show a)

-------------------------------------

myList :: [Showable]
myList = [Showable 1, Showable Bool, Showable "hello"]

showList myList  -- [1, Bool, "\"hello\""]

# A Counter Example

Something we can't do:

data Equatable where
Equatable :: Eq a => a -> Equatable

equate :: Equatable -> Equatable -> Bool
equate (Equatable a) (Equatable b) = a == b

# A Counter Example

This doesn't work, because it's morally equivalent to this:

equate :: exists a b. (Eq a, Eq b) => a -> b -> Bool
equate a b = a == b

We don't know that a and b have the same type!

# Eliminators

In general, the strategy for doing useful things with existential variables is to introduce eliminators for them.

If we want to do something useful with a value of unknown type, we're going to need to provide a function that can do something FOR ALL types.

# Eliminators

The general form of it is this:

eliminate :: SomeExistential -> (forall a. a -> r) -> r

If you give us an existential, and a way of constructing an r for any type I throw at you, then I can give you back an r.

wat?

# Eliminators

A dumb example:

eliminate myExistential (const True)   -- True

# Eliminators

eliminate :: SomeExistential -> (forall a. a -> r) -> r

The forall a. a bit should be replaced with the definition of the existential.

# Eliminators

data Showable where
Showable :: Show a => a -> Showable

eliminateShowable :: Showable
-> (forall a. Show a => a -> r)
-> r

# Eliminators

data Iterator a where
Iterator :: { iterState :: s
, iterNext  :: s -> (a, s)
} -> Iterator a

eliminateIterator :: Iterator a
-> (forall s. s
-> (s -> (a, s))
-> r)
-> r

# Eliminate the Lack of Intuition

The idea is that if can produce some r (that i get to choose) from whatever contents are inside the existential

Then I can produce an r given some existential value!

# A Server

Let's say I want to run a server that will respond to different endpoints.

But each endpoint will take and return different payload types.

# A Server

class Encodable a where
encode :: a -> ByteString
decode :: ByteString -> a

instance Encodable Bool
instance Encodable Int
instance Encodable String
-- etc

# A Server

data SomeHandler where
SomeHandler :: (Encodable a, Encodable b)
=> (a -> IO b)
-> SomeHandler

# A Server

recv :: IO (Endpoint, ByteString)
send :: IO ByteString

serve :: [(Endpoint, SomeHandler)] -> IO ()
serve handlers = forever $do (endpoint, payload) <- recv case lookup endpoint handlers of Nothing -> putStrLn "no handler!" Just (SomeHandler handler) -> result <- handler$ decode payload
send \$ encode result

# Thanks for listening!

Any questions?

Space Forward Next slide Previous slide Open presenter console Toggle this help