我可以通过函数依赖来提升类型相等吗？ [英] Can I magic up type equality from a functional dependency?

问题描述

我尝试了解 MultiParamTypeClasses 和 FunctionalDependencies ，以下内容让我觉得很明显要试一下：

  { - ＃LANGUAGE MultiParamTypeClasses 
，FunctionalDependencies 
，TypeOperators＃ - } 
 
导入Data.Type.Equality 
 
 class C ab | a  - > b 
 
 fob ::（C a b，C a b'）=>代理a  - > b：〜：b'
 fob _ = Refl 
  

不幸的是，这不起作用; GHC不会从该上下文中得出 b〜b'。有没有什么办法可以做到这一点，或者是不是内部可用的函数依赖？ 我不认为这个事实（正如 fob 类型所述）实际上是真实的。由于类型类的开放世界属性，您可以违反模块边界的fundep。

以下示例显示了这一点。此代码仅在GHC 7.10.3中进行了测试（fundeps在旧版本中大量破解 - 不知道会发生什么）。假设您确实可以执行以下操作：

 模块A 
（模块A 
，模块数据。 Type.Equality 
，模块Data.Proxy 
）其中
 
导入Data.Type.Equality 
导入Data.Proxy 
 
 class C ab | a  - > b 
 
 inj_C ::（C a b，C a b'）=>代理a  - > b：〜：b'
 inj_C =错误oops
  

然后再添加几个模块：

 模块C其中
导入A 
 
实例C（）Int 
 
 testC :: C（）b => Int：〜：b 
 testC = inj_C（Proxy :: Proxy（））
  

和

 模块B其中
导入A 
 
实例C（）Bool 
 
 testB :: C（）b => b：〜：Bool 
 testB = inj_C（Proxy :: Proxy（））
  

和

 模块D其中
 
导入A 
导入B 
导入C 
 
 oops :: Int：〜：Bool 
 oops = testB 
 
 oops_again :: Int：〜：Bool 
 oops_again = testC 
  

Int：〜：Bool 显然不是真的，所以相反， inj_C 不能存在。

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

I'm trying to get some sense of MultiParamTypeClasses and FunctionalDependencies, and the following struck me as an obvious thing to try:

{-# 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

Unfortunately, this doesn't work; GHC does not conclude b ~ b' from that context. Is there any way to make this work, or is the functional dependency not "internally" available?

解决方案

I don't think this fact (as stated by the type of fob) is actually true. Due to the open world property of type classes, you can violate the fundep with module boundaries.

This is show by the following example. This code has only been tested with GHC 7.10.3 (fundeps were massively broken in older versions - don't know what happens then). Assume that you can indeed implement the following:

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"

Then a few more modules:

module C where 
import A

instance C () Int 

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

and

module B where 
import A

instance C () Bool 

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

and

module D where 

import A 
import B
import C 

oops :: Int :~: Bool
oops = testB

oops_again :: Int :~: Bool 
oops_again = testC 

Int :~: Bool is clearly not true, so by contradiction, inj_C cannot exist.

I believe you can still safely write inj_C with unsafeCoerce if you don't export the class C from the module where it's defined. I've used this technique, and have extensively tried, and not been able to write a contradiction. Not to say it's impossible, but at least very difficult and a rare edge case.

这篇关于我可以通过函数依赖来提升类型相等吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！