Comment by localghost3000 | Hacker News Reader

Comment by localghost3000 | Hacker News Reader

Parent Full thread

> 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.

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.

Reply on news.ycombinator.com