haskell - 我可以从函数依赖中魔术出类型相等吗？

Question

我正在尝试了解 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'从那个背景来看。有什么方法可以使这项工作，或者功能依赖不是“内部”可用的？

Answer 1

我不认为这个事实(如 fob 的类型所述)实际上是正确的。由于类型类的开放世界属性，您可以违反带有模块边界的fundep。

以下示例显示了这一点。这段代码只用 GHC 7.10.3 测试过(fundeps 在旧版本中被大量破坏 - 不知道会发生什么)。假设您确实可以实现以下内容:

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不可能存在。

相信你还是可以放心写 inj_C与 unsafeCoerce如果你不导出类 C从定义它的模块。我已经使用过这种技术，并且已经广泛尝试，但无法写出矛盾。并不是说这是不可能的，但至少非常困难和罕见的边缘情况。