@edwinbrady @pigworker I know you guys will hate this but bear with me, please: If I basically turned off all runtime type erasure in Idris 2/QTT, would I then have enough RTTI for every value to do arbitrary, safe downcasts, like in a dynlang?
-
-
But typecas{e,t} can break normalization in System F (Girard, as I learn from https://plv.mpi-sws.org/semantics/2017/lecturenotes.pdf … Sec. 3.2 and you experts know better than me), is that fixed without normalization? Do proofs exist? /cc
@mietek -
What does "is that fixed" mean?
- 5 more replies
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.