Упростить подписи типа Haskell

Question

Мой вопрос - о том, как аналитически работать с сигнатурами типа Haskell. Для того, чтобы сделать бетон, я смотрю на функции «исправления»:

fix :: (a -> a) -> a 

и немного выдуманные функции, которую я написал, чтобы сделать Пеано-иш дополнения:

add = \rec a b -> if a == 0 then b else rec (a-1) (b+1) 

Когда я анализирую типы, я получу ожидаемый тип для fix add:

fix add :: Integer -> Integer -> Integer 

И это, кажется, работает, как я ожидал:

> (fix add) 1 1 
2 

Как я могу работать с типом сигнатур для fix и для add, чтобы показать, что у fix add есть подпись подписи? Что такое «алгебраический», если это даже правильное слово, правила работы с типом подписей? Как я могу «показать свою работу»?

Answer 1

ghci говорит нам

add :: Num a => (a -> a -> a) -> a -> a -> a

по модулю некоторые шумы, так как класс типов второй аргумент add требует Eq экземпляра (вы проверяете его на равенство с 0)

Когда мы применяем fix к add, подпись для fix будет

fix :: ((a -> a -> a) -> (a -> a -> a)) -> (a -> a -> a)

Помните, что a s в fix :: (a -> a) -> a может иметь любой типа. В этом случае они имеют тип (a -> a -> a)

Таким образом, fix add :: Num a => a -> a -> a, что является правильным выбором для добавления двух a.

Вы можете работать с сигнатурами типа Haskell в очень алгебраической форме, переменная подстановка работает так же, как вы ожидали. Фактически, theres прямой translation между типами и алгеброй.