我试图了解Haskell如何能够从一个没有通过web指定类型的保护等式中解析类型。
就像下面的函数定义一样，ghci能够解析类型，并告诉我它到底是什么
fun a b c
| a == c = b
| b < 0 = a+b
| otherwise = c
它是怎么做到的？我知道if-then-else构造是如何工作的(基本上：从通用版本开始，添加约束(，但我想知道这里需要哪些额外的步骤？
fun有三个参数和一个结果。因此，最初编译器假设它们可能都是不同的类型：
fun :: alpha -> beta -> gamma -> delta -- the type vars are placeholders
忽略保护，看看方程的rhs结果：它们的类型都必须是delta。因此，从术语水平方程出发，建立了一系列类型水平方程。在类型之间使用~表示它们必须相同。
- 第一个方程的结果为
b，因此b的类型必须与结果相同，即beta ~ delta - 第三个方程式的结果为
c，因此c的类型必须与结果gamma ~ delta相同 - 第二个方程有rhs
+算子CCD_。我们将回到Num a =>。也就是说+有两个参数和一个结果，它们都是相同的类型。该类型是fun的rhs的结果，因此必须是delta。+的第二个参数是b，因此b的类型必须与结果beta ~ delta相同。我们已经从第一个方程中得到了这一点，所以这只是证实了一致性 +的第一个arg是a，因此a的类型必须再次相同，即alpha ~ delta
我们有alpha ~ beta ~ gamma ~ delta。所以回到最初的签名(尽可能通用(，用equals代替equals：
fun :: (constraints) => alpha -> alpha -> alpha -> alpha
限制
随时从操作员那里取下。
- 由于运算符
+，我们已经看到了Num - 第一个方程的CCD_ 27给出了CCD_
- 第二个方程的CCD_ 29给出了CCD_
- 实际上，
0的出现给了我们另一个Num，因为0 :: Num a => a和< :: Ord a => a -> a -> BoolIOW，<的参数必须是相同的类型和相同的约束
因此，将这些约束堆积在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
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等含义——但希望能以一种可接受的方式。