@edwinbrady Does Idris have or plan to have anything similar to Coercible and type roles, or have you given it any thought?
(I was thinking about the problem of intrinsically typed de Bruijn *levels*, and thought this may be part of the solution... I'm not sure if it would be!)
-
-
Uh oh. I can't remember where my own knowledge of these originates. I'll get back to you in a moment...
-
A bunch of relevant material seems to be linked from here: https://ghc.haskell.org/trac/ghc/wiki/Roles … I think I originally read the "Generative Type Abstraction" paper, but this one might be more directly relevant: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/coercible.pdf … (the link to that on the wiki is broken)
- 1 more reply
New conversation -
-
-
My first reaction to this sort of question is often "maybe it can already do that" though :)
-
Yes it's entirely possible that that's the answer, I only just started playing around with Idris a few days ago. :)
- 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.