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

Давай, правда единственная возможность это сделать это перестать оьращать внимание на твой бред.

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

Я имею ввиду в каком смысле натянуто?

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

Хватит уже про свое предупреждение, оно к обсуждаемому коду отношения не имеет.

strLen x = (+ x) - нету никакого предупреждения, ситуация та же самая.

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

Хватит уже про свое предупреждение, оно к обсуждаемому коду отношения не имеет.

Оно на нем выдается? Если да, то имеет.

strLen x = (+ x) - нету никакого предупреждения, ситуация та же самая.

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

Я так не утверждал, советую перечитать, а за одно отличать correct от well typed.

Про жирафов и бегемотов: операция не равно коммутативна a != b <=> b != a

Вот именно! Но тип почему-то выводится из первого аргумента (хотя они равнозначны). Если бы он писал «не могу унифицировать первый и второй аргумент, требуется, чтобы они были одного типа», было бы корректно. Но в существющем виде проще разбирать ошибки из template'ов C++ (они многословные, но хоть корректно сформулированные), чем то, что выдает чекер Haskell'а.

Ещё из «хороших опечаток» с неожиданным эффектом:

Prelude Test> [1,1,2,3,4,5,6,7,9,0]
[1,1,2,3,4,5,6,7,9,0]
Prelude Test> [1,1,2,3,4,5,6,7,9.0]
[1.0,1.0,2.0,3.0,4.0,5.0,6.0,7.0,9.0]

Это как раз про то, что Haskell со строгой типизацией и не приводит типы автоматически.

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

Ну на самом деле более умный алгоритм инференса в данном случае вполне мог бы этот случай разрешить.

Наверное. Но задача «не допустить сложения бегемотов с не-бегемотами» - это не задача «не допустить сложения животных разных пород».

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

Вот именно!

Может трактат ещё написать и ссылки на главы из простенькой книжки типа пирса? Твой вариант её несет нисколько дополнительной информации, а вот его реализация существенно усложняется.

Это как раз про то, что Haskell со строгой типизацией и не приводит типы автоматически.

Куда можно нажать, чтобы ты таки начал пытаться разбираться в том что происходит, а не почтить вещи (с неверными выводами) думая что это окровение?

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

Если ты написал plus1 :: Int -> Int (а значит это соответствует спецификации в твоей голове), то plus1 1 будет иметь тип Int, ведь в твоей голове есть логика и нет шизофрении.

Нет, я просто опечатался и забыл применить к этому show, а чеккер гад не проверил это. (Если что это калька с вас)

Твой вариант нё несет нисколько дополнительной информации

Я всего лишь пытаюсь донести до тебя, что если задача «сделать язык с выводом типов», то получится Haskell, а если задача «сделать язык, в котором система типов позволяет не запуская программу найти ошибку», то получится Typed Racket. Плюс/минус синтаксис.

Вывод типов в Haskell хорош, а вот сообщения об ошибках реально близки к «где-то в программе есть ошибка». Да, с аннотациями чуть лучше, но только если функции очень маленькие.

Плюс система типов, заставляющая половину код посвящать преобразованиям типов. Например, есть у меня список целых или вещественных и функция, которая принимает на вход список целых, вещественных или строк. Так мне придётся взывать её как «f . map Left».

Я всего лишь пытаюсь донести до тебя, что если задача

Не пытайся, пожалуйста. Для этого нужно уметь в оба языка, то, что ты абсолютно не умеешь в Haskell ты доказал, у меня ещё возникают сомнения по поводу racket, но т.к. у меня нету квалификации, чтобы судить об этом я не могу это утверждать.

Давай ты не будешь мне рассказывать как и что работает в Haskell, т.к. опыта программирования на нем у тебя нет?

Я всего лишь пытаюсь донести до тебя, что если задача «сделать язык с выводом типов», то получится Haskell

Хаскел - игрушка академиков. Просто по определению отнюдь не все решения, принятые в ней, окажутся удачными.

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

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

Академики идут туда работать и приносят с собой любимые игрушки. Внезапно, да? %)

P.S. Почему ты так плохо относишься к академикам? Я вот не имею ничего ни против них, ни против их игрушек.

Я хорошо к ним отношусь, в общем то я сейчас в академической среде :) и к этим игрушками хорошо отношусь, я ими на жизнь зарабатываю :)

Ради интереса, а ты диссер Sam Tobin-Hochstadt читал?

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

все это есть в статьях и документации.

Ну, например, чтобы рассказывать почему в ракетке есть local type inference и нету module level, не противореча истокам. И понимая почему sub-tuping важен, и что изменяется если его нет (хотя это я наверное слишком много хочу?)

диссер Sam Tobin-Hochstadt читал

Нет. Спасибо, читаю. Кстати, там как раз про то, что я и анонимус пытались объяснить: «The contract system also ensures appropriate blame for higher-order values». Вот этого-то «appropriate blame» в Haskell и не хватает. Хотя, может быть, вопрос привычки. В Common Lisp тоже ругается на что ни попадя, зато стек выдаёт (потому как рантайм).

И понимая почему sub-tuping важен, и что изменяется если его нет

А чего бы почитать, чтобы понять, почему в Haskell его нет?

К сожалению, не скажу, я пирса до конца не осилил, а т.к. в хацкеле его нету, то с со стороны Haskell статей не читал. Если бы quasimodo кто кастанул - было бы интересно.

рассказывать почему в ракетке есть local type inference и нету module level

не совсем понял.

почему sub-tuping важен

потому что

 (U A B) :> A 

на этом построен occurency typing

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

Кстати хорошая цитата: «Second, type inference is well-known to cause hard-to-decipher type errors with non-local behavior. Third, experience with systems that performed complete type inference for untyped Scheme code suggested that such systems are extremely brittle, with minor code changes radically changing the inference results»

Собственно, к Haskell всё это тоже относится.

Да нифига (про третье) глобальный вывод типов не может вывести тип больший, чем локальный: (localType >= signature >= inferred type), что я так понимаю не справедливо в случае ракетки.

Пример:

n = 5

Вывод типов на основе определения скажет :: Num a => a любая функция которая хочет использовать этот код (в предположении, что он написан правильно) должен уметь работать именно с таким типом. Теперь рассмотрим сингатуру от пользователя (он переписывает спеку из головы в понятный компилятору вид): если она не совместима , напр :: String, то будет ошибка типизации, если совместима, напр. :: Rational a => a, то контракт проверится и будет взят более узкий (юзерский). Тип все ещё не выведен, TI может только уточнить этот тип, напр. до Floating a => a, или конкретного Double. Важно, что последнеетуточнение будет только по месту использования, а на тип функции не влияет.

Разницы с ракеткой тут две: 1. Ракетка требует сигнатуру для топ-левел значений (хотя в ML предлагали это изменить где-то) 2. Третья часть (уточнение типа через то как он используется - отсутвует), есть подозрение что из-за эффектов при subtyping.

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

n = 5
Вывод типов на основе определения скажет :: Num a => a

Prelude> let n = 5
n :: Integer

А иногда вообще глючит:

data T = MyInt Int | MyFloat Float | MyString String

foo :: T -> ((a -> String) -> a -> String) -> String
foo (MyInt x) printerf = printerf show x
foo (MyFloat x) printerf = printerf show x
foo (MyString x) printerf = printerf (\x -> x) x

Test.hs:52:42:
    Couldn't match type `Int' with `Float'
    Expected type: a
      Actual type: Float
    In the second argument of `printerf', namely `x'
    In the expression: printerf show x
    In an equation for `foo':
        foo (MyFloat x) printerf = printerf show x

Test.hs:53:45:
    Couldn't match type `Int' with `[Char]'
    Expected type: String
      Actual type: a
    In the expression: x
    In the first argument of `printerf', namely `(\ x -> x)'
    In the expression: printerf (\ x -> x) x

Зачем он его пытается привести к Int, если указано a ?

Причём по отдельности

foo (MyInt x) = printerf show x
foo (MyFloat x) = printerf show x
foo (MyString x) = printerf (\x -> x) x

printerf f x = (f x)

всё работает. А в виде параметра ни в какую.

может надо monomorphism restriction вырубить?

Я уже устал считать сколько раз я писал про defaulting rules в ghci. В современных ghc (или в старых с NoMonomorphismRetriction) все ок, иначе используется дефолтный инстанс, который для Num - Integer, нужно чтобы показать пользователю интерпретатора хоть что-то - отсутствует в скомпиленых программах.

Читай выше чем отличается a от Any, компилятор не глючит.

Как программист, естественно.

Можно ознакомиться со списком твоих трудов? И трудов, не подверженных соглашению о неразглашении?

Конечно, попробуй -Wall и посмотри какой тип тебе выведется :)

Он вроде только когда типы явно не указаны. «The monomorphism restriction is a rule that affects the automatic inference of the type of an expression when no explicit type signature is provided.»

Test.hs:8:1: Warning:
    Top-level binding with no type signature: foo :: T -> String

Test.hs:10:31: Warning:
    This binding for `x' shadows the existing binding
      bound at Test.hs:10:15

Test.hs:12:1: Warning:
    Top-level binding with no type signature:
      printerf :: forall t t1. (t1 -> t) -> t1 -> t

Если сделать printerf f x = «Ok: » ++ (f x), тогда вообще как в моём типе:

printerf :: forall t. (t -> [Char]) -> t -> [Char]

Читай выше чем отличается a от Any, компилятор не глючит.

Так я не хочу, чтобы он произволбное значение туда передавал. Я хочу, чтобы он принимал функцию с типом ((a -> String) -> a -> String), например \f s -> «Ok: » ++ (f s)

я понимаю, что ты хочешь передать туда (forall a . (a -> String) -> a -> String), но пока ты этого не понимаешь, а требуешь полипорфную фукнцию в которую подставится конерктный 'a', причем, из первого кейса следует что a ~ Int, а из второго, что a ~ Float, компилятор удивляется твоей находчивости и рапортует ошибку, правильно делает, кстати.

sorry if too offencive, то я уже много часов в этой теме потерял/

{-# LANGUAGE RankNTypes #-}
data T = TI Int
       | TF Float
       | TS String

foo :: T -> (forall a . (a -> String) -> a -> String) -> String
foo (TI x) printerf = printerf show x
foo (TF x) printerf = printerf show x
foo (TS x) printerf = printerf id x

можешь не благорадить. Вот это то, что ты хотел сделать.

*Main> foo (TI 1) ($)
"1"
*Main> foo (TF 0.5) ($)
"0.5"
*Main> foo (TS "yo!") ($)
"yo!"

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

Вот это то, что ты хотел сделать.

Работает. Но Type Inference'ом такой тип угадать не может.

*Main> let x = 5

Эту часть я понял. В GHC тип зависит от версии и ключей компиляции. Как раз та самая третья причина, почему нежелательно делать тотальный вывод типов и на него полагаться. В новой версии компилятора тип может стать другой :-)

rankNtypes угадывать это очень сильно.. я бы не отказался, если бы кто осилил, но боюсь там есть не обходящиеся сложности.

Насколько я знаю rank2types ещё выводится, а это уже нет.

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

http://www.podval.org/~sds/ocaml-sucks.html#no-poly

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

Я правда не авторитет в таких вопросах, но все же.

Сложить Float и Int это не полиморфизм это неявное приведение типов, и однозначного ответа на то хорошо ли это нету. По мне так неявное преоьразование типов это плохо. Выше ты приводил пример с двумя массивами, так вот там преобразования типов не было, т.к. в ghc когда ты пишешь цифирь, то она преобразуется в какой-то тип, являющийся Num (реализующий frominteger), так же с расширением OverloadedStrings строка приводится к типу являющемумя IsString, и OverloadedLists - IsList. Сделано это для удобства программиста, если тип не выводится из контекста, то программиста просят явно его указать (исключение ghci). Говорить что в том примере проблема с синтаксисом? Ну.. Не уверен что стоит.

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

Сложить Float и Int это не полиморфизм это неявное приведение типов

Там имелось в виду, что было бы хорошо иметь с одним именем несколько функций, которые подбирались бы в зависимости от параметра. То есть + :: Int -> Int -> Int = ...; x :: Int -> Float -> Float = ...

Вот только с ML-подобным TI такой подход несовместим совсем. Так как не «даны типы, получаем функцию», а «дана функция, подгоняем типы».

Про Scheme подумал. Там как раз ситуация такого типа. Можно в функции расширить тип параметра (был Int, Стал (U Int Real String). И при этом внезапно меняются типы у всех функций, которые используют данную.

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

Там имелось в виду, что было бы хорошо иметь с одним именем несколько функций, которые подбирались бы в зависимости от параметра. То есть + :: Int -> Int -> Int = ...; x :: Int -> Float -> Float = ...

Ясно, в хацкеле для классы типов служат для этого:

class Num a where (+) :: a -> a -> a

Естественно сложить float с Int не удастся, но однинаковые - вполне.

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

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

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

Была функция вывода out. Имела тип OutFile -> String -> OutFile.

Потом программист А решил разрешить выводить также числа (чтобы формат был тот, который нужен в файле, а не тот, который в show).

Тип стал OutFile -> Either String Number -> OutFile.

И была функция process = map out, давно написанная совсем другим программистом Б. Есть документированное API, есть тесты.

А программист В использует функцию process в своём проекте и удивлён, что теперь ей надо передавать параметром [Either String Number], хотя модуль программиста Б не менялся и вообще он в отпуске. Приходится программисту В лезть в исходники чужого модуля и искать от каких модулей зависит process.

Цепочка может быть длинней.

А в случае Scheme всё ещё менее заметно, так как тип-объединение не требует конструктора. А если кто-то воткнёт обработку ошибок в стиле (if (number? x) ... (error 'not-number)), так x вообще становится Any. Фатальных последствий меньше, но тип может внезапно меняться чаще.

Естественно сложить float с Int не удастся

Если бы было

class Num' a, Num' b where (+) :: a -> b -> a

было бы можно. Наверное.