avoid `unsafeCoerce` with some `Coercible` use case

user_242189 0
Viewed 94

In the current implementation of Coercible can we quantify over "representational preserving type constructors", to extract a safer proof in the code below

#!/usr/bin/env stack
-- stack --resolver lts-17.10 script
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module SOQuestionCoercibleInstances0 where

import Data.Coerce
import Data.Constraint
import Data.Kind
import Data.Type.Equality as EQ
import Data.Typeable
import Unsafe.Coerce

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
newtype Id0 a = Id0 {unId0 :: a} deriving (Show)

newtype Id ef a = Id {unId :: ef a}

instance (forall x. (Coercible x (ef x))) => IsomorphismFromTo (Id0 a) (Id0 (ef a)) where
  isofromto (pa :: p (Id0 a)) = unsafeCoerce pa

a = Id0 (7 :: Int)

--- >>> show a
--- >>> show (to a :: Id0 (Id0 Int))
-- "Id0 {unId0 = 7}"
-- "Id0 {unId0 = Id0 {unId0 = 7}}"
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
main :: IO ()
main = do
  print a
  print (to a :: Id0 (Id0 Int))

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
class IsomorphismFromTo a b where
  isofromto :: forall p. p a -> p b
  to :: a -> b
  default to :: IsomorphismFromTo a b => a -> b
  to = unId0 . isofromto . Id0
  from :: b -> a
  default from :: IsomorphismFromTo a b => b -> a
  from = r isofromto
    where
      r :: (forall p. p a -> p b) -> b -> a
      r to = let (Op f) = to @(Op (->) a) (Op id) in f

type Op :: (* -> * -> Type) -> * -> * -> Type
newtype Op m a b = Op (m b a)
haskell
2 Answers

Sort of. You can use the same quantified constraint trick you used in your instance:

class IsomorphismFromTo a b where
  isofromto :: forall p. (forall a b. Coercible a b => Coercible (p a) (p b)) => p a -> p b

This sort of accidentally restricts p to those types that have a representational role in the right place. I don't think there's a direct way to write that restriction exactly. Anyway, after that change, replacing unsafeCoerce with coerce in your existing instance works fine. And just to demonstrate that this is actually callable, in ghci:

> isofromto @(Id0 Int) @(Id0 (Id0 Int)) @Id0 (Id0 (Id0 3))
Id0 {unId0 = Id0 {unId0 = Id0 {unId0 = 3}}}

For a quick refresher on type application rules: the first type argument corresponds to a, the second to b, and the third to p.

user_7916040

We can not allow that without making the type system unsafe.

Assume we have a safe way to obtain

hp :: forall a b. Coercible a b => forall p. p a -> p b
hp = unsafeCoerce  -- assume a safe way to do this exists

Then we can prove these two types equal:

data A
newtype B = B A

lemma1 :: A :~: B
lemma1 = hp Refl

Now we can exploit these two types to define a type-level conditional, and wrap it under a newtype for convenience:

type family If w t e where
   If A t e = t
   If B t e = e

newtype IF w t e = IF {unIF :: If w t e}

We prove a pair of trivial lemmas:

lemma2 :: forall a b t e. a :~: b -> IF a t e -> IF b t e
lemma2 Refl = id

lemma3 :: IF A t e -> IF B t e
lemma3 = lemma2 lemma1

And finally we implement unsafeCoerce:

unsafeCoerce' :: t -> e
unsafeCoerce' = unIF . lemma3 . IF

Conclusion: if we can achieve a (total) implementation of hp, we can also break the type system implementing unsafeCoerce. Therefore, assuming the safety of the type system in the "safe" fragment of Haskell (without unsafe functions), we can not within said fragment implement hp.

Note that the whole point of having newtype B = B A is to create a distinct type B which is isomorphic to A. Since it is distinct, we can define separate instances for A and B, we can have type families distinguish between them, and so on. This copes with the ability of proving equality between them: if we are able to prove GADT-equality A :~: B or Leibniz equality forall p. p A -> p B we are then able to break the rest of the type system which instead relies on this types being distinct.

It looks like you are trying to force Haskell to behave as if it were a structural type system, or even one working up to isomorphism (maybe one inspired from HoTT and univalence). However, Haskell's type system is nominal, and we can't simply take a "quotient" on coercible types without breaking it.

user_32349590
Related