3 ms·
> 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...
by localghost3000 2y 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 2y agoHere'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.