Conversation

Brendan Zabarauskas
@brendanzab
Wondering if you can use interfaces as parameters in Idris, rather than just in constraints (ie. instance arguments in Agda-speak) 🤔 - bleh, I hate that Scala went with 'implicit arguments' for something related but different. Makes things so confusing.
2
Brendan Zabarauskas
@brendanzab
Now what I'd like is to be able to be confident that those instance records aren't passed around at run time - to get static dispatch like in Rust. Maybe McBride's worldly typed thingy could help? 🤔
1
CatTyped
@CatTyped
Does something else exist that is similar in function to modules and type classes, but doesn't use a separate language from values and types?
1
Brendan Zabarauskas
@brendanzab
Check out the other threads under this tweet. You can unify the concepts by using records. 1ML does this in part, but if you really want associated types you need to go dependently typed. You also want a way to pass those records implicitly. See Agda's "instance arguments".
1
Show replies