Every time I see a post like this I get really excited, wonder how far along we are, realize I still don’t understand the roadmap to DT, try to read a paper about it (usually Eisenberg’s roadmap) and give up. But I like reading the reactions of people who get it.
“We” seem to be very much still in the minutiae. All I perceive so far is a lot of work going in to supporting putting types in expressions, without taking advantage of the type herald to disambiguate. Then development could get on to what we can do with types in expressions.
On the topic of impenetrability: can I ask why atravers’ whimsical comment got flagged?
To add something to the topic: Dependent Haskell is an incredible engineering effort. You can tell by witnessing all these incremental changes to an industrial-strength compiler. I’m very glad that Vlad is pushing GHC ever further towards ergonomic, first class use of types. I think his work will become more exciting once all the syntax has been fixed, at which point we can finally talk semantics and supersede type families. All the more reason to laud Vlad’s stamina! We should try to support him on this odyssey however we can.
23 Likes
Hear hear! I love everything that’s coming out of the Dependent Haskell efforts. Every release gives me some way of expressing something more clearly, that I could previously only encode awkwardly. I’d also like to celebrate the efforts of @sand-witch who is working on this too.
13 Likes
Hello, this is my first time posting in this community, but I’ve been following this sequence of work on DH and just wanted to mention that I appreciate @sand-witch and @int-index for these blog posts too-- clearly written and a pleasure to read. Please keep it up!
12 Likes