Of course Idris' erasure works, and works really well. It reduced my O(n) singly-linked lists down to O(1) with this one weird trick
-
-
Replying to @lenary
If you're wondering, the weird trick was deciding all the data was unused and just leaving it out entirely.
2 replies 0 retweets 3 likes -
Replying to @lenary
If you're wondering, erasure is *really* hard, and this was a FFI case where Idris had no way of knowing how I was using the data.
1 reply 0 retweets 0 likes
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.