Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Use of 'unsafeCoerce'

In Haskell, there is a function called unsafeCoerce, that turns anything into any other type of thing. What exactly is this used for? Like, why we would you want to transform things into each other in such an "unsafe" way?

Provide an example of a way that unsafeCoerce is actually used. A link to Hackage would help. Example code in someones question would not.

like image 450
PyRulez Avatar asked Apr 03 '14 19:04

PyRulez


3 Answers

unsafeCoerce lets you convince the type system of whatever property you like. It's thus only "safe" exactly when you can be completely certain that the property you're declaring is true. So, for instance:

unsafeCoerce True :: Int

is a violation and can lead to wonky, bad runtime behavior.

unsafeCoerce (3 :: Int) :: Int

is (obviously) fine and will not lead to runtime misbehavior.


So what's a non-trivial use of unsafeCoerce? Let's say we've got an typeclass-bound existential type

module MyClass ( SomethingMyClass (..), intSomething ) where

class MyClass x where {}

instance MyClass Int where {}

data SomethingMyClass = forall a. MyClass a => SomethingMyClass a

Let's also say, as noted here, that the typeclass MyClass is not exported and thus nobody else can ever create instances of it. Indeed, Int is the only thing that instantiates it and the only thing that ever will.

Now when we pattern match to destruct a value of SomethingMyClass we'll be able to pull a "something" out from inside

foo :: SomethingMyClass -> ...
foo (SomethingMyClass a) =
  -- here we have a value `a` with type `exists a . MyClass a => a`
  --
  -- this is totally useless since `MyClass` doesn't even have any
  -- methods for us to use!
  ...

Now, at this point, as the comment suggests, the value we've pulled out has no type information—it's been "forgotten" by the existential context. It could be absolutely anything which instantiates MyClass.

Of course, in this very particular situation we know that the only thing implementing MyClass is Int. So our value a must actually have type Int. We could never convince the typechecker that this is true, but due to an outside proof we know that it is.

Therefore, we can (very carefully)

intSomething :: SomethingMyClass -> Int
intSomething (SomethingMyClass a) = unsafeCoerce a    -- shudder!

Now, hopefully I've suggested that this is a terrible, dangerous idea, but it also may give a taste of what kind of information we can take advantage of in order to know things that the typechecker cannot.

In non-pathological situations, this is rare. Even rarer is a situation where using something we know and the typechecker doesn't isn't itself pathological. In the above example, we must be completely certain that nobody ever extends our MyClass module to instantiate more types to MyClass otherwise our use of unsafeCoerce becomes instantly unsafe.

> instance MyClass Bool where {}
> intSomething (SomethingMyClass True)
6917529027658597398

Looks like our compiler internals are leaking!


A more common example where this sort of behavior might be valuable is when using newtype wrappers. It's a fairly common idea that we might wrap a type in a newtype wrapper in order to specialize its instance definitions.

For example, Int does not have a Monoid definition because there are two natural monoids over Ints: sums and products. Instead, we use newtype wrappers to be more explicit.

newtype Sum a = Sum { getSum :: a }

instance Num a => Monoid (Sum a) where
  mempty = Sum 0
  mappend (Sum a) (Sum b) = Sum (a+b)

Now, normally the compiler is pretty smart and recognizes that it can eliminate all of those Sum constructors in order to produce more efficient code. Sadly, there are times when it cannot, especially in highly polymorphic situations.

If you (a) know that some type a is actually just a newtype-wrapped b and (b) know that the compiler is incapable of deducing this itself, then you might want to do

unsafeCoerce (x :: a) :: b

for a slight efficiency gain. This, for instance, occurs frequently in lens and is expressed in the Data.Profunctor.Unsafe module of profunctors, a dependency of lens.

But let me again suggest that you really need to know what's going on before using unsafeCoerce like this is anything but highly unsafe.


One final thing to compare is the "typesafe cast" available in Data.Typeable. This function looks a bit like unsafeCoerce, but with much more ceremony.

unsafeCoerce ::                             a ->       b
cast         :: (Typeable a, Typeable b) => a -> Maybe b

Which, you might think of as being implemented using unsafeCoerce and a function typeOf :: Typeable a => a -> TypeRep where TypeRep are unforgeable, runtime tokens which reflect the type of a value. Then we have

cast :: (Typeable a, Typeable b) => a -> Maybe b
cast a = if (typeOf a == typeOf b) then Just b else Nothing 
  where b = unsafeCoerce a

Thus, cast is able to ensure that the types of a and b really are the same at runtime, and it can decide to return Nothing if they are not. As an example:

{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE ExistentialQuantification #-}

data A = A deriving (Show, Typeable)
data B = B deriving (Show, Typeable)

data Forget = forall a . Typeable a => Forget a

getAnA :: Forget -> Maybe A
getAnA (Forget something) = cast something

which we can run as follows

> getAnA (Forget A)
Just A
> getAnA (Forget B)
Nothing

So if we compare this usage of cast with unsafeCoerce we see that it can achieve some of the same functionality. In particular, it allows us to rediscover information that may have been forgotten by ExistentialQuantification. However, cast manually checks the types at runtime to ensure that they are truly the same and thus cannot be used unsafely. To do this, it demands that both the source and target types allow for runtime reflection of their types via the Typeable class.

like image 187
J. Abrahamson Avatar answered Nov 06 '22 18:11

J. Abrahamson


The only time I ever felt compelled to use unsafeCoerce was on finite natural numbers.

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, StandaloneDeriving #-}

data Nat = Z | S Nat deriving (Eq, Show)

data Fin (n :: Nat) :: * where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

deriving instance Show (Fin n)

Fin n is a singly linked data structure that is statically ensured to be smaller than the n type level natural number by which it is parametrized.

-- OK, 1 < 2 
validFin :: Fin (S (S Z))
validFin = FS FZ

-- type error, 2 < 2 is false
invalidFin :: Fin (S (S Z))
invalidFin = FS (FS FZ)

Fin can be used to safely index into various data structures. It's pretty standard in dependently typed languages, though not in Haskell.

Sometimes we want to convert a value of Fin n to Fin m where m is greater than n.

relaxFin :: Fin n -> Fin (S n)
relaxFin FZ     = FZ
relaxFin (FS n) = FS (relaxFin n)

relaxFin is a no-op by definition, but traversing the value is still required for the types to check out. So we might just use unsafeCoerce instead of relaxFin. More pronounced gains in speed can result from coercing larger data structures that contain Fin-s (for example, you could have lambda terms with Fin-s as bound variables).

This is an admittedly exotic example, but I find it interesting in the sense that it's pretty safe: I can't really think of ways for external libraries or safe user code to mess this up. I might be wrong though and I'd be eager to hear about potential safety issues.

like image 44
András Kovács Avatar answered Nov 06 '22 17:11

András Kovács


There is no use of unsafeCoerce I can really recommend, but I can see that in some cases such a thing might be useful.

The first use that springs to mind is the implementation of the Typeable-related routines. In particular cast :: (Typeable a, Typeable b) => a -> Maybe b achieves a type-safe behaviour, so it is safe to use, yet it has to play dirty tricks in its implementation.

Maybe unsafeCoerce can find some use when importing FFI subroutines to force types to match. After all, FFI already allows to import impure C functions as pure ones, so it is intrinsecally usafe. Note that "unsafe" does not mean impossible to use, but just "putting the burden of proof on the programmer".

Finally, pretend that sortBy did not exist. Consider then this example:

-- Like Int, but using the opposite ordering
newtype Rev = Rev { unRev :: Int }
instance Ord Rev where compare (Rev x) (Rev y) = compare y x

sortDescending :: [Int] -> [Int]
sortDescending =  map unRev . sort . map Rev

The code above works, but feels silly IMHO. We perform two maps using functions such as Rev,unRev which we know to be no-ops at runtime. So we just scan the list twice for no reason, but that of convincing the compiler to use the right Ord instance.

The performance impact of these maps should be small since we also sort the list. Yet it is tempting to rewrite map Rev as unsafeCoerce :: [Int]->[Rev] and save some time.

Note that having a coercing function

castNewtype :: IsNewtype t1 t2 => f t2 -> f t1

where the constraint means that t1 is a newtype for t2 would help, but it would be quite dangerous. Consider

castNewtype :: Data.Set Int -> Data.Set Rev

The above would cause the data structure invariant to break, since we are changing the ordering underneath! Since Data.Set is implemented as a binary search tree, it would cause quite a large damage.

like image 2
chi Avatar answered Nov 06 '22 18:11

chi