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
I remember agda-prelude is where you must look to find agda + implicits.
1
2
Meant instance arguments, sorry, as the README says. Monads:
github.com/UlfNorell/agda
Maybe with instances:
github.com/UlfNorell/agda
1
Yeah – the terminology has been annoyingly muddied by Scala's implicit arguments, which aren't what is meant by Coq, Agda, and Idris's implicit args. 😭