Как я могу вручную определить наиболее общие типы для следующих функций?

Question

В настоящее время я изучаю Haskell.Мы должны определить наиболее общие типы для данных функций, но я пока не понимаю.Как интерпретатор определяет наиболее общий тип функции, особенно лямбда-выражения?Каков безопасный способ определения наиболее общего типа вручную?

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в (б-> б).y потребляет b и генерирует c, поэтому конечный результат должен быть c.Но почему b (как промежуточный результат?) Содержится в типе?И если так, то почему это не a -> (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 принимаются только целые числа, а не, например, число с плавающей точкой?

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 здесь в тип?Почему \ y не представлен с использованием (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 принимает три аргумента (для обсуждения я игнорирую карри), игнорирует первый и составляет второй и дважды третий.Таким образом, первый аргумент может иметь любой тип, второй и третий должны иметь тип функции, скажем,

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

Теперь результат первого применения z становится аргументом второго приложения zтаким образом, тип результата z, rz должен быть типом аргумента z, az, назовем это b, поэтому

z :: b -> b

Тогда результатz application становится аргументом 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)

Now, 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, только расширенный eta, предоставляя еще один аргумент в лямбдуПоэтому происхождение типа тоже одинаково.

Answer 2

Я думаю, что многие из ваших сомнений относительно типов функций в Haskell получили бы ответ, прочитав что-нибудь о "curry", например, в wikipedia .

Выводимые типы функций, которые вы написали, выглядят так, потому что Haskell работает с каррированными функциями, то есть функциями только с входным параметром, который может возвращать (в зависимости от определения) другие функции. Таким образом, когда вы пишете функцию, такую ​​как mySum x y = x + y, ее тип a -> a -> a, ее легче читать, если явно указать правильную ассоциативность ->: a -> (a -> a). Увидеть? Дополнительные типы возвращаемых вами данных не являются «промежуточными результатами», как вы их называете. Вы не берете два параметра и не возвращаете результат a. Вы берете один параметр, x, фиксируете его значение в выражении x + y и возвращаете функцию a -> a, которая принимает параметр (y на этот раз) и суммирует его с y, который вы ранее исправили.

Отвечать по пунктам на ваш вопрос было бы довольно долго, так что я пропущу, но это причина, которую вы должны сделать, чтобы проверить типы ваших функций.

Я не уверен в разнице между выведенными типами переводчиком для вашего второго вопроса по tm2.