See this section of the docs: docs.idris-lang.org/en/latest/tuto
Conversation
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.
1
1
Maybe we could church encode it? But I don't really think anyone wants to use something like that 😂
1
If you were asking for something simpler, that is. Depends on what your definition of 'simple' is though.