When discussing Void
on Haskell Libraries mailing list, there was this remark:
Back in the day it used to be implemented by an
unsafeCoerce
at the behest of Conor McBride who didn't want to pay for traversing the wholeFunctor
and replacing its contents, when the types tell us that it shouldn't have any. This is correct if applied to a proper Functor, but subvertible in the presence of GADTs.
The documentation for unsafeVacuous
also says:
If
Void
is uninhabited than anyFunctor
that holds only values of the typeVoid
is holding no values.This is only safe for valid functors that do not perform GADT-like analysis on the argument.
How would such a mischievous GADT Functor
instance look like? (Using only total functions of course, without undefined
, error
etc.)
It's certainly possible if you're willing to give a Functor
instance that does not adhere to the functor laws (but is total):
{-# LANGUAGE GADTs, KindSignatures #-}
import Data.Void
import Data.Void.Unsafe
data F :: * -> * where
C :: F Void
D :: F a
instance Functor F where
fmap f _ = D
wrong :: ()
wrong = case (unsafeVacuous C :: F Int) of D -> ()
Now evaluating wrong
results in a run-time exception, even though the type-checker considers it total.
Because there's been so much discussion about the functoriality, let me add an informal argument why a GADT that actually performs analysis on its argument cannot be a functor. If we have
data F :: * -> * where
C :: ... -> F Something
...
where Something
is any type that isn't a plain variable, then we cannot give a valid Functor
instance for F
. The fmap
function would have to map C
to C
in order to adhere to the identity law for functors. But we have to produce an F b
, for unknown b
. If Something
is anything but a plain variable, that isn't possible.
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