Conversation

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
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
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
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
Show replies