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

前端之家收集整理的这篇文章主要介绍了haskell – 我可以从功能依赖中提升类型的平等吗?前端之家小编觉得挺不错的,现在分享给大家,也给大家做个参考。
我想要获得一些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。我使用这种技术,并且已经广泛尝试,并没有能够写出矛盾。不是说这是不可能的,但至少是非常困难和罕见的边缘案例。

原文链接:https://www.f2er.com/javaschema/282170.html

猜你在找的设计模式相关文章