undefined | Dark Hacker News

25 points by flupe 1 year ago

> 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 1 year ago | |

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 1 year ago |

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 1 year ago |

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