LINUX.ORG.RU

Зависимые типы, жидкие типы. Что лучше?

 , liquid haskell,


1

4

Пытаюсь понять тенденции в современных статических языках. Обычного Haskell явно не хватает. Что ожидать на замену?

★★★★★

Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от alienclaster

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

Я вот читаю твой комментарий и мне кажется, что ты просто тупой. Не знаю, почему так.

И нахрен мне это надо, чтобы уловить класс ошибок размером в 0,2%?

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

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

Я вот читаю твой комментарий и мне кажется, что ты просто тупой. Не знаю, почему так.

А я знаю, потому что тупой - ты :) Ты ведь ни разу не ответил по делу, я понимаю, что вы там развели какого-то лоха на хаскель в вебе с помощью тех базвордов что ты пытаешься здесь втереть, если бы ты честно так и сказал - что это игрушка в которую нам дали поиграть вопрос к тебе бы не было.

Доступность привелигированных API только для аутентифицированных юзеров отлично кодируется в типах хачкелля.

Чем сложно реализовать это в динамике? И чем такое решение будет хуже?

Не уверен, что это прямо 0.2%. Но тебе лучше знать, чувак.

100%.

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

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

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

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

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

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

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

Это не история, это факт.

Это чушь. Но про статическую vs динамическую типизацию не интересно, это обсуждалось много раз. И по итогу - статическая почти никогда не нужна.

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

Это более верно чем то что написано перед тобой.

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

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

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

Это чушь. Но про статическую vs динамическую типизацию не интересно, это обсуждалось много раз. И по итогу - статическая почти никогда не нужна.

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

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

как много новых языков имеют динамическую типизацию

Julia, Hack, Scala. Приобрёл динамическую типизацию C#, добавлен std::any в С++ и Dynamic в Haskell.

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

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

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

void* хватило бы всем и для всего

Там у значения типа нет. То не динамическая, то слабая.

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

Там не было обоснованных аргументов, или «на хаскеле можно нанять макак за борщ и все будет надежно» это и есть самый сильный и адекватный аргумент?

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

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

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

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

То не динамическая, то слабая

ескобар.jpg

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

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

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

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

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

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

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

Точно так. Конечно, хотелось бы, чтобы кухарка могла успешно делать операции на мозге (за зарплату кухарки, разумеется), но вряд ли это хорошо кончится — какой бы крутой наноскальпель мы ей ни вручили.

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

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

Он не помешает перепутать «+» и «-», «<» и «>», ленивое выполнение заставит падать с ошибкой деления на ноль не в операции деления, а в команде putStrLn a, а принципиальное отсутствие пошагового отладчика значительно затруднит поиски ошибки.

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

Видимо мне придется теперь до момента протухания этого треда цитировать себя Зависимые типы, жидкие типы. Что лучше? (комментарий)

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

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

Я как раз на Haskell писал. И когда получил на строчке writeFile outFile . unlines . reverse . result ошибку разбора регулярного выражения был озадачен, а как теперь искать, откуда она взялась.

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

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

Там проще уронить, но и проще поднять. Есть отладчики, есть стектрейс.

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

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

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

A тут что сложного? разбей на части посмотри что происходит, что уж проще может быть.

Как посмотреть? Он же не пишет из какой функции прилетел error.

Как поделить на части? Точек останова в языке не предусмотрено.

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

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

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

Как посмотреть? Он же не пишет из какой функции прилетел error.

вообще-то пишет

Как поделить на части? Точек останова в языке не предусмотрено.

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

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

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

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

вообще-то пишет

Prelude> let f x y  = (x+y) `div` (x-y)
Prelude> let g x  = x - 5
Prelude> let k x = f (g x) 10
Prelude> let s = map k [1..20]
Prelude> sum s
*** Exception: divide by zero

И как увидеть, в какой функции ошибка? В sum точно никакого деления нет, там только суммирование.

декомпозировать код разбив выражение на части

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

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

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

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

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

И как увидеть, в какой функции ошибка? В sum точно никакого деления нет, там только суммирование.

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

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

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

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

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

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

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

И как увидеть, в какой функции ошибка? В sum точно никакого деления нет, там только суммирование.

Собрать код с инструментированием и запускать с нужными флажками RTS:

> cat callstack.hs                       
f x y  = (x+y) `div` (x-y)
g x  = x - 5
k x = f (g x) 10
s = map k [1..20]
main = print $ sum s

> ghc -prof -fprof-auto ./callstack.hs -o ./callstack
[1 of 1] Compiling Main             ( callstack.hs, callstack.o )
Linking ./callstack ...

> ./callstack +RTS -xc
*** Exception (reporting due to +RTS -xc): (THUNK_STATIC), stack trace: 
  GHC.Real.CAF
  --> evaluated by: Main.f,
  called from Main.k,
  called from Main.s,
  called from Main.CAF
  --> evaluated by: Main.main,
  called from Main.CAF
callstack: divide by zero

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

> cat hascallstack.hs
import GHC.Stack (HasCallStack)

f :: HasCallStack => Int -> Int -> Int
f x y  =
  if x == y
  then error "divide by zero"
  else (x+y) `div` (x-y)

g :: HasCallStack => Int -> Int
g x  = x - 5

k :: HasCallStack => Int -> Int
k x = f (g x) 10

s :: HasCallStack => [Int]
s = map k [1..20]

main = print $ sum s

> ghc ./hascallstack.hs -o ./hascallstack
[1 of 1] Compiling Main             ( hascallstack.hs, hascallstack.o )
Linking ./hascallstack ...

> ./hascallstack 
hascallstack: divide by zero
CallStack (from HasCallStack):
  error, called at hascallstack.hs:6:8 in main:Main
  f, called at hascallstack.hs:13:7 in main:Main
  k, called at hascallstack.hs:16:9 in main:Main
  s, called at hascallstack.hs:18:20 in main:Main
Laz ★★★★★
()
Ответ на: комментарий от anonymous

на действительно слабые места haskell, а именно на его систему модульности и как следствие этой системы на его проблемы с неповоротливой долгой сборкой, на инструменты сборки как таковые

Для моих целей хватало. Но фоне C++ он ещё быстрый.

вынужденных блистательно вытанцовывать на цыпочках вокруг таких задач ​чтобы не скатиться в какую-нибудь непролазную императивоподобную лапшу

Как будто это что-то плохое. И в XMonad и в Movie-Monad 95% кода в монаде IO. И так почти в любой прикладной программе.

если вы писали на хаскеле вы знаете, что там никто простынями не пишет

https://github.com/xmonad/xmonad/blob/master/src/XMonad/Core.hs#L565 – это не простыня?

Или https://github.com/hedgewars/hw/blob/master/gameServer/HWProtoLobbyState.hs#L73 ?

Если не простыня, то простынями на всех языках почти никто не пишет.

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

called from Main.k,

Строчку и имя файла угадывайте сами…

Ну да «никто простынями не пишет».

s :: HasCallStack => [Int]

Здесь лучше. Осталось прикрутить макросы, чтобы это по -debug автоматически на все функции прикручивалось. Правда он и так не слишком быстро пересобирвается.

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

95% кода в монаде IO

да ты упорот. там даже main это IO() и что не писать на хаскеле теперь? зачем кстати ты на нём пишешь? ты же скобочкофил, вот и пиши на лишпах, не?

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

да ты упорот. там даже main это IO() и что не писать на хаскеле теперь?

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

По мне IO не хуже любой другой монады.

А для обсуждаемого «менее квалифицированного персонала» это вообще основной режим записи программы.

зачем кстати ты на нём пишешь?

Чтобы получить красивый текст прграммы.

ты же скобочкофил, вот и пиши на лишпах, не?

Это что за сцена ревности?

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

Для моих целей хватало. Но фоне C++ он ещё быстрый.

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

Как будто это что-то плохое.

в общем-то ничего, просто чувство прекрасного истончается день ото дня.

Если не простыня, то простынями на всех языках почти никто не пишет.

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

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

Потерялся в двух анонимах? )

Похоже, да. Или не двух. Вы хоть нумеруйтесь, что ли…

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

Мы будем подписываться Владимир, чтобы нас можно было различать ;)

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

Чтобы получить красивый текст прграммы.

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

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

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

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

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

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

Не обязательно. Чтобы наслаждаться музыкой Баха не обязательно быть композитором.

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

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

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

Это ты

это не я.

красивый текст прграммы.

на пистоне ещё красивше же, ну. и динамическая типизация же.

Это что за сцена ревности?

ты мне в последний раз заливал о том, что нельзя все failure обработать в одном месте, нужно failure01 failure02 и т.д. изобретать, в стат типизации, и что ракет могёт и дин и стат если надо. а теперь вдруг вопрос по хаскелю. неужели я тебя переубедил? ;)

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

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

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

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

на пистоне ещё красивше же, ну. и динамическая типизация же.

Ну как на питоне напишешь

    readFile templateFile
        >>= foldM (processLine processTemplate) context . lines
        >>= writeFile outFile . unlines . reverse . result

Так красиво не получится.

нельзя все failure обработать в одном месте, нужно failure01 failure02 и т.д. изобретать

Типизация ограниченная. failure я свожу просто к строкам.

getResult :: IO (Either String ())
getResult = runExceptT $ do ...

неужели я тебя переубедил

Нет. На Haskell я давно пишу утилитки по мелочи. Ему бы ещё переносимый GUI…

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

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

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

С ленивостью и классами типов на Racket есть Hackett. Но это реально отдельный язык почти без интеграции с Racket. А тогда проще взять Haskell и получить более быстрый результат компиляции.

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

я понимаю, что вы там развели какого-то лоха на хаскель в вебе с помощью тех базвордов что ты пытаешься здесь втереть

А ты никак не можешь найти лоха, которого можно было бы развести на лисп, вот и бесишься?

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

Так красиво не получится.

а (на (ракете)) (красиво получается) ?

failure я свожу просто к строкам.

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

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

а (на (ракете)) (красиво получается) ?

Я же пишу: не настолько красиво как на хаскеле. Строчек в полтора раза больше, интерфейсы многословнее. Зато есть call/cc и контракты.

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

Если работает, то какая разница.

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

добавлен std::any в С++

Дык, ты же сам говорил, что это не может считаться динамической типизацией, если any_cast не будет автоматически выполняться. Да и если на то пошло, то void* в языке было изначально, так что std::any - это скорее ужесточение типизации.

Hack

Это ведь такая себе замена PHP, которая позволяет местами статическую типизацию использовать, разве нет? Kак и тайпскрипт я бы скорее записывал тут «победу статики».

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

Дык, ты же сам говорил, что это не может

Не может. Но подвижка в ту сторону. Также как тайпхинты в питоне - подвижка в сторону статической типизации.

Да и если на то пошло, то void* в языке было изначально

То не динамическая, то бестиповая. Внутри void* тип не хранится.

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

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

кажется ты начал догадываться.

Зато есть call/cc

этим можно гордиться?

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

я понимаю, что вы там развели какого-то лоха на хаскель в вебе с помощью тех базвордов что ты пытаешься здесь втереть

А ты никак не можешь найти лоха, которого можно было бы развести на лисп, вот и бесишься?

В этом треде я надеялся услышать хоть какой-то конструктив от хаскель-фанбоев (хаскель как язык в некоторых нишах весьма выразительный - для написания «факториалов», например - т.е. программ, которые можно свести к одноразовому получению данных вписывающихся в заранее известный алгоритм, соответственно для микросервисной архитектуры, построенной на стабильном API и чистых функциях он тоже подходит). Для разбора грамматик, например, я думаю он тоже смотрелся бы нормально, при условии, если писать просто без ухода в дебри. Но в ответ мне начали рассказыть о якобы гарантиях того, что почему-то в вебе (!), где все данные прилетяют неясно откуда и в каком виде, именно хаскель будет гарантировать то, что деньги с моего счета не перейдут на счет хаскелиста. То есть очевидный тупак. А зачем мне кого-то разводить на лисп, если я сам могу выбирать на чем писать?

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

где все данные прилетяют неясно откуда

Так статическая типизация для таких случаев и нужна. Чтобы гарантировать, что не забыл где-то проверить корректность этих самых данных. А не ловить потом SQL инъекции и переполнения стека.

Не обязательно именно Haskell, но он тоже подходит.

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

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

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

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

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

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

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

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

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

В этом треде я надеялся услышать хоть какой-то конструктив от хаскель-фанбоев

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

Я вон писал блокчейн на расте не столько потому, что мне блокчены интересны (хотя поначалу любопытно было), а потому что на расте.

о якобы гарантиях того, что почему-то в вебе (!), где все данные прилетяют неясно откуда

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

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

ты же понимаешь, что это чтиво из разряда зачем нам в С оператор цикла, если есть goto? call/cc на практике весьма сомнителен, универсальность удивительна разве что для любителей метапрога. на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc. но ты серьёзно думаешь, что кто то будет так писать?

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

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

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

Вот есть

f :: DigitString -> SQL

g :: DigitString -> ....
g x y = ... f x ...

checkStringIsDigit :: String -> Maybe DigitString

И никак строку в f или g не передать, не проверив. А с контрактами появляется сильное желание поставить контракт только на вход g (ведь f больше ниоткуда не вызывается, зачем повторно проверку делать?). А потом через полгода кто-то делает вызов f, не проверив строку контрактом…

И даже с проверкой контрактом: в GLib всё проверяет контрактами и программы массово пишут в stderr что-то вроде: https://bugs.launchpad.net/ubuntu/+source/network-manager/+bug/1264364

А пользователи потом пишут программы, чтобы эти сообщения не видеть.

monk ★★★★★
() автор топика
Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от anonymous

но ты серьёзно думаешь, что кто то будет так писать?

Так же как goto нужен, когда разработчик языка забыл реализовать какую-нибудь нужную конструкцию управления типа цикла n+1/2 раз или выхода из нескольких вложенных циклов, так и call/cc нужен, если разработчик языка забыл сделать генераторы, зелёные потоки, корутины или комбинаторы операций.

Причём Scheme даёт удобный способ любую нужную конструкцию с call/cc завернуть в макрос и использовать call/cc в пользовательском коде почти никогда не надо.

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

на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc

???

Покажешь реализацию?

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

Странно, что ты не понимаешь, что хаскель привлекает сторонников максимально строгой типизации.

Динамическая типизация - тоже строгая. А с контрактами - еще даже более строгая, чем система типов хаскеля.

Есть языки строже, но работы на них ещё меньше.

Вопрос вообще не в строгости, а в том, _когда_ происходит проверка типов, и что собственно мы проверяем.

С позиции такого человека, вопрос звучит странно. Какие преимущества у хаскеля в вебе? Такие же, как и везде.

Ничего подобного, у С очевидные преимущества в написании драйверов перед лиспом, у кложи в разработки веба перед ... почти что перед всеми языками, питон простой язык-клей с кучей батареек, С++ для легаси или как С с классами, джава с шарпом для галер, пхп чтобы вордпрес, перл для написания однострочников, дельфи чтобы формочки клепать, 1с бухгалтерия, своя специализация у erlang, vhdl, prolog итд. В чем ниша хаскеля? Как оказалось веб? :)

Они-то может и проходят, но вообще проверять входные данные идея всегда хорошая.

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

И типизация даёт возможность понимать что происходит,

Ничего она не дает без нормальных зависимых типов (которых нет). Контракты это те же зависимые типы только в динамике, и если расположить инструменты по выразительности от меньшей к большей, то наименьшей выразительностью обладают «обычные типы», далее динамическая типизация (более выразительная), затем на одном уровне идут контракты и завтипы. Завтипами проверяем все что есть проверить на момент компайл-тайма, контрактами в рантайме. Но, т.к. нормальных зависимых типов, которыми можно было бы пользоваться не существуют - то остаются контракты, как средство выразительности тех же типов и гарантий. И тормозят контракты по очевидным причинам - точно так же тормозили бы завтипы, если бы нам дали завтипы в условном лиспе с компилятором на борту и надо было бы постоянно все чекать из агрессивной внешней среды (считай все время программу конпелять).

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

Ты этот словарь вначале получил без всяких гарантий - затем проверил контрактами (потому что проверять больше нечем) и когда отдаешь тоже контрактом проверяешь, раз тебе так важно. А вся статика - это только что между этими точками происходит. Т.е. про опечатки и сложение бульдогов с носорогами. Но прикол в том, что опечатки тебе подсветит ide или нормальный язык скажет, что извините в первый раз такое название вижу, вот вам варнинг держите. А енотобегемоты это ошибка _логическая_, чтобы ее сделать надо или вообще не понимать, что происходит в программе, или веществ объесться прям упороться или опечатка или зловред - то есть к вам в команду пробрался шпион от конкурентов и прописал True=False, решается системой контроля версий.

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

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

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

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

на ski комбинаторах тоже можно наваять абсолютно всё, в том числе и твой call/cc

Покажешь реализацию?

А мне call/cc на лямбда-исчислении, пожалуйста, оно читабельнее. А в SKI я сам потом скомпилю.

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

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

Ну так да, только невнимательность и все. А сколько трейдофов у статики? Впрочем, мне казалось мы тут +- схожего мнения по данному вопросу.

checkStringIsDigit :: String -> Maybe DigitString
И никак строку в f или g не передать, не проверив.

Нормальные контракты будут двигаться к тому, чтобы уметь выводить все что можно в статике, а все что нельзя - как обычно. Это и есть перспективное направление развития контрактов. Но если выбирать между _существующими_ системами типов, а не вымышленными, и существующими контрактами - то языки со статической типизацией проигрывают динамике как в выразительности, так и по итогу в гарантиях надежности, покрывая 2%-ный класс ошибок.

По существу примера - в динамике ты напишешь точно такую же ф-цию которая чекает строку на предмет состоит ли она из цифр. Один раз проверишь и дальше будешь ее передавать по цепочке преобразований, и в конце еще раз проверишь, что отдал не мусор. Статика рулит только, если у тебя все строки они уже известны на момент компиляции (то есть ты пишешь хеллоурлд), в реальном же мире 99% данных приходит из вне, как ты их будешь статически чекать на предмет корректности? _Все_ что ты можешь чекнуть в статике это только результат промежуточных преобразований и то далеко не всегда, а в основном только совпадение типов (чтобы *случайно* вместо бегемотов не подставить носорогов). Единственный реальный профит статики - это статический проход по ветвлению на тему не забыл ли ты какую-то ветку учесть / реализовать (и то возможности такой проверки ограничены). Да, это профит. 3%. И 97% боли.

И даже с проверкой контрактом: в GLib всё проверяет контрактами и программы массово пишут в stderr что-то вроде

Отлично, но почему им тут не помогла хваленая статика? Это неправильная, допустим, статика, плохая, но правильная где? :) Тред ведь об этом.

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

В чем ниша хаскеля? Как оказалось веб? :)

Если брать статистически, то всякие преобразователи данных. Pandoc, freearc, … У них код на хаскеле красивее получается.

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

Так статические типы вообще не про проверку данных. Они про проверку функций.

Ничего она не дает без нормальных зависимых типов (которых нет).

В общем случае даёт. Разве что вместо обычного if придётся пользоваться функциями типа

IsNotZero :: Int -> Maybe NotZero Int
IsNotZero 0 = Nothing
IsNotZero x = Just NotZero x

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

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

В Typed Racket тоже зависимые типы: https://docs.racket-lang.org/ts-reference/Experimental_Features.html

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

затем проверил контрактами (потому что проверять больше нечем) и когда отдаешь тоже контрактом проверяешь

Вот про то и речь. Что контрактами что-то проверяешь дважды, а что-то пропускаешь. В статической системе типов (хоть Haskell хоть Typed Racket) просто пропустить проверку не получится: программа не скомпилируется.

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

Или кто-то троллит или Вы общаетесь на разные темы.
Как узнать, что собеседник Вас понимает?
Как узнать, что собеседник понял Вашу конструкцию и её подоплёку?

Или Вам просто скучно?

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

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

Я же привёл пример. Статика не позволит тебе пропустить проверку в начале цепочки. А в динамике либо проверка происходит на входе каждой функции (оборонительное программирование), либо есть вероятность запустить алгоритм не с первого шага, а со второго без проверки. Либо программист начинает мыслить в духе анекдота: «Чтобы заварить чай надо взять пустой чайник, налить в него воду, закипятить, залить воду в заварник, добавить заварку. У вас есть чайник с кипящей водой, как используя его заварить чай? Вылить воду и выполнить заданный алгоритм.».

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

Отлично, но почему им тут не помогла хваленая статика?

Какая статика в GLib/GObject? Там даже типы при выполнении программы создаются.

но правильная где? :) Тред ведь об этом.

Так в заголовке треда ведь.

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

Так они в рантайме проверяются контрактами. Статически мы их где вообще возьмем эти данные?

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

Именно.

В языках со статической типизацией можно с определённой точностью описать это множество валидных данных.

Но контракты, как система валидации данных, явно мощнее. Т.е. как завтипы. Только у каждой системы есть свои преимущества / недостатки. Завтипы все конпеляем на каждый чих доказываем _всю_ программу, зато надежно. Но и страшно, и вообще их по факту нет. Контракты - почти так же надежно как завтипы (исключение - набухался и забыл проверить что-то очень важное), но будут тормозить в рантаймме (тормозить, но работать, а завтипов там вообще не будет). Не требуют длительной и ресурсоемкой перекомпиляции всей программы с доказательством ее корректности. И, если у нас вообще какие-то участки кода обмазанные контрактами почти никогда не используются, то они и не будут влиять на производительность. Мы вообще в типичной программе можем хотеть гарантий в 1% кода, остальные 99% могут работать по принципу «как-то работает и слава богу». Конечно бывают и противоположные варианты, но тогда придется тормозить на контрактах. Потому что выбора-то все равно никакого нет.

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

_Статически_ он может проверить только то, что срослось по (указанным разработчиком) типам. Т.е., что разработчик _предполагая_, что у него будет сортированный массив или валидный json не решит передать дальше какой-то мусор, а точнее чекер ему просто не позволит взять что попало, а только мусор попадающий в указанный тип. Но ведь и разработчик если не с бодуна не будет подставлять музыкальный трек вместо json'a. А чекнули мы этот пользовательский json все равно контрактом в рантайме и просто ему верим (контракту), потому что если он неверно работает - то никакие типы не помогут.

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

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

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

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

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

Но контракты, как система валидации данных, явно мощнее.

Любой контракт является функцией. Для любой функции X можно сопоставить тип «проверено функцией X». Зависимые типы позволяют для разных значений возвращать разные типы. Если рассматривать только контракты на входящие данные, а не на результат функции, зависимые типы не обязательны. Обычные алгебраические типы Haskell полностью эквивалентны произвольным контрактам на аргументы. Зависимые типы позволяют не выполнять лишние проверки (если уже проверили, что результат x больше нуля и x – бесконечное целое, нет смысла проверять, что x + 10 тоже больше нуля).

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

В чем ниша хаскеля? Как оказалось веб? :)

Если брать статистически, то всякие преобразователи данных. Pandoc, freearc, … У них код на хаскеле красивее получается.

Ну так я ровно об этом и писал, про веб мне рассказывал хаскелист.

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

Так статические типы вообще не про проверку данных. Они про проверку функций.

Это уже начинает быть похожим на упражнение в софистике. Функции как данные, код как данные :)

Ничего она не дает без нормальных зависимых типов (которых нет).

В общем случае даёт. Разве что вместо обычного if придётся пользоваться функциями типа

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

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

Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^W основа :)

В Typed Racket тоже зависимые типы

Они чем-то принципиально отличаются от зависимых типов LH?

Вот про то и речь. Что контрактами что-то проверяешь дважды, а что-то пропускаешь

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

В статической системе типов (хоть Haskell хоть Typed Racket) просто пропустить проверку не получится: программа не скомпилируется.

Так мы знаем все эти аргументы.

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

Я же привёл пример. Статика не позволит тебе пропустить проверку в начале цепочки.

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

А в динамике либо проверка происходит на входе каждой функции (оборонительное программирование)

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

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

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

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

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

Но контракты, как система валидации данных, явно мощнее. Т.е. как завтипы.

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

Ты давеча писал

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

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

Мы вообще в типичной программе можем хотеть гарантий в 1% кода, остальные 99% могут работать по принципу «как-то работает и слава богу».

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

Статически он может проверить только то, что срослось по (указанным разработчиком) типам. Т.е., что разработчик предполагая, что у него будет сортированный массив или валидный json не решит передать дальше какой-то мусор, а точнее чекер ему просто не позволит взять что попало, а только мусор попадающий в указанный тип.

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

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

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

Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^W основа :)

Хаскель не такая уж и плохая основа. GADT ghc + произвольный предикат LH – практически произвольный контракт.

Они чем-то принципиально отличаются от зависимых типов LH?

Нет.

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

Нет.

Делаем сортировку вставкой:

;; контракт
(define/contract (add-item a x)
  (-> sorted/c -> any/c -> sorted/c)
  ...)

;;  тип
(: add-item/t (-> Sorted Any Sorted))
(define (add-item/t a x) ...)

(: sorted/c (-> Any Boolean : Sorted)) 

;; вызываем версию с контрактом
(define a (get-array))
(set! a (add-item a 1))
(set! a (add-item a 2))
;; 4 раза вызвался sorted/c, неявно

;; вызываем типизированную
(define a1 (get-array))
(when (sorted/c a1) ;; добавляем тип
  (set! a1 (add-item a1 1))
  (set! a1 (add-item a1 2)))
;; sorted/c вызвался один раз, явным образом
monk ★★★★★
() автор топика
Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от alienclaster

А с контрактами - еще даже более строгая, чем система типов хаскеля.

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

В остальном, если до тебя не дошла мысль, то замени «строгую типизацию» на «контроль за эффектами» или «обмазывание монадами», в конце концов. Смысл от этого не поменяется: для каждого языка найдутся люди, которые будут пытаться язык запихнуть в любую нишу. И на с++ сайты пишут, например.

Ничего подобного, у С очевидные преимущества в написании драйверов перед лиспом, у кложи в разработки веба перед …

Это всё отлично, но из перечисленного большая часть позиционируется как «язык общего назначения» и на «чужие» ниши очень даже претендует. Драйвера и на С++ местами пишут и так далее.

Я совсем не спорю с тем, что если язык хорош для какой-то ниши, то он её захватывает. Но это совсем не значит, что успешно применять его можно только там. А когда доля языка мала, то возможны странные флуктуации. Вон куча блокчейнов пишут на расте, но я не уверен, что качества этого языка прям критичны в данном случае. Скорее удачное стечение обстоятельств: вовремя появился, акцент на «безопасность», не так принципиально было наличие библиотек для этой ниши.

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

Медицина тут бессильна.

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

Так в этом и дело! Ты вынужден будешь проверять эту ерунду каждый раз в каждой функции. Причём зачастую ничего не проверяют и остаётся гадать почему в этой функции «хрен_знает_что» undefined. По крайней мере, мой (к счастью весьма маленький) опыт с джаваскриптом и питоном был именно такой.

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

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

Контракты мощнее зав.типов, потому что выполняются в рантайме.

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

Это, по-твоему, веская причина не пользоваться статическими анализаторами?

Я наоборот за то, чтобы пользоваться статическими анализаторами, декларациями типов, частичным (локальным) выводом типов и так далее, но в _динамической_ среде (языке), то есть когда все это тебе не навязывают.

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

По твоей логике, варнинг в ide не нужен, ведь можно обмазать код контрактами, которые проверяют, что в процессе выполнения все имена well-scoped

Странно у тебя с чтением, особенно в контексте приводимой цитаты.

Можно написать «верни значение типа JSON, которое …, или доказательство того, что такого значения для этой строки нет». Но тогда разработчик захочет много денег, потому что задача сложная.

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

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

Конечно. А разработка нужна не сама по себе, это обычно какой-то бизнес или исследовательская задача и в обоих случаях там есть критерий time to market.

Но если вам достаточно гарантий в 1% кода, то, наверное, хаскель и прочие идрисы не для вас, там банально об стандартную библиотеку начнёте спотыкаться.

Про 1% это утрирование, хотя в случае вебни где-то близко к истине.

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

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

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

Любой контракт является функцией. Для любой функции X можно сопоставить тип «проверено функцией X».

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

Зависимые типы позволяют для разных значений возвращать разные типы.

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

Если рассматривать только контракты на входящие данные, а не на результат функции, зависимые типы не обязательны.

При достаточно мощной системе типов, да. Но тогда надо понять, чем она будет отличаться от зависимых типов - только отсутствием индуктивного доказательства? Но тогда, выходит, эта система типов будет гарантировать получение валидных данных, а что там в результате их преобразования получилось неизвестно. И проверять результат придется в рантайме.

Обычные алгебраические типы Haskell полностью эквивалентны произвольным контрактам на аргументы. Зависимые типы позволяют не выполнять лишние проверки (если уже проверили, что результат x больше нуля и x – бесконечное целое, нет смысла проверять, что x + 10 тоже больше нуля).

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

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

Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^W основа :)

Хаскель не такая уж и плохая основа. GADT ghc + произвольный предикат LH – практически произвольный контракт.

Попробуем. Надо будет только каких-то задач под это дело придумать.

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

Нет. Делаем сортировку вставкой:
;; вызываем версию с контрактом
;; 4 раза вызвался sorted/c, неявно

Что помешало проверить в динамической версии тип у а единожды перед тем как добавлять элемент?

(define/contract (add-item a x)

(-> sorted/c -> any/c -> sorted/c)

У тебя по контракту после добавления мы должны получить сортированную последовательность.

;; sorted/c вызвался один раз, явным образом
(set! a1 (add-item a1 1))
(set! a1 (add-item a1 2)))

А что у тебя оба раза пересортировка после добавления святым духом произошла? И где проверка типа результата после добавления элемента? В обоих случаях проверка должна быть 3-4 раза (4 в варианте, как ты написал для динамики, 3 если вначале проверить что а1 отсортированный уже, как в статической версии).

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

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

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

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

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

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

И что ты хотел этим сказать?

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

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

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

Требования какие к тому что пишут? Там же скорость обычно нужна максимальная. Скорость это у нас что? С++. Ну, вот поэтому раст и выбирают.

Скорее удачное стечение обстоятельств: вовремя появился, акцент на «безопасность», не так принципиально было наличие библиотек для этой ниши.

Это не «стечение обстоятельств», а объективные характеристики языка - быстрый, не такой инопланетный как хаскель, что-то гарантирует, избавляет от необходимости писать на С++. Бинго.

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

Медицина тут бессильна.

Самокритичненько.

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

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

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

Речь не о питоне с джаваскриптом.

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

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

Любое значение, проверенное некой функцией, можно привязать к соответствующему типу. Если что-то проверено string?, это тип String, если что-то проверено контрактом sorted/c, это тип Sorted. Для сложных контрактов значением является проверяемый кортеж.

Какое-то слишком общее утверждение.

Но реально суть именно в этом. Если мы просто проверяем контракт, нам достаточно типа провереноКонтрактомX. А если мы хотим указать, что массив на выходе имеет на два элемента больше, чем массив на входе, нужны зависимые типы или эквивалент (LH, Typed Racket).

При достаточно мощной системе типов, да.

Только для аналога контрактов достаточно любой системы типов, позволяющей вводить новые типы. Например, Си.

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

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

Зависимые типы позволяют этот процесс частично автоматизировать.

и на выходе, чтобы понять, что мы отдаем верный (по форме) результат.

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

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

Что помешало проверить в динамической версии тип у а единожды перед тем как добавлять элемент?

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

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

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

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

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

Если мы просто проверяем контракт, нам достаточно типа провереноКонтрактомX.

Да, и в большинстве случаев именно этого и достаточно / это и требовалось.

А если мы хотим указать, что массив на выходе имеет на два элемента больше, чем массив на входе, нужны зависимые типы или эквивалент (LH, Typed Racket).

Только для аналога контрактов достаточно любой системы типов, позволяющей вводить новые типы. Например, Си.

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

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

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

Зависимые типы позволяют этот процесс частично автоматизировать.

Так же как и контракты.

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

На да, зависимых типов вполне будет достаточно :) Если нам нужны более сложные проверки на этапе компиляции. И завтипы и контракты это все про проверку типов (привязанных к значениям), зависящих от входных параметров таких же сложных типов и так далее. Если это все не нужно - обычных типов, очевидно, хватит. Как и простых проверок / контрактов.

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

А хаскелисты говорят, что да.

То вы про разное. Контракты и типы, отражающие факт проверки контрактом эквивалентны (сопоставимы один-к-одному). А контракты и функции, являющиеся частями зависимых типов (и выполняемые при компиляции) — нет (потому что при компиляции не все условия на данные можно выполнить).

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

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

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

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

Так а если у тебя ошибка в алгоритме? :) Как ты прогарантируешь? На слово тебе поверить?

А в случае контрактов по крайней мере одна проверка сортированности массива (на входящие данные) будет выполняться на каждый вызов add-item.

Подозреваю, это неверно написанный контракт.

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

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

А как? Пишешь, например, библиотеку по работе с сортированными массивами. Есть функция вставки в сортированный массив? Неужели не будешь проверять, что тебе передают как аргумент? Фактически, без типов всего два выбора: либо тормоза на каждый запуск и O(n) вместо O(log n) либо проверяем что это какой-то массив и всё (в документации пишем, что передача неотсортированного массива UB).

Так а если у тебя ошибка в алгоритме? :) Как ты прогарантируешь? На слово тебе поверить?

На листочке. Плюс тесты.

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

Контракты и типы, отражающие факт проверки контрактом эквивалентны (сопоставимы один-к-одному).

Да, если мы понимаем под этим одно и то же - проверенные данные можно тегнуть как «проверенные».

А контракты и функции, являющиеся частями зависимых типов (и выполняемые при компиляции) — нет (потому что при компиляции не все условия на данные можно выполнить).

Хорошо, а почему ты решил что мы о разном говорим?

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

Да, если мы понимаем под этим одно и то же - проверенные данные можно тегнуть как «проверенные».

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

Хорошо, а почему ты решил что мы о разном говорим?

Из последовательности:

я: Любой контракт является функцией. Для любой функции X можно сопоставить тип «проверено функцией X».

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

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

А как? Пишешь, например, библиотеку по работе с сортированными массивами. Есть функция вставки в сортированный массив? Неужели не будешь проверять, что тебе передают как аргумент?

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

Фактически, без типов всего два выбора: либо тормоза на каждый запуск и O(n) вместо O(log n) либо проверяем что это какой-то массив и всё (в документации пишем, что передача неотсортированного массива UB).

Статика чем тебе поможет убедиться в том, что массив отсортирован верно? Ну, то есть если у нас все данные доступны в компайлтайме, то наверное поможет, ты эти же вычисления в теории можешь провести просто в компайл тайме (и тормозить в нем). Но обычно никаких данный у тебя нет, и появляются они только при выполнении программы. И мы возвращаемся к вопросу как ты статически будешь чекать то что пришло извне? Остаются только потом типа более надежные преобразования, но которые могут быть легко запороты просто ошибкой в алгоритме. Да, ты будешь знать что на входе у тебя сортированная поледовательность (проверишь контрактами), и что на выходе тоже сортированная. Только она может быть отсортирована неверно, поэтому толку от этого не так и много.

Так а если у тебя ошибка в алгоритме? :) Как ты прогарантируешь? На слово тебе поверить?

На листочке. Плюс тесты.

Так это то же самое UB, лол. Везде мы должны поверить «что нам пришли правильные данные». А надо было бы _проверить_, вот как в контрактах - и тормозить. То есть статика опять ничего тут не дала, кроме *локальной* помощи разработчику, чтобы немного вселить в него уверенности в том что он передал _какой-то_ массив, возможно сортированный если он не ошибся в алгоритме), а не строку (при этом ничего не гарантируется).

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

Хорошо, а почему ты решил что мы о разном говорим?

Из последовательности:

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

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

Но это не означает, что такую же проверку надо делать

Но это _означает_ («не» лишнее, опечатка).

Смотри, в твоем примере на ракете со статикой vs контракты. Контрактами мы проверяем все время, и вторая проверка идет после первого set!, то есть мы знаем (снова) что измененный массив - опять проверен на соответствие контракту. А в случае статики мы ведь этого не знаем? Мы просто надеемся, что алгоритм вставки отработал как надо. А хотелось бы убедиться, так это или нет.

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

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

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

int max(int x, int y)
{
  int r = x > y?x:y;
  assert (r >= x);
  assert (r >= y);
  assert (r - x + 1 > 0);
  assert (r - y + 1 > 0);
  if (x < y) assert (r == y);
  if (y < x) assert (r == x);
  // похоже, <, >= и сравнение с нулём работают верно
  return r;
}
monk ★★★★★
() автор топика
Ответ на: комментарий от monk

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

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

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

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

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

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

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

Везде мы должны поверить «что нам пришли правильные данные».

Нет же. Мы имеем гарантию, что данные проверены (иначе они не были бы правильного типа). Мы должны только поверить, что контракт действительно проверяет факт сортировки и алгоритм addElem действительно её не нарушает.

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

мы верим и данным в примере на ракете

Мы верим, что add-elem при получении сортированного массива всегда вернёт сортированный массив. Данным мы не верим. Но все данные после первой проверки получены из доверенных источников.

Второй вариант - нас интересует не то каким алгоритмом он отсортирвоан, а что данные находятся в сортированном виде.

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

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

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

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

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

Ну как на питоне напишешь
readFile templateFile
>>= foldM (processLine processTemplate) context . lines
>>= writeFile outFile . unlines . reverse . result
Так красиво не получится

Вообще-то в питоне есть итераторы, которые и реализуют ленивость. И в том же F# есть ленивость. Я хз, как там с ленивостью в ракете.

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

Вообще-то в питоне есть итераторы, которые и реализуют ленивость.

Я не про ленивость, я про красоту (эстетику). Когда всё компактно и наглядно. Если брать именно возможности семантики, то Racket вне конкуренции: там есть всё, что можно и даже чего нельзя.

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

int r = x > y?x:y;
assert (r >= x);
assert (r >= y);
assert (r - x + 1 > 0);
assert (r - y + 1 > 0);
if (x < y) assert (r == y);
if (y < x) assert (r == x);

Это смешно, но не смешно, потому что я так свою сиху пишу. А иначе нельзя — чем больше дублирования проверок, тем больше шанс, что ошибка не пройдет. Но и больше трудоемкость, и ниже читаемость.

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

Я не про ленивость, я про красоту (эстетику). Когда всё компактно и наглядно. Если брать именно возможности семантики, то Racket вне конкуренции: там есть всё, что можно и даже чего нельзя

Ты можешь сделать with open(templateFile, 'r') as file — файл является итератором по строкам. Дальше либо передавать этот итератор в функции обработки напрямую, либо for line in file.

writelines аналогично принимает итератор.

Если нужно кастомные итераторы — пишешь функцию-генератор.

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

… writelines аналогично принимает итератор.

И вместо

readFile templateFile
  >>= foldM (processLine processTemplate) context . lines
  >>= writeFile outFile . unlines . reverse . result

получим что-то вроде

with open(templateFile, 'r') as file:
  for line in file.readlines():
    context = processLine(processTemplate)(context, line)
  open(outFile, 'w').writelines(context.result.reverse())

По-моему, гораздо менее красиво.

monk ★★★★★
() автор топика
Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от monk

Я не пойму, что это за processLine(processTemplate), но с большой долей вероятности ты пишешь неидеоматичный код на питоне, пытаясь один в один перевести функции хаскеля. А мне, например, кажется дикостью попытка ввода неявных правил последовательной обработки (конвеера) при помощи возвращаемого типа. Тот же F# делает ровно наоборот: конвеерная обработка сделана явной (context expression), а умолчательное последовательное выполнение не отличается от «чистых» выражений.

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

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

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

А в динамике не так? Проверили один раз входящие данные, и затем так же применили функцию сортировки.

Везде мы должны поверить «что нам пришли правильные данные».

Нет же. Мы имеем гарантию, что данные проверены (иначе они не были бы правильного типа).

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

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

Второй вариант - нас интересует не то каким алгоритмом он отсортирвоан, а что данные находятся в сортированном виде.

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

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

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

На моё утверждение «проверка (входных) данных произвольными контрактами равноценна проверке данных типами» ты даёшь ссылку

Там вообще была ветка общения с Laz, параллельная.

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

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

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

А в динамике не так? Проверили один раз входящие данные, и затем так же применили функцию сортировки.

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

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

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

Ок. Тогда теряем только одну проверку сравнения на входе и один malloc на выходе. В остальном эквивалент статики. И тогда вместо контрактов всюду получаем проверку (динамическую) на типы.

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

Везде мы должны поверить «что нам пришли правильные данные».

Нет же. Мы имеем гарантию, что данные проверены (иначе они не были бы правильного типа).

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

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

Потому исчерпывающее доказательство получается только для крайне ограниченных вариантов hello world-а.

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

А в динамике функция не знает, кто её вызывает.

В Racket пошли на компромисс: контракты проверяются только на границе модуля.

Ну, я о таком «компромиссе» и писал, когда говорил что проверяем на входе и на выходе. А все что внутри считаем трастовым.

То есть если add-item вызывается внутри модуля (обработки сортированных массивов), то контракт не проверяется.

Это логично, хотя и да, компромиссное решение.

Но если он экспортирован и вызывается так, как я описал, контракт применяется на каждый вызов.

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

У add-item нет возможности узнать, что данные пришли из другого вызова add-item.

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

alienclaster ★★★
()
Последнее исправление: alienclaster (всего исправлений: 1)
Ответ на: комментарий от monk

Ок. Тогда теряем только одну проверку сравнения на входе и один malloc на выходе. В остальном эквивалент статики. И тогда вместо контрактов всюду получаем проверку (динамическую) на типы.

Да.

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

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

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

Потому исчерпывающее доказательство получается только для крайне ограниченных вариантов hello world-а.

Исчерпывающие - слишком общая формулировка чего бы то ни было.

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

А Вы меня радуете. Спасибо за тёплые слова «Мир», «Бесконечнось доказательств», «Тьюринг».

Как Вы относитесь к Haskell?

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

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

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

Скорее, я имел в виду, что хаскель совсем не имеет инструментов упрощения разработки с побочными эффектами. Он отгораживает побочки, но что делать, если всё приложение слеплено из побочек? Это весь UI, это БД — а если всё это выкинуть, то что остается? Упомянутые выше трансляторы DSL-ей, которые получают на вход строго формализованные единичные запросы и выдают единичный выхлоп — с интерактивностью хаскель уже не справляется.

Исчерпывающие - слишком общая формулировка чего бы то ни было

Исчерпывающая — значит исчерпывающая все возможные варианты выполнения. Основная ведь проблема в чем? В том, что программа имеет более одного набора входных данных и условий, и частенько я не могу быть уверен, что расчитал работу программы для всех условий. И речь тут не только про корректность типов, но и банальную корректность арифметики, чтобы у меня внезапно не возникло деление на ноль или противоположный знак. А в случае вычислений с плавающей точкой покрыть все диапазоны значений крайне тяжело. Не в последнюю очередь поэтому энтерпрайза на хаскеле с плавающей точкой нет или почти нет.

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

что делать, если всё приложение слеплено из побочек?

Страдать и плакать.

Это весь UI

Не обязательно ведь размазывать эффекты тонким слоем по всему гую.

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

Как Вы относитесь к Haskell?

Я поверхностно изучал его. Ну то есть как поверхностно... несколько дней провел изучая его — этого оказалось достаточно для того, чтобы написать и понять принцип работы hello world. Помню, как весело я рвал волосы на голове, пытаясь понять, что же такое монада и при чем тут контейнеры, которые почему-то из раза в раз повторяются во всех гайдах по монадам. И без которых не получится понять, как же работает hello world. Короче говоря, создатели языка приложили все усилия для того, чтобы на нем нельзя было писать прикладные программы — но зато по языку бодро пишут научные работы.

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

Скорее, я имел в виду, что хаскель совсем не имеет инструментов упрощения разработки с побочными эффектами

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

Он отгораживает побочки, но что делать, если всё приложение слеплено из побочек? Это весь UI, это БД

У тебя, у тебя эффекты только когда в базу пишешь, а преобразования могут быть чистыми. gui может инкапсулировать (почти) всю императивщину в frp.

с интерактивностью хаскель уже не справляется

Вопрос же на каком уровне это происходит, что там под капотом никого не интересует.

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

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

Не в последнюю очередь поэтому энтерпрайза на хаскеле с плавающей точкой нет или почти нет.

А при чем тут хаскель?

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

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

Адвокаты хаскеля утверждают, что ад плана «STM STRef IO a» и отсутствие возможности сделать банальный print в функции — это какое-то там удобство для упрощения контроля побочек. Однако же, если этих побочек много, то цепочки из монадических контейнеров начинают взрывать мозг. Даже в банальном Си есть свободное комбинирование функций с побочками — вот тебе и весь «инструмент упрощения». Собственно, диалекты ML являются более близким аналогом хаскеля, со статической типизацией и компиляцией, при этом позволяют свободно комбинировать чистые и грязные функции.

У тебя, у тебя эффекты только когда в базу пишешь, а преобразования могут быть чистыми. gui может инкапсулировать (почти) всю императивщину в frp

У тебя прям позиция хаскелиста. К сожалению, если у БД более одного пользователя, то может оказаться, что писание в базу растянуто по времени, и во время этой записи могут происходить параллельные записи. Даже если допустить, что запись одна, как в SQLite — параллельных чтений может быть несколько.

gui может инкапсулировать (почти) всю императивщину в frp

На эту тему я люблю говорить, что хаскель — это дергалка для сишных функций. Потому что именно они будут выполнять большую часть работы, а хаскелевая часть останется в качестве декларативного конфига, аки CSS. Ведь даже это самое FRP нужно чем-то выполнять, и это «что-то» будет иметь императивный стиль с большим числом побочек. Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

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

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

Плюс вместо минуса может возникнуть, например, если ты поделишь число на че-то квадрат, забыв учесть, что квадрат минус съедает, а у делимого этот минус остается — и вот у тебя уже минус протёк туда, где ты его не ожидал. Более тонкая проблема возникла, например, на Ariane 5, где число просто вышло за предполагаемые границы, из-за чего посыпалась зависимая арифметика.

Не в последнюю очередь поэтому энтерпрайза на хаскеле с плавающей точкой нет или почти нет.

А при чем тут хаскель?

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

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

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

Не вижу тут в упор проблем в разрезе чистоты.

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

Так можно о много чем сказать, и ты например так говоришь и о python, и о clojure. Только смысл данного утверждения от меня ускользает - потому что нас не волнует что находится внутри, ассемблер, vhdl, регистры, вообще до лампочки.

Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

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

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

В зависимых типах как раз можно это гарантировать, иначе зачем они вообще нужны.

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

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

Более тонкая проблема возникла, например, на Ariane 5, где число просто вышло за предполагаемые границы, из-за чего посыпалась зависимая арифметика.

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

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

Какие проблема использования хаскеля для вычислений с плавающей точкой?

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

Простите за оффтоп, а Вы на каком дистрибутиве остановились? Я просто решил почитать Ваши темы, @byko3y как Ваш оппонент тут неясен:

несколько дней провел изучая его

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

О чем речь, о дистрибутивах линукса? На серверах использую ubuntu, родственникам ставлю mint и guix, а у меня весь софт привязан к венде.

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

python, common lisp и немного clojure. Использую emacs и eclipse (по историческим причинам, скорее всего буду полностью с него спрыгивать на emacs).

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

Для haskell есть какой-то аналог slime? Хотелось бы отправлять выражения в репл по хоткеям хотя бы, чтобы не весь модуль и прочие полезные штуки.

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

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

Не вижу тут в упор проблем в разрезе чистоты

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

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

Так можно о много чем сказать, и ты например так говоришь и о python, и о clojure. Только смысл данного утверждения от меня ускользает - потому что нас не волнует что находится внутри, ассемблер, vhdl, регистры, вообще до лампочки

Исходная работа по реактивному программированию где-то из девяностых как раз и применяла декларации на хаскеле для декларативного программирования анимации. Только дело в том, что это уже пользователськие данные, конфиги, а не программы. Да, ты можешь поспорить, что картинка JPEG — это тоже программа, по которой компьютер рисует картинку, но эта «программа» жутко примитивна и ограничена, и не Тьюринг-полна при условии соблюдения этих ограничений. Тот же React.js изначально был просто шаблонизатором, а перестал быть лишь шаблонизатором, когда в нем появилась императивщина плана setState.

Не говоря уже о том, что на чистом FRP не получится писать более-менее сложные интерфейсы.

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

Это тоже фактор, иначе бы операционные системы писали на питоне. Те же БД пишут с параллельным доступом из соображений производительности — иначе бы все сервера работали на SQLite с единственной глобальной блокировкой чтения и записи. В конце-концов машину Тьюринга можно представить как чистую функцию, которая берет предыдущее состояние и вычисляет следующее чистой функцией — мы просто приходим к абстрактным коням в вакууме. Я же говорю с прагматичной позиции, оцениваю то, что можно реализоваать и что будет хоть как-то полезно, и с прагматичной позиции у FRP очень ограниченные возможности, а чтобы их расширить — нужно уйти от FRP, оно становится третьей ногой.

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

В зависимых типах как раз можно это гарантировать, иначе зачем они вообще нужны

Неужели есть такие зависимые типы, которые умеют распознавать радости аппаратных реализаций вещественных чисел, вроде 3.129999999?

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

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

Это задачи «результат не должен выходить за определенные диапазон», в число которых входит также «результат не должен быть равен нулю», которую нужно решить для исключения деления на ноль. Может у тебя есть на примете язык, который будет через связанные типы данных гарантировать, что для переменных x и y всегда будет выполняться условие (cos x)²+(sin y)² = 1?

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

Неужели есть такие зависимые типы, которые умеют распознавать радости аппаратных реализаций вещественных чисел, вроде 3.129999999?

http://flocq.gforge.inria.fr/theos.html

Может у тебя есть на примете язык, который будет через связанные типы данных гарантировать, что для переменных x и y всегда будет выполняться условие (cos x)²+(sin y)² = 1?

Для IEEE-754 это неверное условие.

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

Ы-ы-ы, они превращают вещественные числа в целые с округлениями.

Так если вещественные в компьютере так представлены.

Каким образом неверное? IEEE-754 запрещает тригонометрию?

Ага. И местами арифметику. x / y * y == x, где y > 0 тоже не выполняется.

monk ★★★★★
() автор топика
Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от monk

Ы-ы-ы, они превращают вещественные числа в целые с округлениями.

Так если вещественные в компьютере так представлены

Нет, они именно округляют их с потерей точности.

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

Нет, они именно округляют их с потерей точности.

Чтобы произвольное математическое вещественное вещественное число получить в IEEE-754, его необходимо округлить с потерей точности.

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

Вот есть у нас функция f, yield-ящая цифры числа пи. Было бы здорово, если бы sin[f] по термам внутри f выводил, что это ноль. И так для любых (ну ок, почти любых) полезных f и sin.

От тогда-то (никогда) и заживём.

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

Было бы здорово, если бы sin[f] по термам внутри f выводил, что это ноль

В общем случае это вполне выводится. На зависимых типах можно доказать почти любую математическую теорему. Соответственно, доказать что-то типа sin(f) стремится к нулю при увеличении точности разложения вполне можно.

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

А можно там все-таки отправлять выражения в репл по хоткеям? Дока объемная, если ты пользуешься постоянно по-идее должен быть в курсе. После slime мне сложно даже заставить себя что-то на петончеке писать из-за вот этих вот штук. leksah как я понял это отдельный редактор для прожжоных хаскелюг.

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

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

Simon Peyton Jones used Emacs, really.

https://www.youtube.com/watch?v=iSmkqocn0oQ

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

Я больше не могу, честно.
После Вашего врыва в тред мне стало слегка не по себе.

Есть дядечка, который пишет интересые книги.
Рекомендую некую абстракцию, чтобы на минимальном уровне причаститься. https://www.youtube.com/watch?v=t1e8gqXLbsU

Надеюсь в дальнейшем с Вами плодотворно общаться в FP.

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

А можно там все-таки отправлять выражения в репл по хоткеям?

В leksah в фоне ghci работает и выражения отправляются туда в процессе печатания. Там сразу пытаются выполниться и показывают ошибку. Можно также зайти в REPL явно и посмотреть какие значения получаются при вызове написанных функций.

Второй не пробовал, но по документации должен работать похоже.

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

жидкие типы

Чтобы вас не называли жидким типом, нужно записаться в спортзал …

Владимир

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

Чтобы вас не называли жидким типом, нужно записаться в спортзал …

Тогда будут называть жудким типом.

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

Меня часто чуханили в школе и в дальнейшем. Пока я не начал ходить в спортзал ..

Владимир

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

да ты и щас чухан..

Владимир

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

А в чём пишете код на Windows?

Я пишу в блокноте с парой плагинов. Старая школа, знаете ли …

Владимир

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

Нужен переносимый. Вот скомпилировал я программу с gi-gtk. Для этого Haskell выкачал msys с половиной линукса.

Если бинарник переложить в другую папку и положить рядом все библиотеки, которые показал ldd, начинает падать в неожиданные моменты (например по пункту меню «вставить emoji» в textview, отключить пункт меню нельзя) и матерится про отсутствующий dbus. Распространять программу со всей папкой msys2 на 7 гигабайт?

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