No post body was provided.
Untitled topic
1–5 of 5 posts
Re: undefined
#2A little blog post on how, sometimes, a little bit of dependent types can make your life easier. For practical things.
Re: undefined
#3Some 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...
Re: undefined
#4> 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:
I am sure that theres something useful happening here, but it is definitely too galaxy-brain for this guy.
Re: undefined
#5> 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: I am sure that theres something useful happening here, but it is definitely t…
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