Анализ пользователей Common Lisp и Racket

Для особо одаренных, чекер должен был показать ошибку вот в этом модуле:

module Test
    where
    strlen x = length

expected: Int
given: String -> Int
in length

чекер должен был показать ошибку

Почему «должен»?

Почему «должен»?

Имелось ввиду «если работает показывает корректно, то он должен показать ошибку ...». Почему? Потому что именно эта ошибка сделана! Если же чекер работает некорректно то он ничего никому не должен, коненчо же.

И в первом и во втором случае тип был a -> String -> Int, разница была в том как его использовали - я правильно и у меня собралось, а monk, как если бы тип был String -> Int, и как не удивительно получил ошибку именно в месте неправильного использования.

Потому что именно эта ошибка сделана!

«Эта ошибка» - примерно то же самое, что в вычислении a*x + b*y забыть y. С точки зрения тайпчекера всё правильно. Максимум, что здесь должно выдаваться - предупреждение о неиспользованной переменной.

Нет. ошибка была в том, что не монк опечатлся и не поставил х. То есть тайпчекер даже МОДУЛЬ с ошибкой указал неверно.

Нет. Все верно. И я повторяю свой вопрос, написав ровно ту же функцию (тип которой ровно тот же) я не опечатался, как быть?

Еще раз, тип функции был String -> Int, тайпчекер вывел a -> String -> Int. То есть тайпчекер вывел НЕВЕРНЫЙ ТИП.

Тип функции был a -> String -> Int, что компилятор и вывел. String -> Int он был только в голове у monk, чтобы объяснить компилятору что нужно проверять контракты из твоей головы нужно дать их в понятном компилятору виде, в данном случае добавить аннотацию типа.

Я прекрасно знаю принципы работы и сам писал чекеры.

Если это правда, то это печально.

Ну проектирование написанием кода осуществляться не может.

Выглядит это примерно так:

http://swizard.info/articles/solitaire/article.html

Смысл в том, что любое проектное утверждение можно записать в виде «фразы со скобками», а во что эта фраза будет раскрываться придумать позже.

Или так

«Наиболее сильной и характерной чертой Common Lisp является мощная поддержка интерактивной разработки, что значительно упрощает постоянный рефакторинг кода и проектирование „снизу вверх“, которые характерны для современных подходов к разработке.» (с) http://archimag-dev.blogspot.ru/2010/08/common-lisp-dsl.html

Нет. Ты уже задолбал, эта абсолютно корректная функция с типом a-> String -> Int, пример кода с её использованием я писал. Почему мне должна выдаваться ошибка?

Здесь компилятрр выдаёт warning - отсутствие сигнатуры у top level метода и неиспользование переменной x. И с -Werror не собирается.

Тип функции был a -> String -> Int, что компилятор и вывел. String -> Int он был только в голове у monk

Ну да, а в программе на фортране Анализ пользователей Common Lisp и Racket (комментарий) было присванивание, а цикл был только в голове у программиста.

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

То есть, почему он считает, что strlen имеет правильный тип, а show неправильный, а не наоборот? И предлагает доопределить show (при следоавнии этому совету программа станет совсем неверной, но компилирующейся).

Либо надо считать ошибочным синтаксис языка, который не разделяет частичное применение функции и недостаточное количество аргументов при вызове.

Если язык при опечатке затрудняет место поиска опечатки

Анализ пользователей Common Lisp и Racket (комментарий)

«warning [...] неиспользование переменной x»

Что еще тебе нужно?

И в первом и во втором случае тип был a -> String -> Int

Нет. Тип ф-и String -> Int. Откуда ты взял вообще a -> String -> Int?

разница была в том как его использовали

Это уже какой-то нереальный сюр. программист: - я допустил опечатку, но тайпинференс показал ошибку не там. Бывает, чо... хаскидебил: - НЕТ ИНФЕРЕНС НЕ МОЖЕТ ОШИБАТЬСЯ ЗНАЧИТ ТЫ НАПИСАЛ ВСЕ ПРАВИЛЬНО

То есть ты на полном серьезе утверждаешь сейчас, что ошибка была там, где показал тайпчекер, и исправить ее надо было дописыванием «лишнего» аргумента? Если да, то разговаривать с тобой смысла нет, т.к. ты - дебил. Если нет - тут еще можно что-то обсуждать.

Так это только в этом частном случае есть неиспользование переменной. Если бы там вместо length было например (+ x), то никакого варнинга не было бы. А ошибка в том же месте.

Ты надеюсь тут не будешь, по крайней мере, как предыдущий оратор утверждать, что раз тайпчекер так сказал, то, значит, функция и должна принимать «лишний» аргумент и исправлять ошибку следует его дописыванием в места вызова?

Прочитай все комментарии адресованные тебе и повторить оставшиеся вопросы, мне не хочется писать очевидные вещи по 15 раз.

Нет. Ты уже задолбал, эта абсолютно корректная функция с типом a-> String -> Int

Нет. Это функция с типом String -> Int, в которой допущена ошибка. То, что ошибка допущена так, что ее можно считать корректной ф-ей с другим типом - ничего не меняет. Ты какой-то ебнутый, рли.

Если я напишу

sortInt = id, то ты назовешь это корректной функцией сортировки? И ошибка по-твоему у нас не в sort а в местах ее использованиЯ, то есть надо везде вместо sortInt lst писать sortInt $ realySortInt lst?

раз тайпчекер так сказал, то, значит, функция и должна принимать «лишний» аргумент

Да. «You asked for it - you get it». То, что ты написал неправильно - твои проблемы.

исправлять ошибку следует его дописыванием в места вызова?

Нет.

А того, что статическая проверка типов избавляет от всех ошибок, никто и не обещал. Если же ты из частных случаев типа «flatten требует докторской диссертации» или «а в некоторых случаях warning может не быть» делаешь глобальные выводы о бесполезности статической типизации вообще - это, опять же, твои проблемы.

sortInt = id, то ты назовешь это корректной функцией сортировки? И ошибка по-твоему у нас не в sort а в местах ее использованиЯ, то есть надо везде вместо sortInt lst писать sortInt $ realySortInt lst?

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

Да. «You asked for it - you get it». То, что ты написал неправильно - твои проблемы.

Вроде смысл статической типизации как раз и состоит в том, чтобы определять ЧТО и ГДЕ я написал неправильно, разве нет? И она, как вдино из примера, не определяет.

Нет. Тип ф-и String -> Int. Откуда ты взял вообще a -> String -> Int?

Из определения функции strl и того факта что у неё отсутствует аннотация типа. А вот откуда ты взял String -> Int это вопрос хороший.

TI - выводит, что есть, а не то, что ты хочешь. Он по определению правильно выводит тип написанной функции, а вот правильно ли ты её написал он не говорит. Если у тебя в голове есть представление о типе функции и ты хочешь чтобы компилятор проверял контракт - напиши тип - передай компилятору сакральные знания!

Ошибки тут две: 1. То что функция strl не отвечает представлению о ней автора кода 2. То что использование функции strl не корректно с т.з. типов.

Вроде смысл статической типизации как раз и состоит в том, чтобы определять ЧТО и ГДЕ я написал неправильно, разве нет?

Нет. Смысл именно статической типизации - найти как можно больше ошибок как можно раньше (т.е. без запуска программы). И с этой задачей в твоем примере она справилась (даже дважды - предупреждением и ошибкой).

sortInt = id - в этом треде я скажу, что имеет тип соотв типу функции сортировки. Но компилятор никак это не проверит реализацию. Это вы утверждаете, что компилятор по названию функции должен угадывать семантику и проверять, или не проверяьь ничего. Хочешь чтобы компилятор проверял контракт - вытаскивай его в type level, какой-нибудь ад тип

data SortedList where
  (>[]) :: SortedList MaxValue a
  (:>) :: (LessThen 'a (MinValue proof)) => a -> SortedList proof a

Или возьмёшь язык умеющий в зависимые типы.

Кстати, про сложение жирафов с носорогами. Порядок в сложении в Haskell принципиально роли не играет?

Prelude Test> 5 + 'a'
'f'
Prelude Test> 'a' + 5
'f'
Prelude Test> 5.1 + 5
10.1
Prelude Test> 5.1 + 5 + 'a'
'l'

А можно сделать, чтобы оно целое число вернуло?

Ладно:

Тайпчеккер в хацкеле не позволит подставить значение вместо enumeration, я выше привёл пример где с TI можно прийти к проблемам, пример сугубо искусственный, но вроде я не видел что кто-то отписался о том что он собрался.

Анализатор ошибок обычно выписывает весь контекст и типы выражений в ошибке (во всяком случае в современных версиях) - информации более чем достаточно, кстати почему ошибка не в show? Или ++? А если выписывать все функции то зачем это делать вообще? :)

Он считает что и show и strlen имеют правлтные типы, а ошибка в том что значение которое ты передаешь в show не отвечает контракту: почему именно предложение добавить инстансы - видимо потому что в большинстве таких случаев это действительно просто отсутствие инстанса и не более того.

:t (+)
:i Num

Отсутствие автоматического приведения типов. Берёшь сопоставляешь и анализируешь.

Из определения функции strl и того факта что у неё отсутствует аннотация типа.

Не понял, какое это имеет отношение ктипу функции?

А вот откуда ты взял String -> Int это вопрос хороший.

Либо из спецификации, либо из головы программиста.

TI - выводит, что есть, а не то, что ты хочешь.

О чем и речь. То, что есть - может быть НЕПРАВИЛЬНЫМ. Вместо того, чтобы указать на ошибку, он считает, что все правильно.

Он по определению правильно выводит тип написанной функции

Ты же сам все как надо сказал. Он не выводит правильный тип функции. Он выводит, то что ЕСТЬ. То, что есть и то, что правильно - не одно и то же, если ты допустил ошибку. То есть инференс работает тогда и только тогда, когда программист не допускает ошибок.

а вот правильно ли ты её написал он не говорит.

Ага. Правильно я написал ф-ю или нет - мне должен говорить тайпчекер. А тайпинференс - это часть тайпчекера (на самом деле процесс инференса и процесс тайпчека - это один и тот же процесс и чекер дает ошибку именно тогда, когда не может вывести типы). И если я написал ф-ю неправильно - он должен дать наиболее точно указание на место и характер ошибки. Это назначение тайпчекера. И если тайпчекер указывает какую-то другую ошибку, не ту, что я допустил - это плохой, негодный тайпчекер.

Если у тебя в голове есть представление о типе функции и ты хочешь чтобы компилятор проверял контракт - напиши тип - передай компилятору сакральные знания!

Точно так же я могу сказать «если у тебя есть в голове тип ф-и - то напиши ее код в соответствии с этим типом». И тогда статическая типизация становится ненужна.

Ошибки тут две: 1. То что функция strl не отвечает представлению о ней автора кода 2. То что использование функции strl не корректно с т.з. типов.

Нет, ошибка одна - п.1. В каком-то ИНОМ случае, вощможно, была ошибка п.2. Тоже одна. Но в данном случае нам достоверно известно, что ошибка п.1. - ну потмоу тчо пример так построен. По определению, ошибка была в опечатке.

(т.е. без запуска программы)

Так, давай не путать вещи. «как можно раньше» и «без запуска программы» - концепты полностью ортогональные. Не будем подменять понятия, ок? Статическая типизация - это именно «без запуска». Но не раньше.

Смысл именно статической типизации - найти как можно больше ошибок

Именно. А «найти ошибку» - это значит указать ее место и характер. Если место и характер указано неточно - то ошибка не считается найденной. Потому что иначе я могу напистьа очень простой тайпчекер который просто в любом случае выводит «в вашей программе есть ошибка» - и это будет верно для любой достаточно большой программы.

И с этой задачей в твоем примере она справилась (даже дважды - предупреждением и ошибкой).

Не справилась. Место и характер ошибки указано неверно. Не указан даже модуль, в котором произошла ошибка, что полный фейл.

Это вы утверждаете, что компилятор по названию функции должен угадывать семантику

Нет, не должен. сколько еще можно повторять? Ты не читаешь, что тебе пишут? Компилятор должен потребовать у программиста информацию достаточную для того, чтобы корректно определить тип. Например в какой-нибудь агде или петушке ты можешь написать ф-ю сортировки с соответсвующим типом (которая вернет не просто лист, а сортед лист), но у тебя чекер потребует ДОКАЗАТЕЛЬСТВО. И пока ты не предоставишь доказательство, из которого чекер сможет с гарантией вывести, что возвращаемый тип - сортед, он программу не допустит. Он будет требовать у программиста уточнения. Здесь он должен поступать также - требовать у программиста уточнения до тех пор, пока не сомжет гарантировать, что тип корректен.

кстати почему ошибка не в show? Или ++?

А, кстати, почему?

Он считает что и show и strlen имеют правлтные типы

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

Не понял, какое это имеет отношение ктипу функции?

К типу функции может иметь отшонение только аннотация (она же контракт), которая отсутствует или сам код функции, который присутствует и тип которого a -> String -> Int и никакой другой.

Либо из спецификации, либо из головы программиста.

Спецификации не было, из головы программиста это угадывание, чему компилятор не обучен. Так что дурацкое у тебя предположение о типе.

Ага. Правильно я написал ф-ю или нет - мне должен говорить тайпчекер.

Нет. Тайпчеккер говорит сходятся ли у тебя типы. Пространство корректных функций является подпространством корректно типизированных функций, которое является подпространством всех функций, так что извини тайпчеккер делает что может, но сделать то для чего он не обучен не может. Хочешь - вытаскивай в type level то что надо проверять.

И если я написал ф-ю неправильно - он должен дать наиболее точно указание на место и характер ошибки.

Только с точки зрения типизации, в примере выше - он справился. С точки зрения типизации функция имеет корректный тип выведенный тайпчеккером.

Точно так же я могу сказать «если у тебя есть в голове тип ф-и - то напиши ее код в соответствии с этим типом». И тогда статическая типизация становится ненужна.

Только тайпчеккер проверит соотв типов в компайл тайм, а без статической типизации не проверит, а так да, все тоже.

Нет, ошибка в п1 и в п2 а что вы там по определению себе придумывали волнует мало кого, кроме вас :).

А, кстати, почему?

Потому, что они корректно типизированы, как и strl, т.е. верны с т.з. тайпчеккера.

а почему он так считает? Вот должен не считать, а требовать дополнительной информации

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

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

В нашем случае он никого не выбирает и не предпочитает одних другим. Ты точно тайпчеккеры писал?

Компилятор должен потребовать у программиста информацию достаточную для того, чтобы корректно определить тип.

Должен ли я этот читать как - компилятор обязан требовать аннотаций типа у абсолютно всех функций и абсолютно всех их применений? И с выводом т.к. абсурд, а в противоположном случае типизация не даёт гарантий, то она не нужна совсем?

К типу функции может иметь отшонение только аннотация (она же контракт)

Исправить ошибку можно либо исправив контракт (тип) функции strlen, либо исправив контракт show (добавив instance). Чекер предлагает только вариант с show. Должно быть что-то наподобие «или strlen должен иметь тип, или ++ должен иметь тип...»

С точки зрения типизации функция имеет корректный тип выведенный тайпчеккером

У show тоже корректный тип. Почему предлагается расширять его?

Вот ещё пример:

Prelude Test> Behemoths 5 + 5
Behemoths 10
Prelude Test> Giraffes 5 + 1
Giraffes 6
Prelude Test> Behemoths 5 + Giraffes 1

<interactive>:4:15:
    Couldn't match expected type `Behemoths'
                with actual type `Giraffes'
    In the return type of a call of `Giraffes'
    In the second argument of `(+)', namely `Giraffes 1'
    In the expression: Behemoths 5 + Giraffes 1
Prelude Test> Giraffes 5 + Behemoths 1

<interactive>:5:14:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `(+)', namely `Behemoths 1'
    In the expression: Giraffes 5 + Behemoths 1

Почему чекер уверен, что ошибка во втором аргументе? Более того:

Prelude Test> Giraffes 5 + Behemoths 2 + Behemoths 3 + Behemoths 1

<interactive>:6:14:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `(+)', namely `Behemoths 2'
    In the first argument of `(+)', namely `Giraffes 5 + Behemoths 2'

<interactive>:6:28:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `(+)', namely `Behemoths 3'
    In the first argument of `(+)', namely
      `Giraffes 5 + Behemoths 2 + Behemoths 3'

<interactive>:6:42:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `(+)', namely `Behemoths 1'
    In the expression:
      Giraffes 5 + Behemoths 2 + Behemoths 3 + Behemoths 1

Чекер считает неверными все аргументы кроме первого. «Все не в ногу, первый в ногу». И это в тривиальном случае.

компилятор обязан требовать аннотаций типа у абсолютно всех функций

В Typed Racket так и есть. Если нет аннотации, значит программист заявляет, что функция может принимать аргументы любого типа (Any) и это проверяется.

Почему чекер уверен, что ошибка во втором аргументе?

Потому что ты не сказал ему по-другому. Сделай функцию add с аннотациями типов.

Так, давай не путать вещи. «как можно раньше» и «без запуска программы» - концепты полностью ортогональные. Не будем подменять понятия, ок?

Я не вижу путаницы и подмены, но окей - «без запуска». Меня устраивает.

«найти ошибку» - это значит указать ее место и характер.

Так натянуто, что сейчас порвется...

Если место и характер указано неточно - то ошибка не считается найденной

...порвалось.

Не указан даже модуль, в котором произошла ошибка,

Про наведенные ошибки слышал?

что полный фейл.

Мде. Какой-то подростковый максимализм.

Сделай функцию add с аннотациями типов.

Хочешь сказать, в стандартном «+» не написали аннотации?

Ну ладно.

add :: Num a => a -> a -> a
add x y = x + y

Prelude Test> add (add (add (Giraffes 1) (Behemoths 1)) (Behemoths 2)) (Behemoths 3)

<interactive>:5:29:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `add', namely `(Behemoths 1)'
    In the first argument of `add', namely
      `(add (Giraffes 1) (Behemoths 1))'

<interactive>:5:44:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `add', namely `(Behemoths 2)'
    In the first argument of `add', namely
      `(add (add (Giraffes 1) (Behemoths 1)) (Behemoths 2))'

<interactive>:5:59:
    Couldn't match expected type `Giraffes'
                with actual type `Behemoths'
    In the return type of a call of `Behemoths'
    In the second argument of `add', namely `(Behemoths 3)'
    In the expression:
      add
        (add (add (Giraffes 1) (Behemoths 1)) (Behemoths 2)) (Behemoths 3)

Опять предлагает исправить не в одном месте, а в трёх.

«найти ошибку» - это значит указать ее место и характер.

Так в Racket работает. Значит возможно.

Потому, что они корректно типизированы, как и strl, т.е. верны с т.з. тайпчеккера

А зачем нам точка зрения тапчекера? Кого она может интересовать?

Потому что ты не передал спецификацию, которую он должен проверять.

Так у меня никто и не требовал. Раз не требуется - значит она, полагаю, чекеру не нужна, чтобы вывести ПРАВИЛЬНЫЙ тип (из моих мыслей). Если нужна - то пусть требует.

В нашем случае он никого не выбирает и не предпочитает одних другим.

Вроде ты сам сверху указал - ошибка могла быть в ++, в show, в length - короче в куче ф-й. Но чекер ВЫБРАЛ именно одну из них. Или ты под понятием «выбор» подразумеваешь что-то отличное от того, что подразумевают другие люди?

На самом деле, кстати, если написать алгоритм инференса по-другому (и при этом он останется корректен!), то ошибка будет в другом месте :)

Место в котором будет выдана ошибка зависит от того, как именно происходит унификация. А ее можно проводить в «разном порядке», с сохранением результата.

Должен ли я этот читать как - компилятор обязан требовать аннотаций типа у абсолютно всех функций и абсолютно всех их применений?

При чем тут применения? Только у ф-й. В идеале, да.

Исправить ошибку можно либо исправив контракт (тип) функции strlen, либо исправив контракт show (добавив instance).

Еще можно дописать аргумент в вызове strlen, то есть вызывать ее как strlen str huy.Тогда даже результат итоговой программы будет правильный. Но это очевидно не будет правильным фиксом.

Исправить ошибку можно либо исправив контракт (тип) функции strlen, либо исправив контракт show (добавив instance). Чекер предлагает только вариант с show. Должно быть что-то наподобие «или strlen должен иметь тип, или ++ должен иметь тип...»

Т.к. у тебя проблема в следующем коде: show (strlen «foo»), тут strlen «foo» имеет корректный тип :: String -> Int. А тип show :: Show a=> a -> String, очевидно, что String -> Int является 'a', но вот констрейнт Show (String -> Int) не выполняется, о чем тебе компилятор и сказал, можно ругать его за попцлярную подсказку, но ошибку он указал верно. Исправить её можно как угодно: 1. Дать инстанс 2. Изменить show 3. Изменить strlen 4. Переписать все 5. Нанять фирму консультантов и научиться наконец языку. Но компилятор предлагает только 1 т.к. остальные функции well typed (кстати одноименная фирма является фирмой консультантами).

У show тоже корректный тип. Почему предлагается расширять его?

Это нигде не предлагается.

Про жирафов и бегемотов: операция не равно коммутативна a != b <=> b != a. А кто там правильный кто нет - решать тебе.

Патетискские вопросы типа 'и это ещё простой случай' делать не стоит, т.к. я не уверен, что не простые случаи ты когда-либо писал :) а то меня достанет и я поирачу пол дня на 'изучение' лиспа и буду глупые вопросы тут задавать :)

Так натянуто, что сейчас порвется...

Что натянуто? А что ты понимаешь под «найти ошибку»? Указать сам факт ее наличия? Н см. выше про простейший тайпчекер.

Т.е. в функциях: map, map (+1), map (+1) [1,2,3], b = map (+1) [1,2,3] я должен сделать аннотации типов?

Т.к. у тебя проблема в следующем коде: show (strlen «foo»)

Нет, в этом коде проблем нет. Давай ты не будешь под дурачка косить?

«найти ошибку» - это значит указать ее место и характер.

Так в Racket работает. Значит возможно.

Какой Racket, Typed? Ты хочешь сказать, что Typed Racket _всегда_ правильно указывает место ошибки?

Сделай функцию add с аннотациями типов.

Хочешь сказать, в стандартном «+» не написали аннотации?
Ну ладно.

add :: Num a => a -> a -> a

Не шлангуй. Ты указал «функция принимает аргументы одинакового типа», а для получения сообщения об ошибке, которое ты хочешь, нужно указать «функция принимает двух бегемотов».

Т.е. в функциях: map, map (+1), map (+1) [1,2,3], b = map (+1) [1,2,3] я должен сделать аннотации типов?

в b должен, в осатльном - нет, т.к. там нету никаких других функций. То, что возвращает map, ты уже указал в самом типе map.

При том что plus1 :: Int -> Int мы её применяем: plus1 1, но это ошибка т.к. это не соответствует специкации в моей голове, что результат должен быть String.

А вот ещё C++14:

#include <cstring>
auto len = [](auto x) { return strlen; };
int main() { return len(42)("12345"); /* 5 */ }

ведь в хаскеле strlen x = length это strlen = \x -> length (~ auto len = [](auto x) { return strlen; };) или strlen = \(x :: a) -> length, где length :: String -> Int, вот и получается a -> String -> Int — обычное такое лямбда-исчисление.

Что натянуто?

Там процитировано.

А что ты понимаешь под «найти ошибку»? Указать сам факт ее наличия?

И дать информацию по поиску этой ошибки. Предупреждение о неиспользуемой переменной прямо указывает на ошибку.

Не шлангуй. Ты указал «функция принимает аргументы одинакового типа», а для получения сообщения об ошибке, которое ты хочешь, нужно указать «функция принимает двух бегемотов».

Ну на самом деле более умный алгоритм инференса в данном случае вполне мог бы этот случай разрешить. То есть падать не там где упало (как делает нынешний инференс) а там, где получилось унифицировать «максимум». В racket например в syntax-parse парсинг идет по такому принципу - указывается не первая ошибка, из-за которой парсинг не возможен, а та, при которой сматчено как можно больше.