时间戳

首页 > 解决方案 > 使用一些“Coercible”用例避免“unsafeCoerce”

haskell - 使用一些“Coercible”用例避免“unsafeCoerce”

问题描述

在当前的实现中，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)

标签： haskell

解决方案

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

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。

推荐阅读