welp, I guess I'm writing Haskell in Coq... with monad transformers and everything. 🤖
Conversation
before anyone asks, these all should have been `Require Import`s or `Import`s. 🙄
2
it's *very* neat how much of Haskell idioms can directly translate to Coq, because of how effectively coq-ext-lib uses the notation system.
You can do `... <$> ... <*> ...` chains as well!
2
1
9
The 64 k$ question: does the lack of coherence in Coq get in the way?
I think I run into it a few times per week...
2
What kind of issues do you face? People not defining types with instances tags? eg. hashmaps with the ord instance used to construct it? Or is it about being confused about what instances are in scope?
Usually, a proof fails because a function picks an instance and lemmas in another file pick a different instance. But also: bind different instances in the same lemma accidentally. Or inference picks a random instance instead of generalizing (Haskell) or giving an error (Scala).
2
OTOH, maps are a bad motivation — in fancy not-Haskell languages (ML, Scala(?), Coq/Agda/Idris), that is ones with enough dependent types, two maps with different orderings can have different types, tho convenience is an open question.
2