Как Хаскелл определяет тип (+). (+)

Question

Почему тип (+).(+) равен (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a?

(+) :: Num a => a -> a -> a
(.) :: (b -> c) -> (a -> b) -> a -> c

Я пытался, но не знал, как получится (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a.

(+) :: Num i => i -> i -> i
(.) :: (b -> c) -> (a -> b) -> (a -> c)
(+) :: Num j => j -> j -> j

(+) . (+) :: (i -> (i -> i)) -> ((j -> j) -> i) -> ((j -> j) -> (i -> i))
where: 
  b = i
  c = i -> i
  a = j -> j

Может ли кто-нибудь помочь и дать мне шаги анализа?

Answer 1

В моих объяснениях, как правило, больше слов и меньше формул - извинения, если это бесполезно, но другие ответы меня немного не удовлетворяют, поэтому я подумал, что объясню немного по-другому.

Очевидно, у вас уже есть хорошее представление о том, что делают различные части.В частности, (.) принимает две функции и дает функцию, которая сначала применяет функцию справа от аргумента, затем применяет функцию слева к результату.

Итак, мы начнем с функциисправа: (+).Это имеет тип (Num a) => a -> a -> a, то есть он принимает два аргумента, которые должны быть одного типа, и этот тип должен быть экземпляром Num.И затем он возвращает значение того же типа.

Напомним, что из-за карри это эквивалентно (Num a) => a -> (a -> a).То есть он принимает экземпляр Num и возвращает функцию из того же типа самому себе.

Теперь мы должны скомпоновать ее с другой функцией - той, которая принимает тип результата в качестве входных данных.Что это за другая функция?Это снова (+)!Но мы знаем, что для проверки типа композиции мы должны передать ей тип функции: a -> a (где a - это экземпляр Num).Как мы уже видели, это не проблема, поскольку (+) может принимать любого типа, который является экземпляром Num.Это может включать a -> a, когда у нас есть соответствующий экземпляр.И это объясняет, почему конечный тип имеет 2 ограничения Num a и Num (a -> a).

Теперь все легко собрать воедино.Оставляя без ограничений (с которыми мы уже имели дело), ​​мы схематически имеем:

(+)                                 .     (+)
(a -> a) -> ((a -> a) -> (a -> a))        a -> (a -> a)

Итак, в сигнатуре типа (.), которую я напишу как (c -> d) -> (b -> c) -> (b -> d), мы имеем a как b, a -> a как c и (a -> a) -> (a -> a) как d.Подставляя их в, мы получаем конечный тип (b -> d) как:

a -> ((a -> a) -> (a -> a))

, который мы можем переписать как

a -> (a -> a) -> a -> a

, удалив ненужные скобки, после вызова функции стрелкиправоассоциативная.

Answer 2

Другой подход:

((+).(+)) x y z
= (+) ((+) x) y z
= ((x +) + y) z

Теперь обратите внимание:

(x +) + y

- это сумма двух функций , поскольку один из аргументов является функцией. Давайте предположим, x :: a, поскольку мы должны начать где-то (это предположение не обязательно означает, что a появится в конечном типе, мы просто хотим дать ему имя, чтобы начать наш процесс рассуждения)

x :: a

Тогда

(x +) :: a -> a
y :: a -> a      -- since the operands of + have to be the same type

Также мы добавляем x в (x +), что дает нам Num a, и мы добавляем функции, которые дают нам Num (a -> a) (на данный момент, по сути, это ошибка, поскольку ни один здравомыслящий человек не определяет экземпляр Num для функций - это возможно, но это плохая идея).

В любом случае, выражение, которое мы только что проанализировали, является суммой двух вещей типа a -> a, поэтому результат также должен иметь тип a -> a.

((x +) + y) z    -- since the result of + has to have the same type 
^^^^^^^^^^^      --                                    as its operands 
  a -> a

Следовательно, z :: a.

Итак, наконец, все выражение набрано

(+).(+) :: a -> (a -> a) -> a -> a
           ^    ^^^^^^^^    ^    ^
           x       y        z    final result

плюс ограничения, которые мы подобрали по пути.

Answer 3

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

If you apply two functions to it you get in pseudocode:
(+) . (+) -> a -> c

So what is the type of a? It has the same type as the first argument 
of the second function you pass into (.). You can rewrite the type 
of (+) with brackets and get
(+) :: a -> (a -> a)

From that we know that

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

Now that we know what a and b are, let's look at the first argument of (.).

It's (+) applied by an argument b :: (a -> a). So we get
(a -> a) -> ((a -> a) -> (a -> a))

so we found the type of c:
c :: (a -> a) -> (a -> a) 
and since we can remove the second pair of brackets
c :: (a -> a) -> a -> a

if we plug our findings into 

(+) . (+) -> a -> c

we get 

(+) . (+) :: a -> (a -> a) -> a -> a

Answer 4

Ты почти у цели.

(Num i =>)
b = i
c = i -> i
(Num j =>)
a = j -- this is different, you associated b,c correctly but a wrongly
b = j -> j
=> i = j -> j -- ( by i = b = j -> j )
=> c = (j -> j) -> (j -> j) -- ( by c = i -> i, i = j -> j )
=> (+) . (+) :: a -> c = j -> ((j -> j) -> (j -> j)) 
    = j -> (j -> j) -> j -> j -- ( simplifying brackets )

Answer 5

Тип дифференцирования является чисто механической процедурой:

(+) :: Num a => a -> a -> a
(.) :: (       b -> c     ) ->  (       a -> b     )  -> a -> c

(.)    ((+) :: t -> (t->t))     ((+) :: s -> (s->s))  :: a -> c
----------------------------------------------------
            b ~ t, c ~ t->t,          a ~ s, b ~ s->s    s -> (t -> t)
            Num t                     Num s              s -> (b -> b)
            Num b                     Num s              s -> ((s->s) -> (s->s))
            Num (s->s)                Num s              s -> ((s->s) -> (s->s))

(+) . (+) совпадает с (.) (+) (+).

Answer 6

Типы (.) и (+) таковы:

(+) :: Num a => a -> a -> a
(.) :: (b -> c) -> (a -> b) -> a -> c

Мы можем переименовать, чтобы избежать путаницы:

(+) :: Num i => i -> i -> i -- the first (+)
(.) :: (b -> c) -> (a -> b) -> a -> c
(+) :: Num j => j -> j -> j -- the second (+)

Теперь давайте определимся с типом (+) (.). Это (.) с одним примененным аргументом, поэтому результат будет (a -> b) -> a -> c, и мы сопоставили (b -> c) с типом нашего первого (+) так:

(b -> c) = Num i => i -> i -> i
b = i
c = i -> i

(+) (.) :: (a -> b) -> a -> c
= Num i => (a -> i) -> a -> c -- replacing b
= Num i => (a -> i) -> a -> (i -> i) -- replacing c
= Num i => (a -> i) -> a -> i -> i -- simplifying

Теперь мы можем применить второй аргумент к этому. Результат будет a -> i -> i, и мы сопоставим (a -> i) с типом нашего второго (+) так:

(a -> i) = Num j => j -> j -> j
a = j
i = j -> j

(+) (.) (+) :: Num i => a -> i -> i
= (Num i, Num j) => j -> i -> i -- replacing a
= (Num (j -> j), Num j) => j -> (j -> j) -> (j -> j) -- replacing i
= (Num (j -> j), Num j) => j -> (j -> j) -> j -> j -- simplifying