haskell - 使用一些 `unsafeCoerce` 用例避免 `Coercible`

Question

在 Coercible 的当前实现中我们可以量化“代表性保留类型构造函数”，以在下面的代码中提取更安全的证明

#!/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)

Answer 1

有点。您可以使用您在实例中使用的相同量化约束技巧:

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

这种意外限制了 p到那些在正确位置具有代表性作用的类型。我认为没有一种直接的方法可以准确地编写该限制。无论如何，在更改之后，替换 unsafeCoerce与 coerce在您现有的实例中工作正常。为了证明这实际上是可调用的，在 ghci 中:

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

快速复习一下类型应用规则:第一个类型参数对应于 a ，第二个到 b ，第三个到 p .