Raise proves the law of the excluded middle (well,...

# arrow

[Youssef Shoaib [MOD]]

Raise proves the law of the excluded middle (well, something equivalent to it anyway)!

inline fun <A> doubleNegationElimination(block: ((A) -> Nothing) -> Nothing): A = merge { block(this::raise) }

For more info
Bonus: suspend allows the same thing (which is precisely why early raise builders were made using suspend magic):

suspend fun <A> doubleNegationElimination(block: suspend (suspend (A) -> Nothing) -> Nothing): A = suspendCoroutine { cont ->
    block.startCoroutine({ value ->
        suspendCoroutine<Nothing> {
            cont.resume(value)
        }
    }, cont)
}

[simon.vergauwen]

Yes, it's a cool pattern sadly it comes with some strange side-effects on a language level..

[Youssef Shoaib [MOD]]

EDIT: I wrote this then noticed the pun 🤦🏼 I need more coffee...
Like what? It's fundamentally what allows Arrow to work, no?
Allowing this also allows suspend to work (a CPS transform is similar to a double-negation translation from classical logic to intuitionistic logic). This allows us access to the "mother of all monads", which I consider a definite plus!