如何手动确定以下功能的最常用类型？

Question

目前我正在学习Haskell.我们必须确定给定函数的最一般类型,但我还没有得到它.解释器如何确定函数的最一般类型,尤其是lambda表达式？什么是手动确定最常规类型的安全方法？

tx2 = (\x y z -> y.z.z)

tx2::a->(a->b)->(a->a)->b -- my guess

tx2 :: a -> (b -> c) -> (b -> b) -> b -> c -- interpreter solution

如果第一个变量(a)应用于表达式z,则z必须将a作为输入参数,但它在(b-> b)中使用b.y消耗b并生成c,因此最终结果必须为c.但为什么b(作为中间结果？)包含在类型中？如果是这样,为什么它不是 - >(b - > c) - >(b - > b) - > b-> b - > c？

tm2 = (\i -> [sum,product]!!i)

tm2:: Int->[(Integer->Integer->Integer)]->(Integer->Integer->Integer) -- my guess

\i -> [sum,product] !! i :: Num a => Int -> [a] -> a -- interpreter with direct input
tm2 :: Int -> [Integer] -> Integer -- interpreter with :info tm2

因此,如果tm2在脚本中编码,解释器有关于类型的更详细信息,对吗？所以第二行中的类型是表达式的结果.为什么第2行只接受整数,而不是Float例如？

tp2 = (\x -> \y -> (x.y.x))

tp2::(a->b)->((a->b)->a)->a -- my guess

tp2 :: (a -> b) -> (b -> a) -> a -> b -- interpreter solution

为什么我必须在类型中包含中间结果？为什么没有使用(a-> b) - > a表示下面的tf2？

tf2 = (\x -> \y -> (x (y x), x, y))

tf2::(a->b)->((a->b)->a)->(a,a->b,(a->b)->a) -- solution


tg2 = (\x y z a -> y(z(z(a))));

tg2::a->(b->c)->(b->b)->b->c -- solution

在这里我们不需要任何中间结果？我们写下参数的类型,然后写下结果的类型？

Answer 1

tx2 = (\x y z -> y.z.z)

tx2需要三个参数(为了讨论,我忽略了currying),忽略第一个并组成第二个和第三个两次.所以第一个参数可以有任何类型,第二个和第三个必须有函数类型,比方说

y :: ay -> ry
z :: az -> rz

现在的第一个应用程序的结果z成为第二个应用程序的参数z,那么结果类型z,rz必须的参数类型z,az让我们称之为b,所以

z :: b -> b

然后z应用程序的结果成为参数y,因此参数类型y必须与结果类型相同z,但结果类型y完全不受表达式约束,因此

y :: b -> c

和y . z . z :: b -> c,从而

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

接下来,

tm2 = (\i -> [sum,product]!!i)

现在,sum并且product是来自的函数Prelude,都具有类型Num a => [a] -> a,因此

Prelude> :t [sum,product]
[sum,product] :: Num a => [[a] -> a]

因为(!!) :: [e] -> Int -> e,给定xs类型列表[e],表达式\i -> xs !! i具有类型Int -> e.因此推断的类型tm2 = \i -> [sum,product] !! i是

tm2 :: Num a => Int -> ([a] -> a)

但是,tm2受到没有类型签名的简单模式绑定的约束,因此单态限制开始,并且类型tm2必须是单态的.由违约规则,一个Num a约束是通过实例化类型变量解决a用Integer(除非明确的默认声明另有规定),让您得到

Prelude> let tm2 = \i -> [sum,product] !! i
Prelude> :t tm2
tm2 :: Int -> [Integer] -> Integer

除非你禁用单态限制(:set -XNoMonomorphismRestriction).

tp2 = (\x -> \y -> (x.y.x))

第一次应用的结果x成为参数y,因此结果类型x必须与参数类型相同y.然后应用的结果y成为第二个应用的参数x,所以结果类型y必须是'x`的参数类型,一共

tp2 :: (a -> b) -> (b -> a) -> (a -> b)

然后进去

tf2 = (\x -> \y -> (x (y x), x, y))

唯一有趣的部分是结果的第一个组成部分x (y x),因此x应用于应用程序的结果y,因此x必须具有函数类型

x :: a -> b

并且y必须具有结果类型a.但是y应用于x,所以它的参数类型必须是类型x,

y :: (a -> b) -> a

和

tf2 :: (a -> b) -> ((a -> b) -> a) -> (b, a -> b, (a -> b) -> a)

最后

tg2 = (\x y z a -> y(z(z(a))))

顺便说一下,这tx2只是通过在lambda中提供一个参数来进行eta扩展.因此,类型的推导也是相同的.