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

так если мы складываем её с чем-то, то в ракетке выводится Num, а в haskell выводится 'Num a => a'.

В хаскеле - выводится, в ракетке - не выводится.

В haskell 'a' подставляется тогда и только тогда, когда на вход функции могут поступать _любые_значения_, соотвественно использующий ее код может подставлять туда что угодно и это будет корректно.

Угу. То есть в хаскиле эта функцию возвращает самый узкий тип, который можно засунуть куда угодно. В ракетке обратная ситуация - пока сам программист тип не сузит, он будет наиболее общий.

Это значит, что т.к. ты используешь show, то у параметра должен присутсвовать инстанс Show, данная ошибка обозначает, что проблема в аргументе передаваемом show, а не в show.

И чтобы ее исправить надо реализовать инстанс show для параметра, так?

Ты с концепцией интерфейсов знаком? В ракетке есть они? Просто видимо нужно на чем-то более доступном объяснять :/

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

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

Он имеет ввиду что у Num один параметр и его нельзя доопределить так, чтобы аргументы/результат были разного типа.

В хаскеле - выводится, в ракетке - не выводится.

ракетка мне говорит, что там Num, как это не выводится?!

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

в хацкеле отвечается, что в эту функцию можно подставить любой тип, и функция вернёт тот же тип, что ей передали, в ракетке говорится, что в эту функцию можно подставить Any (т.е. любой тип), и она вернёт Any (т.е. любой тип, не обязательно равный предыдущему). В haskell засунуть тип можно не куда угодно, а только туда, где он проходит от статически проверяемые ограничения.

И чтобы ее исправить надо реализовать инстанс show для параметра, так?

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

Например:

Prelude> data N = N
Prelude> show N

<interactive>:3:1:
    No instance for (Show N) arising from a use of ‘show’
    In the expression: show N
    In an equation for ‘it’: it = show N

О, в 7.8 этой подсказки (которая может поломать жизнь лисперам) вообще нету, так что все, проехали пункт можно вообще не рассматривать :)

ракетка мне говорит, что там Num, как это не выводится?!

Ракетка не говорит что там нум, она говорит что там Any (то есть что угодно, информации о типе нет). Откуда ты взял num?

в хацкеле отвечается, что в эту функцию можно подставить любой тип

Это не важно. Смысл один - (f x) можно подставить _куда угодно_.

В haskell засунуть тип можно не куда угодно, а только туда, где он проходит от статически проверяемые ограничения.

Результат f в данном случае удовлетворяет _любым_ ограничениям. С-но, его можно засунуть куда угодно.

нет, с чего ты взял?

Мне так компилятор сказал :(

Чтобы её исправить нужно посмотреть на блок кода (скопирован в ошибке со типами всех интересующих функций) и подумать, что тут не так.

А там все так. Потому что ошибка не в этой ф-и. И даже не в этом модуле :(

О, в 7.8 этой подсказки (которая может поломать жизнь лисперам) вообще нету, так что все, проехали пункт можно вообще не рассматривать :)

Зачем ты говоришь «лисперы» подразумевая программистов? Программы пишут не только лисперы ;)

Одно из популярных решений - это добавление инстанса, но в этой ситуации оно очевидно не верное (и не реализуемое без предупреждений компиляции).

почему неверное? Кому очевидно? С чего ты взял что нереализуемо? Вполне реализуемо.

Ракетка не говорит что там нум, она говорит что там Any (то есть что угодно, информации о типе нет). Откуда ты взял num?

num был про случай, (define (plus1 x) (x+1)).

Это не важно. Смысл один - (f x) можно подставить _куда угодно_.

но это не правда.

Результат f в данном случае удовлетворяет _любым_ ограничениям. С-но, его можно засунуть куда угодно.

id 7 ++ "show"
Prelude> id 7 ++ "show"

<interactive>:69:4:
    No instance for (Num [Char]) arising from the literal ‘7’

смотри, ка не подставилось, почему?

Мне так компилятор сказал :(

сволочь он, что я могу сказать, но вроде как уже исправился.

А там все так. Потому что ошибка не в этой ф-и. И даже не в этом модуле :(

это печаль. Но это нормально, даже в случае с тестами: пусть есть модуль 'plus a b = a - b', есть куча тестов к модулю, которые это не отловили. Есть модуль 'norm a b = plus (map (^2) a) (map (^2) b)' а тут проверили и отловили, в итоге ошибка тестов будет в другом модуле. Тоже самое и с проверкой типов: тайпчеккер тебе показал, где проблема с типами, проблема с типами может быть из-за проблемы в аргументах (именно то место), или проблеме в используемых функциях - другой модуль. Понять это уже должен программист, в этом примере наглядно видно, что компилятор показывает достаточно информации для этого так что даже в код лезть не надо. Тайпчеккер как подсказывает его называние проверяет только типы, а не корректность. В статически типизированном языке correct => well typed, обратное неверно, но ! well typed => ! correct.

Пока лисперы были едиственными, кто ругался на подобный пример. Впрочем я согласен - дурацкая подсказка была.

Если определишь такой инстанс, то он будет сиростким => предупреждение при компиляции. Так что чтобы делать без предупреждения это только через заворачивание в newtype

num был про случай, (define (plus1 x) (x+1)).

(define (plus1 x)
  (+ x 1))

. Type Checker: type mismatch
  expected: Number
  given: Any in: x
> 

где ты там нум увидел?

но это не правда.

Правда.

смотри, ка не подставилось, почему?

id 6 ++ «show» - прекрасно подставилось

сволочь он, что я могу сказать, но вроде как уже исправился.

Нет. Все про какой-то там инстанс show твердит

это печаль. Но это нормально

Нет, это ненормально. Когда тебе говорят «где-то среди 100мб исходников у вас есть ошибка», то толку от этого ноль.

Number, Num, какая разница, смысла не меняет. Если ты в Haskell поставишь явно, 'а' там где будет констрейнт, то увидишь аналогичную ошибку.

id 6 ++ «show» - прекрасно подставилось

Прекрасно подставилось, но выдало ошибку?

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

Что? оО Где же ее достаточно?

Number, Num, какая разница, смысла не меняет.

У тебя пиздоглазие? Еще раз - там нету нум. И намбер нету. Там Any. В хаскеле такая функция чекается, в ракетке - ошибка.

Если ты в Haskell поставишь явно, 'а' там где будет констрейнт, то увидишь аналогичную ошибку.

Мы говорим о том случае, когда типы не указаны. Поведение чекера в случае указанных типов мы не обсуждаем.

Нет. Все про какой-то там инстанс show твердит

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

Нет, это ненормально. Когда тебе говорят «где-то среди 100мб исходников у вас есть ошибка», то толку от этого ноль.

Передергиваешь, он тебе говорит конкретное место и контекст.

В хацкеле если у функции не указан тип, то её тип выводится локальным type inferring, если указан, то проверяется, что тип указанный пользователем является типом основанным на локальном выводе типов. В ракетке, если тип не указан, то считается что пользователь указал тип Any, и переходим к случаю если тип указан. В случае если пользователь указал тип то проверяется, что он уже, чем тип полученный в результате локального вывода типов.

Итого разница тут в типе функции по умолчанию - в ракетке программиста просят указать тип, если он не равен Any, в Haskell - не просят, при этом и в том и в другом случае функция будет иметь один и тот же тип, modulo subtyping/type classes.

В хацкеле если у функции не указан тип, то её тип выводится локальным type inferring, если указан, то проверяется, что тип указанный пользователем является типом основанным на локальном выводе типов. В ракетке, если тип не указан, то считается что пользователь указал тип Any, и переходим к случаю если тип указан. В случае если пользователь указал тип то проверяется, что он уже, чем тип полученный в результате локального вывода типов.

Именно. В хаскеле если тип не указан то чекер пытается поставить его наугад. В ракетке если тип не указан - то он остается не указанным.

Итого разница тут в типе функции по умолчанию - в ракетке программиста просят указать тип,

Ну да. В хаскеле чекер пытается «угадать» информацию. В ракетке же чекер полагается лишь на ту информацию, которую ему дал программист.

У тебя ведь хватает квалификации чтобы проанализировать, что конкретно он пишет, и что это обозначает

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

Передергиваешь, он тебе говорит конкретное место и контекст.

Говорит, но это не то место. Даже не та функция. Даже не тот модуль.

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

Кстати, в Haskell, похоже, в принципе тип нельзя руками указать не тот, что выведется автоматически. Аналог : Any -> Any (define (f x) x)

id2 :: a -> b
id2 x = x

не скомпилируется. Так как выведен a->a и он не совпадает с a->b.

Можно всякие:

toInt x = x :: Int

тебе все равно придется перепидорасить все сорцы, чтобы понять, что не так

Ну если есть IDE, показывающее (выведенные) типы функций под курсором и позволяющее перейти к исходнику функции, то всё не так страшно.

Разве что в ситуации, где надо программой работает много программистов, претензия (багрепорт) будет направлена не тому программисту :-)

Именно. В хаскеле если тип не указан то чекер пытается поставить его наугад. В ракетке если тип не указан - то он остается не указанным.

да не наугад, а ровно тем же алгоритмом (+- ньюансы), что в ракетке, но ракетка явно спрашивает пользователя о том, правильно ли она угадала. Я в чем-то согласен с таким подходом, во всяком случае для top-level функций.

Ну да. В хаскеле чекер пытается «угадать» информацию. В ракетке же чекер полагается лишь на ту информацию, которую ему дал программист.

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

toInt x = x :: Int

Это всё равно тело функции, а не описание её типа.

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

Нет. В ракетке я могу произвольно сузить тип аргументов и произвольно расширить тип результата. И именно указанный мной тип (а не выведенный) будет проверяться при использовании функции.

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

Спешу обрадовать, в реальности таких ошибок (где из-за ошибки типа придётся пересмотреть все сорцы) вообще не встречается :), встречаются другие проблемы в т.ч. с типами, но о них почему-то в тредах на лоре и т.п. разговор заходит крайне редко. Для следующего «вброса» советую взять какую-нибудь библиотеку, где слишном много используются классы типов, например lens, написать кривой код и словить ошибку типов на 3 страницы на 3-4, (только берите ghc-7.4 или 7.6, там это эффектнее).

Говорит, но это не то место. Даже не та функция. Даже не тот модуль.

именно то место, где ошибка дальше ты видишь, что тип того, что ты подставляешь в show - не тот что ты ожидаешь (у тебя тут всего 2 варианта), удивляешься и смотришь почему - видишь, что strlen не такого типа, что ты ожидал - идёшь и разбираешься, видишь, что тот человек, что писал код не проставил сигнатуру типа у top-level модуля, несмотря на то, что это обязательное требование у закоммиченного кода и делаешь git blame, фиксишь - устраиваешь разнос тому, из-за кого тебе пришлось потратить время.

тип toInt будет :: Int -> Int, что не так?

В ракетке я могу произвольно сузить тип аргументов

в haskell я тоже могу.

произвольно расширить тип результата.

тут да, из-за отсуствия subtyping, такая вещь как «расширение» результа не очень определена, но тем не менее я могу кое-что делать

addX :: Num a => a -> Int
addX = fromIntegral . (+1)

а могу расширить:

addX :: (Num a, Num b) => a -> b
addX = fromIntegral . (+1)

Естественно это не аналог.

впрочем и то и другое а). является частным случаем того, что я написал, т.к. $ f :: A -> B, где A=(a1,..aN), то если A_i* < a_i, а B* > B, то (A_1*,..A_N*) -> B$ будет более узким типом б). не относится к случаю не указывания сигнатуры.

И именно указанный мной тип (а не выведенный) будет проверяться при использовании функции.

Указанный тип является подтипом выведенного, впрочем в haskell как я уже не раз писал выше ровно та же ситуация modulo subtyping/type-classes.

тип toInt будет :: Int -> Int

То, что всё равно придётся писать

toInt :: Int -> Int
toInt x = x :: Int

То есть тип зависит только от тела функции и его нельзя менять не меняя тела функции.

тем не менее я могу кое-что делать

$ cat Test.hs
module Test
    where

addX :: Num a => a -> Int
addX = fromIntegral . (+1)

addX2 :: (Num a, Num b) => a -> b
addX2 = fromIntegral . (+1)

$ ghc Test.hs
[1 of 1] Compiling Test             ( Test.hs, Test.o )

Test.hs:5:8:
    Could not deduce (Integral a) arising from a use of `fromIntegral'
    from the context (Num a)
      bound by the type signature for addX :: Num a => a -> Int
      at Test.hs:4:9-25
    Possible fix:
      add (Integral a) to the context of
        the type signature for addX :: Num a => a -> Int
    In the first argument of `(.)', namely `fromIntegral'
    In the expression: fromIntegral . (+ 1)
    In an equation for `addX': addX = fromIntegral . (+ 1)

Test.hs:8:9:
    Could not deduce (Integral a) arising from a use of `fromIntegral'
    from the context (Num a, Num b)
      bound by the type signature for addX2 :: (Num a, Num b) => a -> b
      at Test.hs:7:10-33
    Possible fix:
      add (Integral a) to the context of
        the type signature for addX2 :: (Num a, Num b) => a -> b
    In the first argument of `(.)', namely `fromIntegral'
    In the expression: fromIntegral . (+ 1)
    In an equation for `addX2': addX2 = fromIntegral . (+ 1)

ghci намекает

Prelude> let f = fromIntegral . (+1)
Prelude> :t f
f :: Integer -> Integer

То есть тип зависит только от тела функции и его нельзя менять не меняя тела функции.

да, тип выводящийся и проверяющийся тип функции это поиск ограничений на входящие и возвращаемые значения, которые обязаны выполняться для того, чтобы функция была well typed.

Писать сингатуры нужно для top-level выражений, т.е. если у тебя что-то вроде

foo = undefined
  where
    toInt x = x :: Int

то сингатуру можешь и не писать.

s/Num/Integral/ я с телефона писал, так что не очень осторожно.

Prelude> :{
Prelude| let addX :: Integral a => a -> Int
Prelude|     addX = fromIntegral . (+1)
Prelude| :}
Prelude> :t addX
addX :: Integral a => a -> Int
Prelude> :{
Prelude| let addX :: (Integral a, Integral b) => a -> b
Prelude|     addX = fromIntegral . (+1)
Prelude| :}
Prelude> :t addX
addX :: (Integral b, Integral a) => a -> b

не забываем :set -XNoMonomorphismRestriction, чтобы default rules не сбивали.

Попадание в инстанс будет на случайным, а подчиняться законами.

Фишка в том что ошибка в общем может быть как угодно далеко и будешь через 100 ф-й прыгать.

let addX :: Integral a => a -> Int

Действительно. Работает. Удивлён.

Кстати, в Haskell, похоже, в принципе тип нельзя руками указать не тот, что выведется автоматически. Аналог : Any -> Any (define (f x) x)

Более узкий может быть.

Маловероятно, даже если не следовать минимальным общепринятым нормам. Впрочем с тестами ровно та же фигня - падающий тест не гарантирует того, что тебе не придется проползти 100 функций в поисках причины бага.

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

А в ракетке есть интерфейсы? Я б тогда продемонстрировал прочие отличия в ТИ и аналог обсуждаемой программы?

Ответ, оно зовется typed class и пока экспериментальное, чтож тогда придется или подождать или объяснять на пальцах :)

да не наугад, а ровно тем же алгоритмом

Это и есть наугад.

что в ракетке

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

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

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

Спешу обрадовать, в реальности таких ошибок (где из-за ошибки типа придётся пересмотреть все сорцы) вообще не встречается :)

Встречаются и часто. Именно по этому все адекватные люди, пишущие на хаскеле, указывают типы для топлевел функций.

Для следующего «вброса» советую взять какую-нибудь библиотеку, где слишном много используются классы типов, например lens, написать кривой код и словить ошибку типов на 3 страницы на 3-4, (только берите ghc-7.4 или 7.6, там это эффектнее).

Ну да, это тоже проблема.

именно то место, где ошибка

Еще раз - ошибка в другом месте. В другой функции. В другом модуле.

ты видишь, что тип того, что ты подставляешь в show - не тот что ты ожидаешь

Но ошибка ведь не в этом. Ошибка в том, что strLen возвращает не то, что нужно.

Указанный тип является подтипом выведенного, впрочем в haskell как я уже не раз писал выше ровно та же ситуация modulo subtyping/type-classes.

Зачем ты повторяешь неправду? Я же показал код, из которого совершенно ясно, что ситуация не такая.

Это и есть наугад.

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

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

Мне кажется что разговор зашёл в тупик. Наверное единственный вариант продолжить его это услышать от тебя описание на пальцах того, как работает type inferring с описанием на каждом пункте что проверяется и какие гарантии даются.

В так же того, что ТВ согласишься, что тайпчеккер проверяет то что программа правильно типизирована, а не корректна и в этом его цель.

Иначе мы живём в разной аксиоматике и спор не имеет смысла.

Маловероятно, даже если не следовать минимальным общепринятым нормам

Проблема в том что хаскель не форсирует эти нормы. Более того - идеологически и концептуально хаскель как раз стимулирует топ-левел аннотации НЕ ПИСАТЬ.

Впрочем с тестами ровно та же фигня - падающий тест не гарантирует того, что тебе не придется проползти 100 функций в поисках причины бага.

Но при чем тут тесты?

Почему с типами такая ситуация маловероятна я строго доказать не могу

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

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

Что значит «наугад проверяет»? Ракетка ничего наугад не делает. Сперва требует спецификацию, потом проверяет, соответствует ли реализация этой спецификации. Хаскель угадывает спецификацию, при чем угадывает так, чтобы реализация была заведомо корректна и по-этому ему проверять ничгео не надо.

Наверное единственный вариант продолжить его это услышать от тебя описание на пальцах того, как работает type inferring с описанием на каждом пункте что проверяется и какие гарантии даются.

Открой тапл и посмотри как работает хиндли-милнер, в чем проблема?

В так же того, что ТВ согласишься, что тайпчеккер проверяет то что программа правильно типизирована, а не корректна и в этом его цель.

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

[..] все адекватные люди, пишущие на хаскеле, указывают типы для топлевел функций.

Мне казалось, что эта идея красной нитью проходила через добрую половину моих комментариев.

Вообще в хацкеле сначала пишутся типы, а потом код. А типы ещё и для документации пишут - удобно ведь.

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

Ну да, это тоже проблема.

Это как раз такм проблема, тут уже даже интересно говорить будет.

Еще раз - ошибка в другом месте. В другой функции. В другом модуле.

Ошибка типизации тут - ошибка в логике в другом месте. Но не в любом а в том, что связан с данным конекстом, причем поиск будет линейным, т.е. кюна каждом шаге у тебя будет единственная ветка где ошибка.

Но ошибка ведь не в этом. Ошибка в том, что strLen возвращает не то, что нужно.

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

Цель тайпчекера - проверка корректности программы, он делает это при помощи проверки типов.

Ну ок, поговорили ;) спасибо за разговор.