Haskell:如何手动推断表达式的类型

Question

给出了Haskell函数:

head . filter fst

现在的问题是如何手动"手动"找到类型.如果我让Haskell告诉我我得到的类型:

head . filter fst :: [(Bool, b)] -> (Bool, b) 

但是我想了解它是如何工作的,只使用已定义如下的已使用函数的签名:

head :: [a] -> a
(.) :: (b -> c) -> (a -> b) -> a -> c
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a

编辑:这么多很好的解释......选择最好的一个并不容易!

Answer 1

使用通常称为统一的过程来推断类型.Haskell属于Hindley-Milner族,它是用于确定表达式类型的统一算法.

如果统一失败,则表达式是类型错误.

表达方式

head . filter fst

经过.让我们手动统一,看看为什么我们得到了什么.

让我们从filter fst:

filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a'                -- using a', b' to prevent confusion

filter拿一个(a -> Bool),然后一个[a]给另一个[a].在表达式中 filter fst,我们传递给filter参数fst,其类型是(a', b') -> a'.为此,类型fst 必须与filter第一个参数的类型统一:

(a -> Bool)  UNIFY?  ((a', b') -> a')

该算法统一了两个类型表达式,并尝试将尽可能多的类型变量(例如a或a')绑定到实际类型(例如Bool).

只有这样才会filter fst导致有效的类型化表达式:

filter fst :: [a] -> [a]

a'显然Bool.所以类型变量 a'解析为a Bool.并且(a', b')可以统一到a.所以,如果a是(a', b')和a'是Bool,然后a就是(Bool, b').

如果我们传递了一个不兼容的参数filter,例如42(a Num),那么Num a => awith的统一a -> Bool就会失败,因为这两个表达式永远不能统一到一个正确的类型表达式.

回来

filter fst :: [a] -> [a]

这与a我们所讨论的相同,因此我们将其替换为先前统一的结果:

filter fst :: [(Bool, b')] -> [(Bool, b')]

下一点,

head . (filter fst)

可以写成

(.) head (filter fst)

所以拿 (.)

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

因此,要使统一成功,

1. head :: [a] -> a 必须统一 (b -> c)
2. filter fst :: [(Bool, b')] -> [(Bool, b')] 必须统一 (a -> b)

从(2)我们得到表达式 中的a IS )b(.) :: (b -> c) -> (a -> b) -> a -> c

因此,类型变量的值a,并c在表达(.) head (filter fst) :: a -> c很容易地告诉,因为(1)给了我们之间的关系b和c,即:b是的列表c.当我们知道a是[(Bool, b')],c只能统一到(Bool, b')

因此head . filter fst成功进行类型检查:

head . filter fst ::  [(Bool, b')] -> (Bool, b')

UPDATE

有趣的是,您可以从各个方面统一启动流程.我filter fst先选择,然后继续(.),head但正如其他例子所示,统一可以通过多种方式进行,与数学证明或定理推导可以多种方式完成的方式不同!

Answer 2

filter :: (a -> Bool) -> [a] -> [a]获取一个函数(a -> Bool),一个相同类型a的列表,并返回该类型的列表a.

在确定指标的使用filter fst与fst :: (a,b) -> a这样的类型

filter (fst :: (Bool,b) -> Bool) :: [(Bool,b)] -> [(Bool,b)]

是推断.接下来,您撰写你的结果[(Bool,b)]与head :: [a] -> a.

(.) :: (b -> c) -> (a -> b) -> a -> c是两个功能的组成,func2 :: (b -> c)和func1 :: (a -> b).在你的情况下,你有

func2 = head       ::               [ a      ]  -> a

和

func1 = filter fst :: [(Bool,b)] -> [(Bool,b)]

所以head这里[(Bool,b)]作为参数并按(Bool,b)定义返回.最后你有:

head . filter fst :: [(Bool,b)] -> (Bool,b)

Answer 3

让我们开始吧(.).它的类型签名是

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

它说"鉴于从功能b到c,并从功能a到b,并且a,我可以给你一个b".我们想用head和 filter fst,所以`:

(.) :: (b -> c) -> (a -> b) -> a -> c
       ^^^^^^^^    ^^^^^^^^
         head     filter fst

现在head,这是一个从一个东西到一个东西的函数的函数.所以现在我们知道它将b成为一个数组,并且c将成为该数组的一个元素.所以为了表达的目的,我们可以认为(.)有签名:

(.) :: ([d] -> d) -> (a -> [d]) -> a -> d -- Equation (1)
                     ^^^^^^^^^^
                     filter fst

签名filter是:

filter :: (e -> Bool) -> [e] -> [e] -- Equation (2)
          ^^^^^^^^^^^
              fst

(注意,我已经更改了类型变量的名称,以避免与a我们已经拥有的s 混淆!)这说"给定一个函数来自eBool,以及一个es 列表,我可以给你一个es 的列表".该功能fst 有签名:

fst :: (f, g) -> f

他说,"如果有一对包含一个f和一个g,我可以给你一个f".与公式2相比,我们知道它将 e是一对值,其中第一个元素必须是a Bool.所以在我们的表达中,我们可以认为filter 有签名:

filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]

(我在这里所做的就是e用(Bool, g)公式2 替换.)表达式filter fst的类型如下:

filter fst :: [(Bool, g)] -> [(Bool, g)]

让我们再回到公式1,我们可以看到,(a -> [d])现在必须 [(Bool, g)] -> [(Bool, g)],所以a必须[(Bool, g)]和d 必须(Bool, g).所以在我们的表达中,我们可以认为(.)有签名:

(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)

总结一下:

(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                head                         filter fst
head :: [(Bool, g)] -> (Bool, g)
filter fst :: [(Bool, g)] -> [(Bool, g)]

把它们放在一起:

head . filter fst :: [(Bool, g)] -> (Bool, g)

这相当于你所拥有的,除了我用作g类型变量而不是b.

这可能听起来很复杂,因为我用血淋淋的细节描述了它.然而,这种推理很快成为第二天性,你可以在脑海中做到这一点.

Answer 4

^{（跳过手动推导）}

找到head . filter fst==的类型((.) head) (filter fst)，给定

head   :: [a] -> a
(.)    :: (b -> c) -> ((a -> b) -> (a -> c))
filter :: (a -> Bool) -> ([a] -> [a])
fst    :: (a, b) -> a

这是通过一个小的 Prolog 程序以纯机械的方式实现的：

type(head,    arrow(list(A)       , A)).                 %% -- known facts
type(compose, arrow(arrow(B, C)   , arrow(arrow(A, B), arrow(A, C)))).
type(filter,  arrow(arrow(A, bool), arrow(list(A)    , list(A)))).
type(fst,     arrow(pair(A, B)    , A)).

type([F, X], T):- type(F, arrow(A, T)), type(X, A).      %% -- application rule

当在 Prolog 解释器中运行时，它会自动生成，

3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A))       %% -- [(Bool,a)] -> (Bool,a)

其中类型以纯语法方式表示为复合数据项。例如，类型[a] -> a由 表示arrow(list(A), A)，可能与 Haskell 等效Arrow (List (Logvar "a")) (Logvar "a")，给出适当的data定义。

仅使用了一个推理规则，即应用程序的推理规则，以及 Prolog 的结构统一，即如果复合词具有相同的形状且其成分匹配，则复合词匹配：f(a ₁ , a ₂ , ... a _n )和g (b ₁ , b ₂ , ... b _m )匹配仅当f与g相同，n == m并且a _i匹配 b _i，逻辑变量可以根据需要取任何值，但只能取一次 （无法更改）。

4 ?- type([compose, head], T1).     %% -- (.) head   :: (a -> [b]) -> (a -> b)
T1 = arrow(arrow(A, list(B)), arrow(A, B))

5 ?- type([filter, fst], T2).       %% -- filter fst :: [(Bool,a)] -> [(Bool,a)]
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))

要以机械方式手动执行类型推断，涉及将一个东西写在另一个下面，注意旁边的等价物并执行替换，从而模仿 Prolog 的操作。我们可以将 any->, (_,_), []等纯粹视为句法标记，而根本不了解它们的含义，并使用结构统一来机械地执行该过程，在这里，只有一种类型推断规则，即。的规则应用：(a -> b) c ? b {a ~ c}（取代的并置(a -> b)和c，与b，的等价下a和c）。一致地重命名逻辑变量很重要，以避免名称冲突：

(.)  :: (b    -> c ) -> ((a -> b  ) -> (a -> c ))           b ~ [a1], 
head ::  [a1] -> a1                                         c ~ a1
(.) head ::              (a ->[a1]) -> (a -> c ) 
                         (a ->[c] ) -> (a -> c ) 
---------------------------------------------------------
filter :: (   a    -> Bool) -> ([a]        -> [a])          a ~ (a1,b), 
fst    ::  (a1, b) -> a1                                    Bool ~ a1
filter fst ::                   [(a1,b)]   -> [(a1,b)]  
                                [(Bool,b)] -> [(Bool,b)] 
---------------------------------------------------------
(.) head   :: (      a    -> [     c  ]) -> (a -> c)        a ~ [(Bool,b)]
filter fst ::  [(Bool,b)] -> [(Bool,b)]                     c ~ (Bool,b)
((.) head) (filter fst) ::                   a -> c      
                                    [(Bool,b)] -> (Bool,b)