haskell – 我可以从功能依赖中提升类型的平等吗？

发布时间：2020-12-14 04:30:58 所属栏目：百科来源：网络整理

导读：我想要获得一些MultiParamTypeClasses和FunctionalDependencies的感觉，下面这个我觉得很明显的是尝试一下： {-# LANGUAGE MultiParamTypeClasses,FunctionalDependencies,TypeOperators #-}import Data.Type.Equalityclass C a b | a - bfob :: (C a b,C a

我想要获得一些MultiParamTypeClasses和FunctionalDependencies的感觉，下面这个我觉得很明显的是尝试一下：

{-# LANGUAGE MultiParamTypeClasses,FunctionalDependencies,TypeOperators #-}

import Data.Type.Equality

class C a b | a -> b

fob :: (C a b,C a b') => proxy a -> b :~: b'
fob _ = Refl

不幸的是，这不行; GHC不会从此上下文中得出b?b’。有没有办法使这项工作，或功能依赖不是“内部”可用？

我不认为这个事实(由fob的类型所表明的)实际上是真的。由于类型类的开放世界属性，您可以违反具有模块边界的资金。

这通过以下示例显示。这段代码只用GHC 7.10.3测试(在较旧的版本中大量破坏了底线 – 不知道会发生什么)。假设你可以实际执行以下操作：

module A 
  (module A,module Data.Type.Equality,module Data.Proxy
  )where 

import Data.Type.Equality
import Data.Proxy 

class C a b | a -> b 

inj_C :: (C a b,C a b') => Proxy a -> b :~: b' 
inj_C = error "oops"

然后还有几个模块：

module C where 
import A

instance C () Int 

testC :: C () b => Int :~: b 
testC = inj_C (Proxy :: Proxy ())

和

module B where 
import A

instance C () Bool 

testB :: C () b => b :~: Bool 
testB = inj_C (Proxy :: Proxy ())

和

module D where 

import A 
import B
import C 

oops :: Int :~: Bool
oops = testB

oops_again :: Int :~: Bool 
oops_again = testC

Int：?：Bool显然不是真的，所以通过矛盾，inj_C不能存在。

如果您不将C类从定义的模块导出，我相信您仍然可以安全地使用unsafeCoerce写入inj_C。我使用这种技术，并且已经广泛尝试，并没有能够写出矛盾。不是说这是不可能的，但至少是非常困难和罕见的边缘案例。

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!