Mastodon Feed
dysfun@treehouse.systems ("gaytabase") wrote:
what is erasure anyway? it's not the same thing as const. they both imply being known at compile time, but const also implies some runtime presence, whereas erased implies no runtime presence. this makes it perfect for proofs that should be checked during compilation but we don't want to have to check at runtime.
the common case everybody wants of course is generics. are these const or erased? i guess that depends on how you feel about reifying types at runtime.
now, many dependently typed systems choose to have a Prop universe, for runtime irrelevant data. what the world token buys you is not having to have a Prop universe. why is that a problem? imagine we see something used to the right of a colon. it used to be that meant it was a Type, but now it could also be a Prop. so what do you do, assume it's a Type unless they annotate it as a Prop? try both?
by hardcoding the very short list of all types that are erased into the compiler, you don't suffer this problem.
idris 1 had a universe of uniqueness types. not sure what it did about inferring them, probably assume it was a Type unless told otherwise.