类型推断如何在存在功能依赖性的情况下工作

Question

请考虑以下代码:

{-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts  #-}
class Foo a c | a -> c
instance Foo Int Float 
f :: (Foo Int a) => Int -> a 
f = undefined

现在,当我在ghci中看到f的推断类型时

> :t f
> f :: Int -> Float

现在如果我添加以下代码

g :: Int -> Float 
g = undefined 

h :: (Foo Int a) => Int -> a 
h = g

我收到了错误

Could not deduce (a ~ Float)

我无法理解这里发生了什么？限制Foo Int a应该限制hto 的类型,Int -> Float如推断类型所示f.

是因为在解析实例之前发生了类型统一吗？

[更新]

Dan Doel在咖啡馆邮件列表中给出的解释

我相信,答案是fundep实现和类型系列之间的区别是局部约束信息.Fundeps没有本地传播.

因此,在您的第一个定义中,您已在本地提供' Int -> a',这是GHC可接受的.然后它从外部计算出(Foo Int a) => Int -> a"实际上"的功能Int -> Float.

在第二个定义中,你试图给' Int -> Float',但是GHC只在本地知道你需要提供' Int -> a'带有约束' Foo Int a',它不会用来确定它a ~ Float.

这不是fundeps所固有的.人们可以制作一个具有局部约束规则的fundeps版本(通过转换为新类型系列的东西很容易).但是,差异也是为fundep而不是类型系列支持重叠实例的原因.但我现在不会接受这一点.

我还是不明白这是什么意思.所以仍然在寻找更好的理解答案.

Answer 1

为了避免这个问题，您可以使用类型族：

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}

class Fooo a where
  type Out a :: *

instance Fooo Int where
  type Out Int = Float
  
ff :: (Foo Int) => Int -> (Out Int)
ff = undefined

gg :: Int -> Float
gg= undefined

hh :: (Foo Int) => Int -> (Out Int)
hh = gg

类型家庭都很好。尽可能使用类型族！

我猜你的错误是因为 ghc 可以f :: Int -> Float从f :: Foo Int a => Int -> a你的类定义和实例中推断出来，但它不能g :: Foo Int a => Int -> a从g:: Int -> Float.

将约束视为函数上的秘密字典参数是很方便的。f 中有一种固有的但受限制的多态性，而 g 中没有。

我认为注意到 ghci 给我们提供的错误消息与我们尝试定义的错误消息基本上完全相同是有帮助的

j :: Int -> Float
j = undefined

k :: Eq a => Int -> a
k = j

显然，这不应该起作用，因为我们知道k它的第二个参数应该是受限多态的。ghc 尝试将类型Int -> a与匹配Int -> Float并失败，抱怨它无法a ~ Float从上下文中推断Eq a，即使有一个实例Eq Float。在您的示例中，它表示即使存在 的实例，也无法a ~ Float从上下文中推断。我意识到我们可以推断出只有一种可能的类型，但是通过为 Foo 创建类和实例，您已经定义了一个关系并断言它是函数依赖。这与定义函数不同（这就是类型族解决问题的原因 - 它定义了函数）。Foo Int aFoo Int Floata

当你写的时候 ghc 也会抱怨

aconst :: (Foo Int a) => a
aconst = 0.0

甚至

anotherconst :: (Foo Int a) => a
anotherconst = 0.0::Float

总是因为它无法将它想要的约束多 a态与您给它的特定类型（Fractional a或Float）相匹配。

你要

forall a.Foo Int a

与 属于同一类型Float，但事实并非如此。只有一种类型满足forall a.Foo Int a， 它Float，所以 ghci 可以采用f::forall a.(Foo Int a)=>a->Float并推断（使用 Foo 的字典）f::Int->Float，但你期望 ghci 采取Float并发现注意它是forall a.Foo Int a，但没有 Float 的字典，它是一种类型，而不是一个类型类。ghci 可以以一种方式做到这一点，但不能以另一种方式做到这一点。

Dan 关于本地信息的观点是 ghc 必须同时使用 的Foo定义和实例来推断Float可以重写forall a.(Foo Int a)，并且在编译的这一点上，ghc 不使用全局信息，因为它只是试图做一个匹配。我的观点是Float匹配forall a.(Foo Int a)但forall a.(Foo Int a)不匹配Float，即"this"匹配模式(x:xs)但(x:xs)不匹配模式"this"。