Mastodon Feed
dysfun@treehouse.systems ("gaytabase") wrote:
idris has a world type which is runtime irrelevant and used to sequence I/O.. or to sequence linear I/O.
now isn't that a strange thing? we can linearly bind it to enforce the sequentiality, but we want it to be erased too. the normal erasure mechanism is multiplicity 0, which we're not using, because we're already using multiplicity 1. and so we rely on the world token being hacked up in the compiler to get the best of both worlds.
or perhaps linearity and erasure are more orthogonal in reality than the (admittedly nice) semiring of 0, 1, many.