function - Haskell 和一般类型

Question

我对 Haskell 有点陌生，我想了解一般类型的工作原理。

获取表达式类型的“系统”思维方式应该是什么？

举个例子，如果我们有:

(\x y z -> x (y z))

我思考这个问题的方式就是使用直觉，但这并不总是有效。

在这种情况下我会说:

   (y z) :: (t -> t1) --function y takes t and return t1
 x (y z) :: (t1 -> t2) --function x takes argument of type (return type of y)

(\x y z -> x (y z)) :: (t1 -> t2) -> (t -> t1) -> t -> t2 --return type is t2 (of x) with argument of type t for function y

我很确定这应该是正确的，但有时会更困难，而且这种思考方式似乎行不通。

例如，如果我们有:

1.  (\x -> x (<))  or
2.  (.) . (.)

在这种情况下，我不知道如何找到类型，首先我猜测 (<) 是两个元素上的函数，返回 Bool 但我在编写孔表达式。

所以问题是，进行此类练习的最佳方法是什么？

<小时/>

添加:我知道如何使用 ghci 检查类型，问题是如何在没有它的情况下实际找到它们(以了解 Haskell 的工作原理)。

Answer 1

您可以使用 :t 轻松检查表达式的类型在ghci :

Prelude> :t (\x y z -> x (y z))
(\x y z -> x (y z)) :: (r1 -> r) -> (r2 -> r1) -> r2 -> r
Prelude> :t (\x -> x (<))
(\x -> x (<)) :: Ord a => ((a -> a -> Bool) -> r) -> r
Prelude> :t (.) . (.)
(.) . (.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c

但我假设您想自己派生类型。

1. 首先，我们可以从查看变量开始。这些是x , y和z 。我们首先为它们分配“通用类型”，因此:

   x :: a
   y :: b
   z :: c
   

   现在我们查看表达式的右侧，看到 (y z) 。这意味着我们“调用”y与 z作为论证。因此，我们“专门化” y 的类型至y :: c -> d 。 (y z)的类型那么就是(y z) :: d 。现在我们看到x (y z) 。所以我们再次“专门化” x 的类型进入x :: d -> e 。结果我们得到:

   x :: d -> e
   y :: c -> d
   z :: c
   

   最后，lambda 表达式映射 \x y z -> x (y z) 。因此，这意味着我们查看的结果类型是“伪代码”中的内容:type(x) -> type(y) -> type(z) -> type('x (y z)') 。或者:

   \x y z -> x (y z) :: (d -> e) -> (c -> d) -> c -> e
   

2. 对于第二个表达式，我们首先必须导出 (<) 的类型:

   Prelude> :t (<)
   (<) :: Ord a => a -> a -> Bool
   

   这是因为(<)是在 Prelude 中定义的与该类型。

   现在我们知道了，我们可以查看类型签名。我们首先假设 x :: b 的类型。现在我们看向右侧，看到我们调用 x (<) 。这意味着我们知道 x类型为 Ord a => (a -> a -> Bool) -> c我们知道x (<) :: c 。然后我们又得到了一个 lambda 表达式，正如我们在上面看到的，我们可以像这样解析它:

   (\x -> x (<)) :: Ord a => ((a -> a -> Bool) -> c) -> c
   

3. 最后对于第三个表达式，让我们首先将其重写为:

   (.) (.) (.)
   

   这是第一个 (.)函数，原来是. (不带括号)，但我们将首先删除运算符语法糖。

   接下来我们将为操作符命名(只是为了让我们更方便地命名它们)。 Haskell 中不允许这样做，但我们暂时忽略它。我们这样做的原因是为了稍后引用特定 (.) 的类型功能:

   (.<i>1</i>) (.<i>2</i>) (.<i>3</i>)

   接下来我们查找 (.) 的类型:

   Prelude> :t (.)
   (.) :: (b -> c) -> (a -> b) -> a -> c
   

   所以我们首先分配一些类型:

   (.1) :: (b -> c) -> (a -> b) -> a -> c
   (.2) :: (e -> f) -> (d -> e) -> d -> f
   (.3) :: (h -> i) -> (g -> h) -> g -> i
   

   现在我们需要进一步分析这些类型。我们调用(.1)与 (.2)作为参数，所以我们知道 (b -> c) ( (.1) 的第一个参数相当于 (e -> f) -> (d -> e) -> d -> f 。这意味着:

   (b -> c) ~ (e -> f) -> (d -> e) -> d -> f
   

   由于类型箭头是右关联的，(e -> f) -> (d -> e) -> d -> f实际上意味着(e -> f) -> ((d -> e) -> (d -> f)) 。那么现在我们可以进行分析:

     b        -> c
   ~ (e -> f) -> ((d -> e) -> (d -> f))
   

   这意味着 b ~ (e -> f)和c ~ ((d -> e) -> (d -> f)) 。所以我们“特化”我们的第一个(.1) :: (b -> c) -> (a -> b) -> a -> c进入

   (.1) :: ((e -> f) -> ((d -> e) -> (d -> f))) -> (a -> (e -> f)) -> a -> ((d -> e) -> (d -> f))
   

   现在的类型为 (.1) (.2)是

   (.1) (.2) :: (a -> (e -> f)) -> a -> ((d -> e) -> (d -> f))
   

   但现在我们用 (.3) 调用该函数所以我们必须导出 ((.1) (.2)) (.3) 的类型。因此，我们必须再次进行类型解析:

     a        -> (e        -> f)
   ~ (h -> i) -> ((g -> h) -> (g -> i))
   

   这意味着 a ~ (h -> i) , e ~ (g -> h)和f ~ (g -> i) 。所以现在我们已经将类型解析为:

   ((.1) (.2)) (.3) :: a -> c
   =                   (h -> i) -> ((d -> (g -> h)) -> (d -> (g -> i)))
   =                   (h -> i) -> (d -> g -> h) -> d -> g -> i
   

   最后一行只是语法上的简化。正如您所看到的，这映射到我们从 ghci 派生的类型。 .

正如您所看到的，对于所有三个查询，我们获得相同的类型(当然类型变量的名称不同)。