Понимание упражнения изоморфизма Карри-Говарда из мышления с типами - PullRequest
Новая
       71

Понимание упражнения изоморфизма Карри-Говарда из мышления с типами

4 голосов
/ 13 мая 2019

Я начал читать книгу «Мышление с типами», которая является моим первым опытом в программировании на уровне типов.Автор предлагает упражнение и решение, и я не могу понять, насколько оно правильно.

Упражнение

enter image description here

Я попытался выполнить это упражнение со следующими 

productToRuleMine :: (b -> a, c -> a) -> Either b c -> a
productToRuleMine (f, _) (Left b) = f b
productToRuleMine (_, g) (Right c) = g c

productFromRuleMine :: (Either b c -> a) -> (b -> a, c -> a)
productFromRuleMine f = (f . Left, f . Right)

productToRuleMine . productFromRuleMine = id

Я чувствуюэто правильное решение, однако в книге дано другое решение, которое, похоже, не проверяет тип, что приводит меня к убеждению, что мое общее понимание неверно 

productToRuleBooks :: (b -> a) -> (c -> a) -> (Either b c) -> a
productToRuleBooks f _ (Left b) = f b
productToRuleBooks _ g (Right c) = g c

productFromRuleBooks :: (Either b c -> a) -> (b -> a, c -> a)
productFromRuleBooks f = (f . Left, f . Right)

Единственный способ получить ответы на книгипроверка типа выглядит следующим образом: 

(uncurry productToRule1 . productFromRule1) = id

, поскольку только сигнатуры типов не выстраиваются в линию 

(Either b c -> a) -> (b -> a  ,   c -> a)
                     (b -> a) -> (c -> a) -> (Either b c) -> a

Итак, у меня вопрос: неверно ли мое решение?Почему подпись типа книг для productToRuleBooks принимает в качестве первого и второго аргумента функции b -> a и c -> a, когда я понимаю, что x (multiplication) из алгебры равно (,) в типах, так почему бы и нетв ответе книги (b -> a, c -> a) в качестве первого аргумента?

...