Some1 Like You

Dependent Pairs in Haskell

A talk by Sandy Maguire

reasonablypolymorphic.com

Slides available.

reasonablypolymorphic.com/some1-like-you

An (almost) real life example.

We will make a simple data-ingestion platform for our life-tracking app.

The program will provide an API with a unique endpoint for each distinct type of data we can ingest.

Survey says: big growth!

The marketing team says that by the end of the year, we'll have over 500 different "events" we'll want to be able to ingest.

At this scale, any boilerplate is bad news.

Boilerplate is boring to write and easy to get wrong.

A first attempt.

data Event = WakeUp
           | Eat     Meal
           | RockOut Song Duration

instance FromJSON Event where
  parseJSON = parseWakeUp
          <|> parseEat
          <|> parseRockOut

The API.

type Req  = ReqBody '[JSON] Value
type Resp = Post    '[JSON] Response

type EventAPI =
  "api" :> "event" :>
             ( "wake-up"  :> Req :> Resp
          :<|> "eat"      :> Req :> Resp
          :<|> "rock-out" :> Req :> Resp
             )

importEvent :: Value -> ExceptT ServantErr IO Response
importEvent blob =
  case fromJSON blob of
    Error   err -> throwM err
    Success ev  -> pure $ Response ev

wakeUp  = importEvent
eat     = importEvent
rockOut = importEvent

eventServer :: Server EventAPI
eventServer = serve $
  wakeUp :<|> eat :<|> rockOut

Notice how there is no type safety here.

Our wake-up endpoint will happily accept a eat payload.

We can do better!

Separate the constructors of our sum type into their own types.

data PayloadWakeUp  = PayloadWakeUp
data PayloadEat     = PayloadEat     Meal
data PayloadRockOut = PayloadRockOut Song Duration

instance FromJSON PayloadWakeUp
instance FromJSON PayloadEat
instance FromJSON PayloadRockOut

{-# LANGUAGE TemplateHaskell #-}

data Event = EventWakeUp  PayloadWakeUp
           | EventEat     PayloadEat
           | EventRockOut PayloadRockOut

makePrisms ''Event

Optics provide type safety!

We can use these prisms to lift our payload types into our Event type.

{-# LANGUAGE RankNTypes #-}

importEvent :: FromJSON e
            => Prism' Event e
            -> Value
            -> ExceptT ServantErr IO Response
importEvent prism blob =
  case fromJSON blob of
    Error   err -> throwM err
    Success e   -> pure . Response $ review prism e

Server upgrades.

wakeUp  = importEvent _PayloadWakeUp
eat     = importEvent _PayloadEat
rockOut = importEvent _PayloadRockOut

eventServer :: Server EventAPI
eventServer = serve $
  wakeUp :<|> eat :<|> rockOut

We've gained type safety!

The endpoints will no longer accept payloads of the wrong type.

The compiler doesn't know that our new payload types are related.

We can do better!

Grouping our payload types together might provide opportunities for more clever tricks.

A brief interlude.

On data kinds and type families.

Data kinds lifts values to types, and types to kinds.

Wat?

data Bool = True
          | False

begets, via DataKinds:

kind Bool where
  type 'True
  type 'False

Type families.

A type family is a function that returns a type.

A silly thing.

type family NotInt t where
  NotInt Int = ()
  NotInt a   = a

foo :: NotInt Bool
foo = True

bar :: NotInt Int
bar = ()

Type families only exist at the type level.

We can write type families over DataKinds.

Back to our regularly scheduled talk.

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}

data EventType = WakeUp | Eat | RockOut

data family Payload (e :: EventType)

data instance (Payload 'WakeUp) =
  PayloadWakeUp

data instance (Payload 'Eat) =
  PayloadEat Meal

data instance (Payload 'RockOut) =
  PayloadRockOut Song Duration

instance FromJSON (Payload 'WakeUp)
instance FromJSON (Payload 'Eat)
instance FromJSON (Payload 'RockOut)

Data types for free.

Armed with this type family, we can get our old sum type for free.

{-# LANGUAGE GADTs #-}

data Event where
  MkEvent :: Payload (et :: EventType) -> Event

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE ScopedTypeVariables #-}

importEvent :: forall (et :: EventType)
             . FromJSON (Payload et)
            => Value
            -> ExceptT ServantErr IO Response

importEvent blob =
  case fromJSON blob of
    Error err ->
      throwM err

    Success (e :: Payload et) ->
      pure . Response $ MkEvent e

Make it compile again.

{-# LANGUAGE TypeApplications #-}

wakeUp  = importEvent @'WakeUp
eat     = importEvent @'Eat
rockOut = importEvent @'RockOut

eventServer :: Server EventAPI
eventServer = serve $
  wakeUp :<|> eat :<|> rockOut

Notice that we've eliminated some boilerplate.

We no longer need to keep our Event type in sync with the payload types.

We can do better!

Generating the API definition automatically would remove a lot more boilerplate.

The EventType now exists at the value level.

We might have a chance!

API changes.

type Req  = ReqBody '[JSON] Value
type Resp = Post    '[JSON] Response

type EventAPI =
  "api" :>
    "event" :>
      Capture "event-type" EventType :> Req :> Resp

Too clever for our own good.

importEvent :: EventType
            -> Value
            -> ExceptT ServantErr IO Response

importEvent et blob =
  case fromJSON blob of
    Error err ->
      throwM err

    Success (e :: Payload et) ->
      pure . Response $ MkEvent e

It doesn't work.

No instance for (FromJSON (Payload et))
  arising from a use of `fromJSON'
  

Huh??

A brief interlude.

On singletons.

Consider Unit.

() :: ()

If you know what value you have, you know its type, and vice-versa.

Singletons generalize this.

We'll introduce a new type for each value we'd like to move to the type level.

Sounds like DataKinds!

But it's not.

Unfortunately, not the same types as provided by DataKinds.

{-# LANGUAGE PolyKinds  #-}
{-# LANGUAGE TypeInType #-}

data family Sing (a :: k)

class SingKind k where
  fromSing :: Sing (a :: k) -> k
  toSing   :: k -> SomeSing k

data instance (Sing 'True)  = STrue
data instance (Sing 'False) = SFalse


instance SingKind Bool where
  fromSing s = case s of
    STrue  -> True
    SFalse -> False

  toSing b = case b of
    True  -> SomeSing STrue
    False -> SomeSing SFalse

It doesn't have to be so bad!

singletons [d|
  data Bool = True
            | False
  |]

Not just for Bools!

singletons [d|
  data EventType = WakeUp
                 | Eat
                 | RockOut
  |]

A helper function.

withSomeSing :: SingKind k
             => k
             -> (forall (a :: k). Sing a -> r)
             -> r

Back to our regularly scheduled talk.

Armed with this knowledge, we can lift our EventType value into the type system!

importEvent :: EventType
            -> Value
            -> ExceptT ServantErr IO Response

importEvent etype blob =
  withSomeSing etype $ \ (_ :: Sing et) ->
    case fromJSON blob of
      Error err ->
        throwM err

      Success (e :: Payload et) ->
        pure . Response $ MkEvent e

It still doesn't work.

No instance for (FromJSON (Payload et))
  arising from a use of `fromJSON'
  

Huh?????????????

Didn't we fix this?

Stupid compiler.

We know that FromJSON is total over Payload.

But how can we prove it?

If it's too hard, prove it at the term level.

dictFromJSON :: ( FromJSON (Payload 'WakeUp)
                , FromJSON (Payload 'Eat)
                , FromJSON (Payload 'RockOut)
                )
             => Sing (a :: EventType)
             -> Dict (FromJSON (Payload a))

A Dict c is a proof that we have the constraint c.

dictFromJSON :: ( FromJSON (Payload 'WakeUp)
                , FromJSON (Payload 'Eat)
                , FromJSON (Payload 'RockOut)
                )
             => Sing (a :: EventType)
             -> Dict (FromJSON (Payload a))
dictFromJSON s = case s of
  SWakeUp  -> Dict
  SEat     -> Dict
  SRockOut -> Dict

importEvent :: EventType
            -> Value
            -> ExceptT ServantErr IO Response

importEvent etype blob =
  withSomeSing etype $ \ (setype :: Sing et) ->
    case dictFromJSON setype of
      Dict ->
        case fromJSON blob of
          Error err ->
            throwM err

          Success (e :: Payload et) ->
            pure . Response $ MkEvent e

So groovy.

eventServer :: Server EventAPI
eventServer = serve importEvent

Compiler driven coding.

It is now impossible to incorrectly hook up a new EventType:

• Exhaustiveness checking of dictFromJSON ensures we made a new payload type and gave it a ToJSON instance.
• The API definitions and server handlers write themselves.

The other half of the problem.

We also want to serialize these new events into a single pipe for downstream consumption.

For simplicitly we'll also use JSON going downstream.

We know the drill.

dictToJSON :: ( ToJSON (Payload 'WakeUp)
              , ToJSON (Payload 'Eat)
              , ToJSON (Payload 'RockOut)
              )
           => Sing (a :: EventType)
           -> Dict (ToJSON (Payload a))
dictToJSON s = case s of
  SWakeUp  -> Dict
  SEat     -> Dict
  SRockOut -> Dict

We can do better!

Besides the constraints under consideration, dictToJSON is identical to dictFromJSON.

{-# LANGUAGE ConstraintKinds #-}

dictPayload :: ( c (Payload 'WakeUp)
               , c (Payload 'Eat)
               , c (Payload 'RockOut)
               )
            => Sing (a :: EventType)
            -> Dict (c (Payload a))
dictPayload s = case s of
  SWakeUp  -> Dict
  SEat     -> Dict
  SRockOut -> Dict

We can now lift any constraint that is total over Payload.

Let's use it to implement ToJSON over Events.

instance ToJSON Event where
  toJSON (MkEvent payload) = toJSON payload

It doesn't work.

No instance for (ToJSON (Payload et))
  arising from a use of `toJSON'
  

Oh yeah. It doesn't lift automatically.

We need a singleton to get the Dict.

But we don't have one.

But we used to!

Save that singleton.

data Event where
  MkEvent :: Sing (et :: EventType)
          -> Payload et
          -> Event

instance ToJSON Event where
  toJSON (MkEvent setype payload) =
    case dictPayload @ToJSON setype of
      Dict ->
        object [ "type"    .= fromSing setype
               , "payload" .= payload
               ]

We can write a similar FromJSON instance.

We're done!

But what can we take away?

We didn't invent the Event type.

In the literature, the combination of a value and a type that depends on that type is known as a dependent pair.

We can write the type of a dependent pair like this:

$$\sum_\text{a :: EventType} \text{Payload}(a)$$

Highschool algebra.

$$\sum_\text{a :: EventType} \text{Payload}(a) = \text{Payload}(a_1) + \text{Payload}(a_2) + \cdots + \text{Payload}(a_n)$$

Look familiar?

data Event = EventWakeUp  (Payload WakeUp)
           | EventEat     (Payload Eat)
           | EventRockOut (Payload RockOut)

This type is perfectly captured by the dependent pair.

More generally.

$$(a, b) :: \sum_\text{a :: A} \text{F}(a)$$

We can encode this directly in Haskell.

Namesake of the talk.

data Some1 (f :: k -> Type) where
  Some1 :: Sing (a :: k) -> f a -> Some1 f

Specializing.

type Event = Some1 Payload

But that's not all.

We can generalize our dictPayload function as well:

class Dict1 (c :: output -> Constraint)
            (f :: input  -> output) where
  dict1 :: Sing (a :: input) -> Dict (c (f a))

It comes pre-assembled.

All of this machinery has already been built for you!

https://hackage.haskell.org/package/exinst

It also provides instances lifting Dict1 over Some1, as well as tons of other goodies.

Thanks for listening!

Questions?