Dlaczego funkcja (+) pasuje do typu (a -> b -> b)? Funkcja

Question

krotnie:

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

zaczerpnięte z http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

Jaki typ (a -> b -> b) mecz z rodzaju a -> a -> a dla (+) funkcji?

Jako że definicja fold przyjmuje typ funkcji (a -> b -> b) oznacza to, że pierwsze 2 parametry (a -> b) muszą być różnych typów?

Answer 1

Nie, wszystko to oznacza, że ​​a i bmoże być różne, ale nie jest to obowiązkowe, aby była ona inna. W twoim przypadku jest to to samo.

znacznie prostszy przykład przekazać punkt:

data SomeType a b = Test a b deriving (Show) 

Teraz w ghci:

Answer 2

myślisz w odwrotnym kierunku. Nie trzeba by sprawdzić, czy + jest identyczna lub mecze a -> b -> b, chcesz rodzaj + być specjalizacja od a -> b -> b i sprawdzić to trzeba ujednolicić typy.

Ujednolicenie oznacza, że ​​chcesz zobaczyć, czy rodzaj i typ +a -> b -> b może być zrównana przez zmiana nazwy zmiennych typu.

Tak + ma typ Num x => x -> x -> x. Zignorujmy teraz ograniczenie klasy i zobaczmy, czy możemy dopasować typy funkcjonalne. Typy stają się x -> x -> x i a -> b -> b. W rzeczywistości jest lepiej, gdy patrzymy na nie takimi, jakimi są naprawdę, bez użycia asocjatywności: x -> (x -> x) i a -> (b -> b).

-> jest konstruktorem typu . To znaczy. jest to funkcja, która odwzorowuje określoną liczbę typów na inny typ. W takim przypadku konstruktor -> odwzorowuje dwa typy: t_1 i t_2 na typ funkcjonalny (->) t_1 t_2 (który jest zwykle oznaczony przez t_1 -> t_2).

Więc typ x -> (x -> x) jest rzeczywiście (->) x ((->) x x) który jest konstruktor typu -> stosowane do x i do konstruktora typu -> stosowanej do x i x. Drugi typ to (->) a ((->) b b).

Podczas ujednolicania należy wziąć pod uwagę najbardziej zewnętrzny konstruktor typów dla obu typów (-> dla obu w tym przypadku). Jeśli to nie pasuje, nie można ujednolicić. W przeciwnym razie musisz ujednolicić argumenty konstruktora.

Więc musimy zjednoczyć x z a. Oba są zmiennymi typu, dzięki czemu możemy zmienić jedną z nich na. Załóżmy, że zmieniamy nazwę na a na x. Teraz stosujemy zmianę nazwy na typy, uzyskując: (->) x ((->) x x) i (->) x ((->) b b) i widzimy, że x i x są teraz zgodne.

Rozważmy drugi argument. Nie jest to zmienna typu, więc musimy dopasować konstruktor typu i dla obu jest to znowu ->. Więc recursywnie prowadzimy argumenty.

Chcemy dopasować x i b. Oba są zmiennymi typu, dzięki czemu możemy zmienić nazwę jednego z nich. Załóżmy, że zmieniamy nazwę na x na b. Zastosujemy tę zamianę do typów, uzyskując: (->) b ((->) b b) i (->) b ((->) b b). Teraz wszystko się zgadza. Dlatego te dwa typy jednoczą się.

odniesieniu do ograniczeń klasy, gdy nazwy x z b zastosowano do podstawienia na ograniczenie zbyt więc Num x się Num b i dwa ostatnie rodzaje są zarówno Num b => b -> b -> b.

Mam nadzieję, że dzięki temu lepiej zrozumiesz, jak działają typy i jak są sprawdzane.

---

Nota boczna: To właśnie robi haskell podczas wykonywania wnioskowania o typ. Najpierw przypisuje do nieznanej funkcji świeżą zmienną typu t. Następnie używa unifikacji, aby uzyskać typ wyrażenia, który ją definiuje i sprawdzić, jaki typ był powiązany z t i jest to typ funkcji.