LINUX.ORG.RU

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

 , ,


9

7

Common Lisp разрабатывался и используется в предположении, что пользователь программы — программист. Поэтому из языка намеренно исключены сложные для понимания конструкции (пользователь не обязательно квалифицированный программист), поэтому в языке мощнейший отладчик, позволяющий без остановки программы переопределять функции и вообще делать что угодно. Но из-за этого документация по большей части библиотек Common Lisp существует только в виде docstring и комментариев в коде (некоторые вообще считают, что код сам себе документация). Из-за этого обработка ошибок почти всегда оставляется на отладчик (главное сделать рестарт «перезапустить с последней итерации», а там пользователь сам разберётся). Из-за этого в программе проверяется только happy path (пользователь ведь «тоже программист»).

Racket разрабатывался и используется в предположении, что пользователь программы не программист, а задача разработчика написать программу так, чтобы она корректно работала при любых входных данных (если данные некорректны, то сообщала об этом в том месте, где данные были введены). Поэтому в языке эффективная библиотека для написания тестов, система контрактов на уровне модулей, макимально широкий спектр инструментов программирования (разработчик должен быть профессионалом!). Также реализована идея инкапсуляции: считается, что пользователь модуля не должен знать особенности реализации и, более того, не может в своём коде изменить функцию чужого модуля если это явно не разрешено разработчиком того модуля. Исходный код разумеется доступен, но его не требуется смотреть, чтобы использовать модуль. Достаточно документации. Поэтому реализована мощнейшая система документировния Scribble, а при реализации макроса есть возможность обеспечить указание на ошибки в коде, предоставленном макросу пользователем, не показывая потроха макроса.

И поэтому в Racket нет CLOS (есть как минимум две реализации, но не используются) - провоцирует заплаточное программирование (monkey patching), поэтому отладчик намеренно ограничен (если ты отлаживаешь программу, значит ты не знаешь как она должна работать!), поэтому нет разработки в образе (image based) - она провоцирует разработку через отладку (а значит непонимание программы и проверку только happy path).

Таким образом, Racket и Common Lisp несмотря на внешнее сходство являются очень разными языками. И я рекомендую писать на Racket, если только конечными пользователями программы не являются исключительно программисты на Common Lisp.

Взято с http://racket-lang.blog.ru/#post214726099

Хотелось бы знать, что по этому поводу думают пользователи ЛОРа. А также, мне кажется, что для Java и C++ будет где-то такая же разница.

★★★★★

Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

И чтобы ее исправить надо реализовать инстанс 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 этой подсказки (которая может поломать жизнь лисперам) вообще нету, так что все, проехали пункт можно вообще не рассматривать :)

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

anonymous ()
Ответ на: комментарий от anonymous

Ракетка не говорит что там нум, она говорит что там 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’

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

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

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

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

Правда.

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

id2 :: a -> b
id2 x = x

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

monk ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

monk ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

toInt x = x :: Int

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

monk ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

monk ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от monk

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

в 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.

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

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

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

monk ★★★★★ ()
Ответ на: комментарий от qnikst

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

$ 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

monk ★★★★★ ()
Ответ на: комментарий от monk

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

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

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

foo = undefined
  where
    toInt x = x :: Int

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

qnikst ★★★★★ ()
Ответ на: комментарий от monk

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
qnikst ★★★★★ ()
Последнее исправление: qnikst (всего исправлений: 2)
Ответ на: комментарий от monk

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

qnikst ★★★★★ ()
Ответ на: комментарий от monk

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

monk ★★★★★ ()
Ответ на: комментарий от monk

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от monk

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

что в ракетке

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от qnikst

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от qnikst

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

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

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

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

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

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

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

qnikst ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

qnikst ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.