(跳过手动推导部分)
给定 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)).
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).
当在Prolog解释器中运行时,它会自动产生。
3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A))
类型被表示为复合数据项,以纯语法方式。例如,类型[a] -> a
由arrow(list(A), A)
表示,可能的Haskell等价物为Arrow (List (Logvar "a")) (Logvar "a")
,给定适当的data
定义。
只使用了一个推理规则,即应用,以及Prolog的结构统一,其中复合术语匹配,如果它们具有相同的形状和它们的组成部分匹配:f(a1, a2, ... an)和g(b1, b2, ... bm)匹配,如果f与g相同,n == m且ai匹配bi,逻辑变量能够根据需要采取任何值,但只能一次(不能更改)。
4 ?- type([compose, head], T1).
T1 = arrow(arrow(A, list(B)), arrow(A, B))
5 ?- type([filter, fst], T2).
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))
要手动进行类型推断,需要机械地将事物写在下面,侧边记录等价关系并执行替换,从而模拟Prolog的操作。我们可以将任何->,(_,_), []
等仅视为语法标记,而不理解其含义,并使用结构统一来机械地执行此过程,这里只使用一条类型推断规则,即应��规则:(a -> b) c ⊢ b {a ~ c}
(在a
和c
等价的情况下,用b
替换(a -> b)
和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)
42
作为参数传递给filter
,则一致性将成功,并导致文字42
具有类型forall a. Num(a->Bool) :: a->Bool
。在处理过程的更晚阶段,ghc将报告范围内没有有效的“instance Num(a->Bool)”。这具有实际后果,因为此类错误在实践中有些常见,并且了解为什么ghc会产生此错误而不是更有用的错误提示是很有用的。 - John L