我想要获得一些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的类型所表明的)实际上是真的。由于类型类的开放世界属性,您可以违反具有模块边界的资金。
原文链接:https://www.f2er.com/javaschema/282170.html这通过以下示例显示。这段代码只用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。我使用这种技术,并且已经广泛尝试,并没有能够写出矛盾。不是说这是不可能的,但至少是非常困难和罕见的边缘案例。