2 ms·

Idris has implicit parameters: https://idris2.readthedocs.io/en/latest/tutorial/miscellany.html https://idris2.readthedocs.io/en/latest/tutorial/miscellany....

by sestep 3y ago

Idris has implicit parameters: https://idris2.readthedocs.io/en/latest/tutorial/miscellany.html https://idris2.readthedocs.io/en/latest/tutorial/miscellany.... As does Lean: https://lean-lang.org/lean4/doc/implicit.html https://lean-lang.org/lean4/doc/implicit.html Would yours look different from those, or is it the same idea?

gpderetta 3y ago
Thanks for the pointers. I'll read the details of these languages for inspiration. To be clear, I'm not inventing anything here, I found out about implicits from scala.
- sestep 3y ago
  Ah cool, I didn't realize Scala has them too!
  - naasking 3y ago
    I believe the Scala creators invented implicits, as an alternative to type classes that fit more naturally with an OOP language. They were later shown to be equivalent to type classes.