The Hidden Type Theory Powering Reflex — Dependent Types in Production Haskell

by lazyLambda

If you've used Reflex, you've felt it: once your code compiles, the event wiring just works. Wrong connections? The compiler catches them. You never cast, never pattern match on a sum type to recover what event you're dealing with. It's eerily smooth.

What you might not know is that this isn't some FRP magic. Under the hood, Reflex is a dependently-typed event system — smuggled into Haskell via GADTs. The libraries that make this possible are dependent-sum, dependent-map, and dependent-sum-template. If you've seen them in your dependency tree and wondered what they do, this post is for you.

The Problem: Heterogeneous Event Streams

Imagine a websocket connection. Messages arrive as a single stream, but each message type carries different data:

In most frameworks, you'd model this as a sum type:

data WsMsg
  = ChatMessage Text
  | UserJoined UserId
  | PriceUpdate (Map Ticker Double)
  | ServerError ErrorCode

Then you'd pattern match everywhere downstream. Every handler has to deal with the full sum, even though each handler only cares about one constructor. Refactoring means touching every pattern match. Adding a new message type means hunting down every case expression.

This is fine for small programs. It does not scale.

DSum: The Existential Pair

dependent-sum introduces DSum, a pair where the value type is determined by the key:

data DSum tag f = forall a. !(tag a) :=> f a

The tag is a GADT — each constructor fixes the type variable a:

data WsTag a where
  ChatMessage :: WsTag Text
  UserJoined  :: WsTag UserId
  PriceUpdate :: WsTag (Map Ticker Double)
  ServerError :: WsTag ErrorCode

Now you can write:

ChatMessage :=> Identity "hello"       -- DSum WsTag Identity
PriceUpdate :=> Identity priceMap      -- same type, different payload

One type, heterogeneous contents, zero runtime casts. The type system guarantees that if the key is ChatMessage, the value is Text. Period.

DMap: The Heterogeneous Map

dependent-map extends this to a full map data structure:

insert ChatMessage (Identity "hello")
  $ insert PriceUpdate (Identity priceMap)
  $ empty

One map holding Text and Map Ticker Double, fully type-safe. Try putting those in a Map k v — you can't, because v must be a single type.

DMap is internally a balanced binary tree, ordered by GCompare — a GADT-aware version of Ord. This is where dependent-sum-template comes in: it generates the boilerplate GEq, GCompare, and GShow instances via Template Haskell, so you write three lines instead of quadratic pattern match cases.

fan/select: Where It Gets Wild

Here's the core Reflex API that uses all of this:

fan    :: GCompare k
       => Event t (DMap k Identity)
       -> EventSelector t k

select :: EventSelector t k
       -> k a
       -> Event t a

fan takes a single event stream carrying a DMap (a heterogeneous bundle of values) and returns an EventSelector. Then select extracts individual typed streams by their GADT key:

handleWebsocket :: Event t (DMap WsTag Identity) -> m ()
handleWebsocket wsEvent = do
  let sel = fan wsEvent

  let chats  = select sel ChatMessage   -- Event t Text
  let joins  = select sel UserJoined    -- Event t UserId
  let prices = select sel PriceUpdate   -- Event t (Map Ticker Double)
  let errors = select sel ServerError   -- Event t ErrorCode

  chatLog   <- foldDyn (:) [] chats
  userCount <- count joins
  ...

Each downstream Event is perfectly typed. No pattern matching on sum types. No fromJust. No runtime errors. If you accidentally wire chats into something expecting UserId, the compiler stops you.

The Performance Trick

fan doesn't eagerly split anything. Internally, EventSelector holds a reference to the parent event and a DMap of subscribers. When you call select sel ChatMessage, it registers interest in that key. If nobody ever calls select sel PriceUpdate, that branch has zero cost — events for that key are simply dropped.

This is how Reflex handles thousands of DOM elements efficiently. The DOM itself is a massive heterogeneous event source — clicks produce coordinates, inputs produce text, scrolls produce offsets. fan and select route them with type safety and lazy subscription, so you only pay for what you use.

The Deeper Insight

What Reflex has done is build a type-level routing table for events. Your entire event network is verified at compile time. Wrong connections are type errors, not runtime bugs. This is genuinely dependent typing in production Haskell — the value type depends on the key value — achieved without any language extensions beyond GADTs and existentials.

This is also why Reflex code has that distinct feeling of "if it compiles, it works." The type system isn't just checking shapes — it's checking the semantics of your event wiring. Every select call is a proof that the downstream consumer expects exactly the type that the upstream producer emits.

The next time you see dependent-sum and dependent-map in your build output, know that you're looking at the foundation of one of the most sophisticated uses of Haskell's type system in any production framework. And unlike academic dependent type systems, this one ships real applications.