search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
903 stars 58 forks source link

[ fix ] `absurd` does not need a runtime argument #371

Closed gallais closed 3 years ago

gallais commented 4 years ago

absurd is called to dismiss impossible branches. If we ever start executing such a branch at runtime we have something to worry about.

Edit: one annoying thing is the fact that No absurd is now ill-typed because No expects a a -> Void function and not an 0 a -> Void one. Manual eta-expansion fixes the problem but it is a bit annoying. Is it still worth merging this PR in?

alebahn commented 3 years ago

I was wandering about this today and I found this PR. What would happen if Dec was changed to take a 0 a -> Void? What about making a separate version of absurd (Either adding an absurd0 that takes an erased argument or making an absurd' that accepts a unrestricted argument).

gallais commented 3 years ago

What would happen if Dec was changed to take a 0 a -> Void

It would probably be annoying because that would mean that you cannot pattern-match on the a argument without the system complaining that you are not allowed to.

But now that I think about it, it may be possible to get away with

data Dec : Type -> Type where
  Yes : (prf : prop) -> Dec prop
  No  : (0 contra : (0 _ : prop) -> Void) -> Dec prop

and recover the ability to conveniently write No \case (...). We should try and see what happens.

alebahn commented 3 years ago

Actually, why is absurd used with No in the first place? No is looking for an a -> Void which is the type of uninhabited. Shouldn't that be used instead?

gallais commented 3 years ago

If I had to guess, I'd say it's because, being more polymorphic, absurd is usually more convenient to use and therefore what one reaches for in these situations.