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.
8 Likes
This post was flagged by the community and is temporarily hidden.
“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?
I had nothing to do with the decision, but I think it is good that it has been flagged.
Note that anyone can still read the comment and chuckle if they feel like it. However, it adds nothing to the topic, arguably spreads FUD (“make Agda lazy” is inaccurate on a few levels) and has the potential to derail it. (Just like this answer, in fact. I would be fine if our discussion were broken out or hidden.)
Flagging the comment as such ensures that people do not engage.
2 Likes
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.
9 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.
4 Likes