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

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

Я делал проще.

(module constants racket/base
  (provide (all-defined-out))
  (define const1 123)
  (define const2 "ok"))
(require 'constants)

Для типизированного замени racket/base на typed/racket/base.

Ну что я могу сказать? Дно!

Prelude> :t id
id :: a -> a
Prelude> :t map
map :: (a -> b) -> [a] -> [b]
Prelude> map id [1, 2, 3]
[1,2,3]
Prelude>

`map id :: [a] -> [a]`, данный тип будет выведен или из типа который передан в функцию [1,2,3::Int], напр, или выведен если известно где данная функция использована, т.е. через результирующий тип.

что было раньше (с monomorphism restriction): map id [1,2,3] это Num a => [a] -> [a], что не хватает для вывода. В этом случае в ghci срабатывает default typing rules, для целых это будет Integer, он и подставится.

что сейчас, без monomorphism restriction:

Prelude> :t map id [1,2,3]
map id [1,2,3] :: Num b => [b]
Prelude> map id [1,2,3]
Prelude> :t it
it :: Num b => [b]

Для типизированного замени racket/base на typed/racket/base.

const1: undefined; cannot reference an identifier before its definition

const1: undefined; cannot reference an identifier before its definition

Покажи весь буфер. Или (provide (all-defined-out)) или (require 'constants) пропущено.

map :: (a -> b) -> [a] ->

С таким map и в Racket работает:

#lang typed/racket

(: id : (All (A) A -> A))
(define (id x) x)

(: mymap (All (A) (A -> A) (Listof A) -> (Listof A)))
(define (mymap f x) (map f x))

> (mymap id '(1 2 3))
- : (Listof Positive-Byte)
'(1 2 3)

Я про описание типов наподобие

> map
- : (All (c a b ...)
      (case->
       (-> (-> a c) (Pairof a (Listof a)) (Pairof c (Listof c)))
       (-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c))))
#<procedure:map>

(: mymap (All (A) (A -> A) (Listof A) -> (Listof A)))
(define (mymap f x) (map f x))

Почему A -> A ? Мне нужно A -> B!

(: mymap (All (A B) (A -> B) (Listof A) -> (Listof B)))
(define (mymap f x) (map f x))

> (mymap id '(1 2 3))
. Type Checker: Polymorphic function `mymap' could not be applied to arguments:
Argument 1:
  Expected: (-> A B)
  Given:    (All (A) (-> A A))
Argument 2:
  Expected: (Listof A)
  Given:    (List One Positive-Byte Positive-Byte)
 in: (mymap id (quote (1 2 3)))

const1: undefined

Увидел. all-defined-out в Typed Racket как-то не так работает. Если (provide const1 const2), то работает...

http://docs.racket-lang.org/ts-guide/caveats.html#(part._.Type_inference_for_...

Если (provide const1 const2), то работает

Всё равно не работает. Внутренний модуль не подключается. Если во внешнем файле - без проблем, но (module ...) не работает.

Вот так работает:

#lang typed/racket

(define-syntax-rule (const id val)
  (define-syntax id 
    (syntax-id-rules ()
      (id val))))

(const const1 123)
(const const2 "ok")

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

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

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

Так у тебя там может быть любой надтип (U One Two Three), откуда чекер должен узнать, какой из этих надтипов тебе нужен?

откуда чекер должен узнать, какой из этих надтипов тебе нужен

Для (: mymap (All (A) (A -> A) (Listof A) -> (Listof A))) почему-то выводит. Хотя на практике для таких ситуаций всё равно лучше всегда тип указывать. Также, как и тип функций. Его Racket тоже выводить «не может» (а если точнее, то было принято решение, что для функции вывод типа вреден и приводит к ошибкам).

Для (: mymap (All (A) (A -> A) (Listof A) -> (Listof A))) почему-то выводит.

Потому что он знает тип аргумента, но не знает тип результата. Смысл в том что ограничение в Id (A -> A) не ведет к тому, что в инстансе map будет A = B:

((inst mymap Byte Integer) (inst id Byte) '(1 2 3))

Нормально чекается. На месте Integer может быть любой надтип Byte. Если же у тебя в mymap A->A вместо A->B, то тип аргумента фиксирует тип результата, то етсь А выводится из аргумента и все (просто будет взят наиболее узкий тип).

Смысл в том что ограничение в Id (A -> A) не ведет к тому, что в инстансе map будет A = B:

Упс. Да, затупил. А в haskell'е, по-моему, ведет.

было принято решение, что для функции вывод типа вреден и приводит к ошибкам

Пример

$ cat Test.hs
module Test
    where
    strlen x = length

опечатались, забыли в конце написать x.

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

Ошибок нет.

$ cat Main.hs 
import Test

main = do
  putStrLn "Please enter a word"
  num <- getLine
  let size = strlen num
  putStrLn $ "The size of your string is: " ++ show size ++ "!"

$ ghc Main.hs 
[2 of 2] Compiling Main             ( Main.hs, Main.o )

Main.hs:7:48:
    No instance for (Show ([a0] -> Int)) arising from a use of `show'
    Possible fix: add an instance declaration for (Show ([a0] -> Int))
    In the first argument of `(++)', namely `show size'
    In the second argument of `(++)', namely `show size ++ "!"'
    In the second argument of `($)', namely
      `"The size of your string is: " ++ show size ++ "!"'

Очень внезапная ошибка. Тут и show и ++ и $. Всё, кроме strlen.

А в haskell'е, по-моему, ведет.

Да, в хаскеле нету подтипирования.

Ну да. Смысл в том, что вывести тип в map можно принипиально из двух мест - либо из типа id, либо на основе возвращаемого типа (из синтаксического контекста то есть). Из id вывести не получается потому что подтипирование, а из контекста не выводят идеологически - чтобы не было описанных вещей. То есть предполагается что программист фиксирует тип в контексте + в самом выражении, в результате чего чекер именно проверяет соответствие типов, а не пытается их подобрать в достаточно свободных границах (в результате чего может быть сильная бяка). Ну это примерно как ф-я с контрактом вс ф-я без контрактов - с контрактами мы увидим ошибку там где она возникла, без контрактов - хз где дальше по control-flow. Т.о. контракт создает некоторую «границу», которую ошибка не может пересечь - вот и в выводе типов тут неучет возвращаемого значения при выводе создает такую же «границу», котоаря не позволяет ошибке типов «улететь» хз куда дальше по control-flow вывода.

Тут идейно разный подход. Некоторые пользователи пишут то, что действительно знаю, а некоторые придумывают всякую чушь на ходу.

То, что ты написал, является ложью.

То, что ты написал, является ложью.

Вон monk выше привел доказательство моих слов. Любой может проверить и убедиться. Так что врешь тут ты.

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

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

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

Зачем бегать и собирать? Комментарий монка был пятью постами выше, там весь код, все просто и понятно.

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

От анонима я могу попросить код хотя бы проходящий -Wall -Werror. Тот код не проходит.

Зато много какой другой спокойно проходит. Проблема заключается в том, что тайпинференс в хаскеле использует информацию из синтаксического контекста. В результате ошибка вдоль этого контекста бежит бежит и когда наконец случится - то выблев чекера будет совершенно невнятен. Чтобы выблев чекера был внятен - надо делать больше аннотаций. Но сам хаскель этих аннотаций не требует - и их ленятся писать. А Typed Racket их строго требует.

А далее можно будет поговорить почему это не проблема

Нет, это очень большая проблема.

и насколько все было бы хуже если бы было поведение как в лиспе

В лиспе тебе тайпчекер просто не даст написать подобный код.

(где из-за подтипирования такое поведение осмысленно)

Это в хаскеле оно осмысленно и допускается чекером. Ракетка как раз потребует у тебя аннотаций.

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

Для чего «для этого»?

Внутренний модуль не подключается.

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

опечатались, забыли в конце написать x.

Проиграл всем классом. Ошибка четко говорит, что нельзя функцию напечатать, в чем проблема?

Зато много какой другой спокойно проходит.

пример.

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

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

Нет, это очень большая проблема.

нет, это не проблема. monk написал функцию с типом forall a, b . a -> b -> String это вполне валидная и нормальная функция и если бы тайпчеккер не дал её написать, вот это была бы проблема, причем очеть большая. Так, что ничего общего с выводом из контекста указанная проблема не имеет.

В лиспе тебе тайпчекер просто не даст написать подобный код.

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

Это в хаскеле оно осмысленно и допускается чекером. Ракетка как раз потребует у тебя аннотаций.

Да в хацкеле осмысленное - верное поведение.

Для чего «для этого»?

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

monk второй абзац тоже прочитай, полезно будет :)

ошибка в том, что тайпчеккер не дал написать функцию с типом :: forall a, b . (Show b) => a -> b -> String

наверное foo = const show тоже написать нельзя должно быть.

пример.

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

это не проблема

Это проблема, лол.

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

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

нет, это не проблема. monk написал функцию с типом forall a, b . a -> b -> String это вполне валидная и нормальная функция и если бы тайпчеккер не дал её написать, вот это была бы проблема, причем очеть большая.

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

возможно в typed racket очень плохой тайпчеккер

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

То есть есть два варианта действий тайпчекера - он при виде неопределенности либо требует программиста неопределенность устрнатиь (как в ракетке) либо думает «если предположить что ф-я возвращает жирафов, то, вроде, все ок, по-этому пусть она будет возвращать жирафов».

Да в хацкеле осмысленное - верное поведение.

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

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

А чего тут создавать, если оно в каждом втором проекте на хаскеле сплошь и рядом? Это одна из основных проблем хаскеля, которая известна сообществу и с которой сообщество пытается бороться, кстати. Только методы не те.

ошибка в том, что тайпчеккер не дал написать функцию с типом :: forall a, b . (Show b) => a -> b -> String

Ошибка тут в том, что тайпчекер решил, что у strlen тип a -> String -> Int, хотя он у нее String -> Int.

Ошибка четко говорит, что нельзя функцию напечатать, в чем проблема?

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

Нет, он у неё a -> String -> Int. Если ты хочешь продолжать упорствовать, то я препочту прекратить участие в этой ветке дискуссии в виду её бесполезности.

Пример, подобной ошибки тайпчеккера:

УмножитьНаДва x = show x

Тайпчеккер будет выводить Show a=> a -> Int, вместо Int -> Int, что показывает его убогость.

Нет, он у неё a -> String -> Int.

Лолчто? Откуда у тебя взялся a? Функция принимает строку и возвращает ее длину. Где там второй аргумент ты увидел?

От анонима я могу попросить код хотя бы проходящий -Wall -Werror. Тот код не проходит.

Проходит:

$ ghc -Wall -Werror Test.hs
$ ghc -Wall -Werror Main.hs
[2 of 2] Compiling Main             ( Main.hs, Main.o )

Main.hs:7:48:
    No instance for (Show ([a0] -> Int)) arising from a use of `show'
    Possible fix: add an instance declaration for (Show ([a0] -> Int))
    In the first argument of `(++)', namely `show size'
    In the second argument of `(++)', namely `show size ++ "!"'
    In the second argument of `($)', namely
      `"The size of your string is: " ++ show size ++ "!"'

В смысле, на Test не ругается (хотя там ошибка). В Main ругается н всё что угодно кроме strlen (в котором ошибка).

Если я правильно понял, но это всё-таки ограничение типизированного диалекта. Там не поддерживаются несколько модулей в одном файле

Да. Именно так.

Проиграл всем классом. Ошибка четко говорит, что нельзя функцию напечатать, в чем проблема?

В том, что в C++ и даже в Common Lisp (который весь из себя динамический) я получу предупреждение, что strlen получает праметр и не использует его. А супер-типизированный Haskell считает код strlen абсолютно корректным и ошибку выдаёт совсем про другое (рекомендует сделать для Show ещё один instance).

у нечитаемых ошибок обычно другие источники

Обычно — может быть.

В моём примере ошибку позволяет сделать исключительно тайпчекер. Кстати, тип вроде [a] -> -> Int получился вместо [a] -> Int.

Нет, он у неё a -> String -> Int.

По мнению компилятора — да. Но в этом и ошибка. Которую нигде не видно (или можно как-то отчёт по компиляции получить — какие объекты с какими типами сформировались?).

То есть есть два варианта действий тайпчекера - он при виде неопределенности либо требует программиста неопределенность устрнатиь (как в ракетке) либо думает «если предположить что ф-я возвращает жирафов, то, вроде, все ок, по-этому пусть она будет возвращать жирафов».

Маленькое уточнение. В Haskell нет неопределённости, так как каждый объект имеет ровно один тип. Но суть системы типов в Haskell и Typed Racket действительно противоположная.

Typed Racket: укажите ожидаемые типы, проверим, соответствует ли код функции заявленному. Работает как контракты, но с проверкой при компиляции.

Haskell: по коду функции угадаем тип входящих параметров и результата. Помогает компилятору оптимизировать код, но при неверном угадывании запутывает программиста. Как в моём примере: Possible fix: add an instance declaration for (Show ([a0] -> Int)).

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

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

qnikst@localhost ~/tmp/haskell $ ghc -Wall -Werror 123.hs 
[1 of 1] Compiling Test             ( 123.hs, 123.o )

123.hs:3:9: Warning:
    Top-level binding with no type signature:
      strlen :: forall t a. t -> [a] -> Int

123.hs:3:16: Warning: Defined but not used: ‘x’

<no location info>: 
Failing due to -Werror.

В смысле, на Test не ругается (хотя там ошибка).

В модуле Test нету ошибок, там есть одна причина для Warning-а

В моём примере ошибку позволяет сделать исключительно тайпчекер.

В твоём случае typechecker позволяет написать валидную функцию, я не вижу ни одной причины, почему ты считаешь это ошибкой, вот ниже код

mystrlen x = length

main = do
  x <- getLine
  putStrLn $ "length of my line is: " ++ show (mystrlen "debug" x)

По твоему он не должен собираться, есть хоть одна причина почему?

По мнению компилятора — да.

по мнению моему мнению тоже, в общем-то так же как и по мнению любого другого человека не имеющего ложных представлений о haskell :)

Которую нигде не видно (или можно как-то отчёт по компиляции получить — какие объекты с какими типами сформировались?).

а). В данном случае типы можно и самому вывести, б). кинется warning (в случае toplevel) в). есть data holes выводящее тип дыры при сборке, г). в любых devtools есть возможность вывести тип и на этапе создания кода, д). можно дать stub вместо сингатуры и увидеть, во что сигнатура должа была вывестить

слушай, давай ты не будешь рассказывать как в haskell работает typechecker.. у меня, например, отпадает желание как-либо комментировать такой «анализ».

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

В твоём примере: ты написал функцию с типом t -> String -> Int, ты её частично применил, и получил [a] -> Int. Ты применил к этому show :: Show a => a -> String , компилятор проверяет данный констрейнт и очевидным образом он видит, что у типа [a] -> Int нету инстанса Show, о чем он тебе и написал. Ты видишь, что в call site у тебя функция с типом [a0] -> Int, можешь начинать думать почему :) в силу чистоты и referece transparancy это сделать сравнительно просто.

В модуле Test нету ошибок,

А тот факт, что функция strlen работает неправильно - это что? Или ты что-то иное подразумеваешь под «ошибкой», не то, все нормальные люди?

В твоём случае typechecker позволяет написать валидную функцию, я не вижу ни одной причины, почему ты считаешь это ошибкой

Ошибка в том, что ф-я не соответствует свой спецификация. Функция должна считать длину переданной ей строки. Она этого не делает. Что тут неясного-то?

по мнению моему мнению тоже, в общем-то так же как и по мнению любого другого человека не имеющего ложных представлений о haskell :)

При чем тут хаскель? Тип функции определяется спецификацией ф-и, а не тем, при помощи какого кода она реализована, какая семантика у ЯП и т.д.

Ошибка в том, что ф-я не соответствует свой спецификация.

в том модули нет спецификации функции, нечему соответствовать.

Соответствует ли спецификации функция? как typed racket решает эту проблему и ловит ошибку?

умножитьНаДва x = x + 1

Пожалуйста, прекращай уже дурить, мне надоело.