GHC выводит следующий для выражения (flip id) следующий тип: flip id :: b -> (b -> c) -> c.
Я понимаю, каким образом этот тип получается. Достаточно заменить заменить тип функции id на (b -> c) -> b -> c. Но мне неясно, почему такая замена типа делается компилятором (если конечно делается, я мог и ошибиться в своем предположении). Мне кажется такое поведение странным, потому что тип a -> a более общий. Подскажите пожалуйста, где почитать, почему происходит именно так.
Здравствуйте, Аноним, Вы писали:
А>GHC выводит следующий для выражения (flip id) следующий тип: flip id :: b -> (b -> c) -> c.
А>Я понимаю, каким образом этот тип получается. Достаточно заменить заменить тип функции id на (b -> c) -> b -> c. Но мне неясно, почему такая замена типа делается компилятором (если конечно делается, я мог и ошибиться в своем предположении). Мне кажется такое поведение странным, потому что тип a -> a более общий. Подскажите пожалуйста, где почитать, почему происходит именно так.
Коротко — ищется наиболее общий допустимый тип
всего выражения flip id.
Подробнее.
Выпишем явно правую ассоциативность первого аргумента
flip :: (a -> (b -> c) ) -> b -> a -> c
При подстановке
id :: t -> t
в выражении flip id получаем систему равенств
t == a
t == b -> c
Откуда происходит унификация
a == b -> c
Получается, что не всякий id во flip подходит, что ясно и из других соображений: переставлять flip'ом аргументы у совсем общего одноаргументного id — это как выполнять хлопок одной ладонью
Гуглить: Damas-Hindley-Milner; unification.
Здравствуйте, Аноним, Вы писали:
А>GHC выводит следующий для выражения (flip id) следующий тип: flip id :: b -> (b -> c) -> c.
А>Я понимаю, каким образом этот тип получается. Достаточно заменить заменить тип функции id на (b -> c) -> b -> c. Но мне неясно, почему такая замена типа делается компилятором (если конечно делается, я мог и ошибиться в своем предположении). Мне кажется такое поведение странным, потому что тип a -> a более общий. Подскажите пожалуйста, где почитать, почему происходит именно так.
id :: a -> a
flip :: (a -> b -> c) -> b -> a -> c
flip id :: b -> (b -> c) -> c
Применяя flip к id компилятор сопоставляет (a -> a) и (a -> b -> c). Отсюда получается a = (b -> c) и соответствующий тип результата flip id.
Компилятор использует наиболее общий, удовлетворяющий ограничениям, тип. Но т.к. в результате применения функции flip установилось дополнительное ограничение на a, то он и не использует a.
А>GHC выводит следующий для выражения (flip id) следующий тип: flip id :: b -> (b -> c) -> c.
А>Я понимаю, каким образом этот тип получается. Достаточно заменить заменить тип функции id на (b -> c) -> b -> c.
Не "заменить тип id", а совместить структуры типов x -> x и a -> b -> c и произвести подстановку a := b -> c в оставшемся типе flip.
Prelude> :t flip
flip :: (a -> b -> c) -> b -> a -> c
Prelude> :t id
id :: a -> a
Пусть тип id :: x -> x.
flip :: (a -> b -> c) -> b -> a -> c
id :: x -> x
flip :: (a -> (b -> c)) -> b -> a -> c
id :: x -> x
Следует, что
x := a
x := b -> c
Отсюда следует a := b -> c
Выполняем подстановку в типе flip всех a:
flip с подстановкой из-за id. :: ((b->c) -> b -> c)) -> b -> (b -> c) -> c
Самый первый аргумент у нас id, мы его использовали для вычисления подстановок,
поэтому мы его отбрасываем.
Получается
flip id :: b -> (b -> c) -> c
А>Но мне неясно, почему такая замена типа делается компилятором (если конечно делается, я мог и ошибиться в своем предположении).
А>Мне кажется такое поведение странным, потому что тип a -> a более общий. Подскажите пожалуйста, где почитать, почему происходит именно так.
TAPL, Types and programming languages.
