Haskell:函数依赖的非明显示例
我见过的函数依赖的例子归结为映射容器 -> 。元素和参数 ->结果
(如Mult Matrix Vector Vector
)。它们似乎用类型函数更好地表达。在数据库理论中,更复杂的关系被认为不是这种形式(例如a -> b,b -> a
)。
Haskell 中是否存在无法使用类型函数很好地编写 FD 用法的示例?
The examples of functional dependencies I've seen boil down to mapping container -> element
, and arguments -> result
(as in Mult Matrix Vector Vector
). They seem to be better expressed with type functions. In database theory, more complex relationships are considered that are not of this form (like a -> b, b -> a
).
Are there examples of usage of FDs in Haskell that cannot be nicely written using type functions?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
正如 Manuel Chakravarty 解释,类型函数和函数依赖关系具有大致相同的表达能力,您可以将一种表述转换为另一种表述。仅当您查看与其他语言扩展(例如 GADT 或 UndecidableInstances)的交互时,它们才开始有所不同。我认为类型族目前在 GHC 中更受青睐,因为它们与 GADT 和存在类型的交互要简单得多。
As Manuel Chakravarty explains, type functions and functional dependencies have roughly the same expressiveness, you can translate one formulation into the other. They only begin to differ when you look at interaction with other language extensions like GADTs or UndecidableInstances. I gather that type families are currently favored for implementation in GHC because their interaction with GADTs and existential types is substantially simpler.
正如 Heinrich Apfelmus 已经说过的那样,MPTC+FunDeps 和单独的 TF 是等效的。当它们与其他扩展结合使用时,特别是与重叠实例结合时,就会出现差异。当允许重叠时 TF 不健全,而 FunDeps 允许重叠。例如,使用 FunDeps 很容易实现类型相等:
这里的关键点是重叠。原则上,可以在不重叠的情况下实现类型相等,但需要编译器支持。 Oleg 在此处描述了该方法: http://okmij.org/ftp/Haskell/typeEQ.html
PS 在 haskell 上有冗长的讨论 - 有关此主题的主要邮件列表。
As Heinrich Apfelmus already said MPTC+FunDeps and TF alone are equivalent. Differences arise when they are combined with other extensions in particular with overlapping instances. TF are unsound when overlapping is permitted while FunDeps allow overlapping. For example it's easy implement type equality with FunDeps:
Key point here is overlapping. In principle it's possible to implement type equality without overlapping but it will require compiler support. That approach is described by Oleg here: http://okmij.org/ftp/Haskell/typeEQ.html
P.S. There was lengthy discussion on haskell-prime mailing list on this subject.