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
Brendan Zabarauskas
@brendanzab
Replying to
@CatTyped
@freebroccolo
and 4 others
Here it is: youtube.com/watch?v=9v4_FQ - not sure it's been published anywhere though. If I understand well enough, it allows you to have more control over what is erased at run-time. Still getting my head around this stuff too, and it might be obsoleted by cubical types… 🤷‍♂️
youtube.com
Conor McBride - Worldly Type Systems
Talk given at UNSW, 3 May 2016.
Twitter Web Client
1
Like