On the Agda mailing list, Conor McBride asked:
is there any way to get hold of operations like a putative
trustFromJust :: Maybe x -> x
which doesn't actually check for Just and Goes Wrong (in Milner's sense) if fed Nothing?
Agda might prove Maybe a == Just1 a, and the intermediate constructor for the sum type could be eliminated.
I can think of approaches using unsafeCoerce# or unpackClosure#, but does anyone else have thoughts?
import GHC.Prim
trustFromJust :: Maybe x -> x
trustFromJust x = y
where Just1 y = unsafeCoerce# x
data Just1 a = Just1 a
though this segfaults (single constructor types can avoid some of the closure overhead). The core looks ok though:
main2 =
case (Data.Maybe.Just @ Type.Integer main3)
`cast`
(CoUnsafe
(Data.Maybe.Maybe Type.Integer)
(Just1 Type.Integer)
:: Data.Maybe.Maybe Type.Integer
~
Just1 Type.Integer)
of _ { Just1 y_aeb ->
$wshowsPrec 0 y_aeb ([] @ Char)
Since this is a research question, we've got a few possible ways forward, but they all come down to:
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With