类型推断如何在函数依赖存在的情况下工作 [英] How Type inference work in presence of Functional Dependencies

问题描述

  { - ＃LANGUAGE MultiParamTypeClasses，FlexibleInstances，FunctionalDependencies，UndecidableInstances，FlexibleContexts＃ - } 
 class Foo ac | a  - > c 
 instance Foo Int Float 
 f ::（Foo Int a）=> Int  - > a 
f = undefined 
  

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

 > ：t f 
> f :: Int  - >浮动
  

现在，如果我添加以下代码：

  g :: Int  - >浮动
 g =未定义
 
 h ::（Foo Int a）=> Int  - > a 
h = g 
  

我得到错误

 无法推断（a〜Float）
  

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

这是因为type unification发生在解决实例之前？

[更新]

Dan Doel在咖啡馆邮件list

我相信答案是fundep
实现和类型系列之间的区别是局部约束信息。
Fundeps不会进行本地传播。

因此，在您的第一个定义中，您在本地提供了< Int - >一个'，其中
是GHC可以接受的。然后它从外部计算出函数
，即'（Foo Int a）=> Int - >一个'实际上是 Int - > Float 。

在第二个定义中，您试图给' Int - > Float '，但
GHC只在本地知道您需要提供' Int - >一个'与一个
约束' Foo Int a '它不会用来确定 a〜
Float 。

这不是fundeps固有的。人们可以制作具有本地约束规则的fundeps
版本（通过转换为
新类型的家庭资料很容易）。但是，不同之处在于
重叠实例支持fundeps而不支持type family。
但我现在不会进入。

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

解决方案

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

< pre $ { - ＃LANGUAGE TypeFamilies，FlexibleContexts＃ - }

class Fooo a where
type Out a :: *

实例Fooo Int其中
类型Out Int = Float

ff ::（Foo Int）=> Int - > （Out Int）
ff =未定义

gg :: Int - >浮动
gg =未定义

hh ::（Foo Int）=> Int - > （Out Int）
hh = gg


类型族很好。使用类型家庭，当你可以！

---

我猜你的错误是因为ghc可以推断 f :: Int - > Float from f :: Foo Int a => Int - >一个和你的类定义和实例，但它不能推导出 g :: Foo Int a => Int - >来自 g :: Int - >的浮。

将约束想象为函数中的秘密字典参数很方便。 f中存在一个固有的但受约束的多态现象。

我认为有助于指出，ghci给我们提供了基本上完全相同的错误信息，就好像我们试图定义

  j :: Int  - >浮动
 j =未定义
 
 k ::方程a => Int  - > a 
k = j 
  

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

ghc在编写时也会抱怨

  aconst ::（Foo Int a）=> a 
 aconst = 0.0 
  

甚至

  anotherconst ::（Foo Int a）=> a 
 anotherconst = 0.0 :: Float 
  

总是因为它无法匹配约束 polymorphic a 它需要您输入的特定类型（小数a 或浮）。

你想

  forall a.Foo Int a 
  

与 Float 类型相同，但它不是T。只有一种类型满足 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）与模式<$ c不匹配$ C> 这个。

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.

解决方案

To avoid this problem, you can use type families instead:

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

Type families are nice. Use type families when you can!

---

I'm guessing your error is because ghc can deduce f :: Int -> Float from f :: Foo Int a => Int -> a and your class definition and instances, but it can't deduce g :: Foo Int a => Int -> a from g:: Int -> Float.

It's convenient to think of constraints as a secret dictionary parameter on the function. There's an inherent but constrained polymorphism in f that there isn't in g.

I think it's helpful to note that ghci is giving us essentially exactly the same error message as if we tried to define

j :: Int -> Float
j = undefined

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

It's obvious that this shouldn't work, because we know that k should be contrainedly polymorphic in its second argument. ghc tries to match the type Int -> a with Int -> Float and fails, complaining that it can't infer a ~ Float from the context Eq a, even though there's an instance Eq Float. In your example, it says it can't infer a ~ Float from the context Foo Int a even though there's an instance for Foo Int Float. I realise we can deduce that there's only one possible type for a, but by making the class and instance for Foo, you have defined a relation and asserted it's a functional dependency. This isn't the same as defining the function (which is why type families solves the problem - it defines the function).

ghc also complains when you write

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

or even

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

always because it can't match the constrainedly polymorphic a it wanted with the specific type you gave it (Fractional a or Float).

You want

forall a.Foo Int a

to be the same type as Float, but it isn't. There's only one type that satisfies forall a.Foo Int a, it's Float, so ghci can take f::forall a.(Foo Int a)=>a->Float and deduce (using a dictionary for Foo) that f::Int->Float , but you're expecting ghci to take Float and find notice it's forall a.Foo Int a, but there's no dictionary for Float, it's a type, not a type class. ghci can do it one way, but not the other.

Dan's point about local information is that ghc would have to use both Foo's definition and the instance you made to deduce that Float can be rewritten forall a.(Foo Int a), and that at this point in compilation, ghc isn't using global information because it's just trying to do a match. My point is that Float matches forall a.(Foo Int a) but forall a.(Foo Int a) doesn't match Float, in the sense that "this" matches the pattern (x:xs) but (x:xs) doesn't match the pattern "this".

这篇关于类型推断如何在函数依赖存在的情况下工作的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！