类型推断算法如何解决受保护的方程？

Question

我试图找出 Haskell 是如何从一个没有通过网络指定类型的受保护方程中解析类型的。

例如遵循函数定义，ghci 能够解析类型并准确告诉我它是什么。

fun a b c
| a == c = b
| b < 0 = a+b
| otherwise = c

它是如何做到的？我知道这对于 if-then-else 结构是如何工作的（基本上：从通用版本开始，添加约束）但我想知道这里需要哪些额外步骤？

Answer 1

fun 有三个参数和一个结果。所以最初编译器假设它们可能是不同的类型：

fun :: alpha -> beta -> gamma -> delta         -- the type vars are placeholders

忽略守卫，看看方程的 rhs 结果：它们每个都必须是类型delta。所以从词项级方程中建立一系列类型级方程。在类型之间使用~ 表示它们必须相同。

• 第一个方程有结果b，所以b的类型必须与结果相同，即beta ~ delta。
• 第三个方程有结果c，所以c的类型必须与结果gamma ~ delta相同。
• 第二个等式有 rhs + 运算符 :: Num a => a -> a -> a。我们将回到Num a =>。这就是说+ 有两个参数和一个结果，它们都是相同的类型。该类型是 fun 的 rhs 的结果，因此必须是 delta。 + 的第二个参数是b，所以b 的类型必须与结果beta ~ delta 相同。我们已经从第一个等式中得到了这一点，所以这只是为了确认一致性。
• + 的第一个参数是a，所以a 的类型必须再次相同，alpha ~ delta。

我们有alpha ~ beta ~ gamma ~ delta。所以回到最初的签名（尽可能通用），用equals代替equals：

fun :: (constraints) => alpha -> alpha -> alpha -> alpha

约束

从运营商那里即时取货。

• 由于运营商+，我们已经看到Num。
• 第一个等式的a == c 为我们提供Eq。
• 第二个等式的b < 0 为我们提供Ord。
• 实际上0 的出现给了我们另一个Num，因为0 :: Num a => a 和< :: Ord a => a -> a -> Bool IOW 的参数< 必须是相同的类型和相同的约束。

所以在fun的类型前面堆积这些约束，消除重复

fun :: (Num alpha, Eq alpha, Ord alpha) => alpha -> alpha -> alpha -> alpha

这就是你最喜欢的编译器告诉你的吗？它可能使用类型变量a 而不是alpha。它可能没有显示Eq alpha。

消除不必要的超类约束

Main> :i Ord
...
class Eq a => Ord a where
...

Eq a => 告诉每个Ord 类型必须已经带有Eq。因此，在为fun 提供签名时，编译器会假设它的Eq 消失。

fun :: (Num a, Ord a) => a -> a -> a -> a

QED

Answer 2

fun a b c
| a == c = b
| b < 0 = a+b
| otherwise = c

是否清楚这如何转换为 if/else？

fun a b c
 = if a == c
      then b
      else if b < 0
             then a+b
             else c

如果我们添加一些人类可读的注释：

fun a b c      -- Start reasoning with types of `a`, `b`, `c`, and `result :: r`
 = if a == c   -- types `a` and `c` are equal,  aka `a ~ c`.  Also `Eq a, Eq c`.
      then b   -- types `b ~ r`
      else if b < 0   -- `Num b, Ord b`
             then a+b -- `a ~ b ~ r` and `Num a, Num b`
             else c   -- `c ~ r`

如果你把所有这些事实放在一起，这个类型很快就会归结起来。

a ~ b ~ r  and c ~ r

所以我们知道实际上只有一种类型，我们只需调用 a 并在事实中重命名所有其他类型变量。

Num a, Eq a, Ord a

我们知道Ord 意味着Eq 是一个小的认知节省，所以我们最终可以得到约束Num a, Ord a。

所有这些都席卷了机制 - 利用诸如 (==) t1 t2 ~~> t1 = t2 之类的含义 - 在地毯下，但希望以可接受的方式。