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.  (.) . (.)

在这种情况下,我不知道如何找到类型,因为我猜第一个(<)是两个返回a的元素的函数,Bool但我在编写孔表达式时遇到了麻烦.

所以问题是,使用这种练习的最佳方法是什么？

---

补充:我知道如何检查类型ghci,问题是如何在没有它的情况下实际找到它们(了解Haskell如何工作).

Answer 1

您可以使用:tin 轻松检查表达式的类型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允许的,但我们会忽视现在.我们这样做的原因是稍后引用特定(.)函数的类型:

   (.1) (.2) (.3)

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

   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)as作为参数调用,所以我们知道(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.

正如您可以看到的所有三个查询我们获得相同的类型(当然类型变量的名称是不同的).