Sure, I'd imagine so! I recall saying that Idris can do "ML modules" using Idris' interface facility (which is kind of like a type class and/or modular implicit). I think there's a paper in the works.
This Tweet is unavailable. Learn more
Conversation
Oh really! I was thinking that Idris had coherent type classes - this is nice news!
I think they were mostly modelled after Scala's implicit mechanism (but Agda has something similar). I let Edwin know one time about "Type classes versus the world" and he didn't seem too bothered :)
1
1
The tricky thing is whether you can use them like ML modules. That's how the modular implicits paper proposes getting around the 'set problem'.
1
1
Show replies