proof irrelevance vs computation irelavance

Stream: new members

[John Ericson]

Does anyone know a good paper on this?

For systems more concerned with runtime performance and less with proving things, I've seen a more modality-based than kind-based approach, where the RHS of typing judgements is always fine with erased items.

They key difference seems to be "actually has 0 or 1 inhabitants" vs "merely not allowed to destinguish at runtime.

I know of papers that talk about each of these in isolation, but not both at once.

[John Ericson]

Ah, I guess Agda has both kinds these days. Well, that's a place to start.