Are there any other examples of ML modules + overloading other than Scala's implicits and OCaml's modular implicits?
This Tweet is unavailable. Learn more
Conversation
Idris—in one respect it's interfaces/implementations look like Haskell type classes. There are no coherence guarantees though and they get plumbed when in scope (ala implicits). With named implementations, you can be explicit and I _think_ they amount to first class modules also.
1
2
Agda has its instance arguments thingy, but I haven't seen it used all that much in the wild. Coq is in a similar boat. Lean has non-canonical typeclasses too.
2
1
Would actually be interested to see more examples of Agda's instance arguments in use - I found the docs abit hard to make head-or-tail of 🙄 - anyone know of any?