实例化Haskell参数化数据类型

Question

试图掌握下面的Haskell type parameter，

Prelude> data T a = C1 a | C2 (a -> a)
Prelude> :t C1 1
C1 1 :: Num a => T a
Prelude> :t C1 (+1)
C1 (+1) :: Num a => T (a -> a)
Prelude> :t C2 1
C2 1 :: Num (a -> a) => T a
Prelude> :t C2 (+1)
C2 (+1) :: Num a => T a

据我所知，C1 1是毫无疑问的，C2 1毫无意义，C1 (+1)和C2 (+1)似乎是矛盾的。

为什么上面的类型检查都没有投诉？非常感谢您的启发。

Answer 1

在Haskell中，数字文本是多态的:

1 :: Int
1 :: Integer
1 :: Double
...

从技术上讲，这是通过一般类型的获得的

1 :: Num a => a

因此，"1可以是任何类型，只要这种类型属于Num类"。

当您这样做时，例如C2 1，1被认为是函数类型a -> a，并生成一个额外的约束以确保a -> a是Num:

C2 1 :: Num (a -> a) => T a

当然，函数不是数字。为什么没有类型错误？因为在Haskell中，并不禁止扩展Num类以包含函数。你可以这样做，例如：

instance Num b => Num (a -> b) where
   fromInteger n = _ -> n
   x + y = z -> x z + y z
   ...

有效地将CCD_ 14转化为"常一"函数。

这可以启用诸如（下面是人为的示例）之类的代码

 case (some value of type T Int) of
 C1 x -> x
 C2 f -> (f + g) 50
 -- assumning g :: Int -> Int
 -- result is f 50 + g 50 

如果您不提供实例，那么代码本身并不是错误的，因为稍后可能会添加实例。在这种情况下，约束将保留在代码中，因为它无法释放。如果您试图将T a转换为任何不涉及a的类型，这需要释放Num约束，届时编译器确实会抱怨。

---

涉及CCD_ 18的情况可以通过注意到这是算子部分来解释，所以它不仅仅是1前面的一元加。特别是

(+1) means x -> x + 1

所以CCD_ 19实际上是后继函数。

Answer 2

如果您希望出现错误，请创建一个a必须相同的情况，如：

> :t [C1 (+1), C2(+1)]
Couldn't match expected type ....

在您的示例中，a是不同的，如a1和a2。并且没有错误