Closed RyanGlScott closed 4 years ago
Actually, you don't even need to use error "unreachable"
. This also works:
instance ProfunctorComonad TambaraSum where
proextract (TambaraSum p) = dimap Left port p
where
port :: Either a Void -> a
port = either id absurd
I like this solution even more. Patch incoming.
I discovered recently that
profunctors
will emit warnings when built with-Wincomplete-uni-patterns
:Each
-Wincomplete-uni-patterns
violation is of a similar nature: GHC is expecting something of typeforall a. Either a b0 -> a
(whereb0
is a skolem type variable quantified by a rank-n field, such as the field in theTambaraSum
constructor), soprofunctors
cuts corners and just uses a quick-and-dirty(\(Left a) -> a)
solution. Under most cirumstances, it would be impossible for a function of typeforall a. Either a b0 -> a
to ever haveRight
as an argument, but this is possible in Haskell due to⊥
. Here is an example that shows where things go wrong:Unsurprisingly, this program will throw an error at runtime. What is surprising is the exact error it throws. Rather than throwing a
"boom"
error, this program will fail due toproextract
not being exhaustive:One way to avoid this is to tweak
proextract
and friends so that it defines a case forRight
. For example, here is what a repaired version ofproextract
might look like:The only way to supply
port
with a non-Left
argument is to pass it⊥
orRight ⊥
, andport
's definition ensures that the bottoms are evaluated in either case. Now the original program will throw a"boom"
error, as expected: