Skip to content(if available)orjump to list(if available)

Making my life easier with GADTs

Making my life easier with GADTs

4 comments

·January 21, 2025
Visit

localghost3000

> They are often misrepresented presented as a futile toy for “galaxy-brain people”, providing no benefit to the regular programmer

Me: Go on I am listening...

> The backend I’m writing is just a program — written in Haskell — that takes as input the internal representation of Agda programs, and outputs λ□ programs. A compiler of sorts.

Me: <Closes laptop lid>

I am sure that theres something useful happening here, but it is definitely too galaxy-brain for this guy.

nyssos

Here's a less galactic version. Suppose you're implementing a binary tree where every leaf has to have the same height - a toy model of a self-balancing search tree.

Here's an implementation using GADTs and type-level addition

    data Node (level :: Nat) (a :: Type) where
        Leaf :: a -> Node Zero a
        Interior :: a -> (Node l a, Node l a) -> Node (l + 1) a
It's impossible to construct an unbalanced node, since `Interior` only takes two nodes of the same level, and every `Leaf` is of level 0.

kreyenborgi

Some follow-ups:

Making My Life Harder with GADTs https://www.parsonsmatt.org/2025/01/21/making_my_life_harder...

Making my life easier with two GADTs http://systema10.org/posts/making-my-life-easier-with-two-ga...

flupe

A little blog post on how, sometimes, a little bit of dependent types can make your life easier. For practical things.