我可以通过功能依赖来实现类型相等吗？

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。我已经使用了这种技术，并进行了广泛的尝试，但无法写出矛盾。并不是说这是不可能的，但至少非常困难并且是罕见的边缘情况。unsafeCoerceC