Getting dangerously close to becoming an “ML module guy”
Conversation
What if the typeclasses… were bad
4
1
8
yes, yes,
…but still can I have something like modular implicits or instance arguments?
1
3
The programmer can have a little modular implicits, as a treat
1
3
yes, I like treats!
1
3
just kind of a mistake to make me try to make a main course out of the treat imo (as much as I like them)
1
3
Moving out of shitposting mode for a sec, my main gripe with typeclasses is that global coherence rarely makes sense for “good” typeclasses, and wrapping everything in a pile of newtypes, calling a function, then unwrapping is a lot of ceremony!
2
4
Also, they conflate a bunch of notions that _ought_ to be distinct, namely syntax + dynamic dispatch
Like, do notation is hardwired to Monad, even though it still makes sense when we have monad-ish things that aren’t Monad on the nose
2
4
Leans situation with Additive/Multiplicative Groups is another example here. By tying overloaded syntax to dynamic dispatch, we end up in all sorts of weird places
3
3
If we zoom out, instance resolution is kinda just a limited form of program synthesis, where all we can do is synthesize records of functions with really specific rules. What if we broadened our horizons here, and opened up the door to broader, user programmable synthesis?
2
3
Agda has _some_ support for this with tactic arguments, and it’s super useful. I’m definitely interested in seeing how far one can push this though :)
1
2
Show replies