haskell - How Type inference work in presence of Functional Dependencies

Question

Consider the code below :

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

Now when I see the inferred type of f in ghci

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

Now If I add the following code

g :: Int -> Float 
g = undefined 

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

I get the error

Could not deduce (a ~ Float)

I am not able to understand what has happened here? The restriction Foo Int a should have restricted the type of h to Int -> Float as shown in the inferred type of f.

Is it because type unification is occurring before resolving the instances ?

[Update]

An explanation given by Dan Doel on the cafe mailing list

The answer, I believe, is that the difference between the fundep implementation and type families is local constraint information. Fundeps do no local propagation.

So in your first definition, you've locally provided 'Int -> a', which is acceptable to GHC. Then it figures out externally to the function that '(Foo Int a) => Int -> a' is actually Int -> Float.

In the second definition, you're trying to give 'Int -> Float', but GHC only knows locally that you need to provide 'Int -> a' with a constraint 'Foo Int a' which it won't use to determine that a ~ Float.

This is not inherent to fundeps. One could make a version of fundeps that has the local constraint rules (easily so by translating to the new type families stuff). But, the difference is also the reason that overlapping instances are supported for fundeps and not type families. But I won't get into that right now.

I still don't understand what that mean. So still looking for better understandable answer.

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从 context推断Eq a，即使有一个 instance Eq Float。在您的示例中，它表示a ~ Float即使Foo Int a有Foo Int Float. 我意识到我们可以推断出只有一种可能的类型a，但是通过为 Foo 创建类和实例，您已经定义了一个关系并断言它是一个函数依赖。这与定义函数不同（这就是类型族解决问题的原因——它定义了函数）。

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"。