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.
Conversation
Seems you can - I just can't figure out how to access the 'compare' field:
1
Got it!
1
1
See this section of the docs: docs.idris-lang.org/en/latest/tuto
1
1
2
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
2
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
Well if you want that, just use records and functions:
Ord : Type -> Type = \a -> sig {
eq : Eq a,
compare : a -> a -> Ordering,
}
OrdUnit : Ord Unit = rec {
eq = EqUnit,
compare = \_ _ -> Equal,
}
1
That's pretty much what I was proposing at any rate.
Maybe we could church encode it? But I don't really think anyone wants to use something like that 😂
1
Show replies