Снова о статической типизации

Т. Е. Функции mapcar мы передаем 1) Функцию f, 2) произвольное число списков n. При этом функция f должна принимать n аргументов (по одному из каждого списка). Ну и результат есть список результатов применения функции к соответствующим элементам аргументов?

Да. При этом тип аргумента функции должен соответствовать типу соответствующего списка.

На Typed Racket я такое могу изобразить, на Haskell уже никак.

Впрочем, на Haskell даже простенькое

data Cons a b = Cons a b

lenCons (Cons a (Cons b c)) = 1 + lenCons (Cons b c)
lenCons _ = 1

не типизируется.

Мне кажется или это похоже на аппликативный функтор, только в список обёрнутый как то?

Похоже. Только для произвольного количества списков. Для любого конкретного конечного количества проблемы нет. А вот сделать тип «кортеж из любого числа списков» уже никак. Система типов такое не описывает.

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

пару Cons a b сделать можно, но на ней нельзя делать рекурсивные функции.

пару Cons a b сделать можно, но на ней нельзя делать рекурсивные функции.

Даже нельзя сделать так, чтобы b обязательно было Cons.

Что-то типа

data Cons a = Nil | Cons a Cons

Поэтому, там, где в динамических языках есть zip, map, curry, в Haskell есть zip2, zip3, … zip7, zipWith (почему не map2???), zipWith3 (почему не map3???), zipWith4, … zipWith7, curry2, … curry4.

Ещё одна проблема — пространство имён.

В лиспах я пишу:

(defun f (x)
  (if (= x 0) 'error (+ x ...))

(defun g (x)
  (if (= x 0) 'error (format t "~a" x))

В Haskell надо сделать типы. Один тип «число или error» второй «строка или error».

data ResF = N Int | Error
data ResG = S String | Error

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

data ResCalcF = CalcFN Int | CalcFError
data ResFormat = FormatS String | FormatError
data ResAge = AgeS String | AgeF Float | AgeError
...

или используешь Maybe вместо символа если у тебя один вид символа и Either если несколько (и переписываешь программу, если вдруг добавилась ветка со вторым символом).

А с Either ещё и принудительно расширяешь тип результата.

В исходнике было

f : (integer? ->  (or/c integer? 'overflow 'division-by-zero))

а в Haskell пишешь

f :: Int -> Either String Int

и ограничение на список символов пропадает.

Для начала порты бывают двух видов

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

Если тип данных [1024;65536] в вашей системе типов непредставим, то и дальнейшую пользу от статической типизации вы получить не сможете

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

Просто для Боинга.. как бы это помягче.. ну нет убытков от того что иногда, раз там в N лет, самолёт упадёт из-за ошибки в ПО.. понимаете? Ну какой им от этого убыток?

Уже заметный убыток, а в перспективе они могут и доиграться, как раз из-за того что забили на качество:
Reuters: производство Boeing 737 MAX резко упало после проверок властей США
Акции Boeing упали на фоне проверки в США и смерти бывшего инженера

В исходнике было

А что толку, если в вызывающей функции придётся делать type case в рантайме(?), причём специфичный для данного списка типов. Как сделать обобщённый bind (>>=) если веток больше двух и вообще переменное количество?

open Result

exception Error

let f x =
  if x = 0
  then error Error
  else ok (x + 42)

let g x =
  if x = 0
  then error Error
  else ok (Printf.sprintf "%d" x)

exception Overflow
exception Division_by_zero

let f2 : int -> (int, exn) result = function
  | 0             -> error Division_by_zero
  | x when x > 42 -> error Overflow
  | x             -> ok (x + 42)

let bindf f x = bind x f

let main x =
  f2 x
  |> bindf f
  |> bindf g
  |> map_error Printexc.to_string
  |> fold ~ok:print_endline ~error:print_endline

let () =
  main 0 ;
  main 43 ;
  main (-42) ;
  main 1

=>

Division_by_zero
Overflow
Error
85

А потом вспомнил из недавно читаного ZeroMQ Guide категорический рецепт избавления от любых проблем с многопоточностью: «just don’t share state». (Мужик конечно жжот, люблю максималистов, хотя по здравому размышлению, заменять atomic bool stopBgThread посылкой сообщения stop фоновому потоку я не готов – но твой случай явно посложнее будет.)

Shared state может быть неявным. Поток 1 ждёт сообщения от потока 2, поток 2 ждёт сообщения от потока 1. Deadlock.

Или какие-то хитрые комментарии добавлять.

А потом еще нужно убедиться, что комментарий:

1. Подписан именно такой, какой для этой функции надо.
2. Нигде не прощен.

Что будет эквивалентно созданию частной системы типов под данную задачу.

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

Пример с простыми числами хорошо показывает, почему к «матану», которым так гордится анонимный тролль (на самом деле – юзер masterOf), работает универсальный принцип про дурака и стеклянный предмет.

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

А если мы делаем:

функцию, заведомо производящая значения данного типа.

то ровно в этом месте формальная верификация превращается в классический аудит

Ну в практическом отношении тип «целое число от 0 до 300» можно описать просто предвычисленным перечислением + описание инварианта для данного перечисления. Инвариант проверяется компилятором. Наверное на шаблонах C++ можно такое провернуть.

Или скажем, можно описать тип, который содержит простые множители числа 1 522 605 027 922 533 360 535 618 378 132 637 429 718 068 114 961 380 688 657 908 494 580 122 963 258 952 897 654 000 350 692 006 139.

Но невозможно заставить компилятор вывести значения этого типа. Если ты только не потусторонняя зелёная летучая мышь.

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

Реализовать add(Int, Int ) -> Optional<Int> можно на чём угодно, только в нашем мире так не принято. Принято писать по принципу «да похрен на переполнения»

И если вдруг шаблон разворачивается в a+b-b, то нельзя заменять на a, надо вычислять сумму и проверять на переполнение.

Почему нельзя? В Си и Си++ не гарантирован порядок вычислений внутри арифметического выражения. При вычислении a+(b-b) никакого переполнения нет.

Более того, смысл переполнения в том, что результат вычисления выходит за рамки представимого диапазона. А результат вычисления a+b-b заведомо лежит в диапазоне типа переменной a при любом b.

Поэтому в выражении (a+b)*c*2+3 может содержаться от 4 до 0 проверок, в зависимости от того, что именно компилятор знает о диапазонах значений, которые могут принимать эти переменные.

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

Кто сказал, что это важно для примера?

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

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

Покажете как? На случай если беседа примет оборот «а вот мы сделаем класс и в конструкторе всё проверим», сразу контртезис: а) это проверяется на этапе работы, т.е. в динамике; б) в случае позднего связывания мы узнаём какой метод вызываем только в процессе работы, снова динамика; в) а вот, что мы гарантированно не забудем сделать проверку, признаю, полезное свойство.

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

Какому еще «пользователю»? Тип проверят то, что описал в нём программист. Это инструмент для разработчика, чтобы структурировать кисель в чёткую архитектуру.

Покажете как? На случай если беседа примет оборот «а вот мы сделаем класс и в конструкторе всё проверим», сразу контртезис: а) это проверяется на этапе работы, т.е. в динамике; б) в случае позднего связывания мы узнаём какой метод вызываем только в процессе работы, снова динамика; в) а вот, что мы гарантированно не забудем сделать проверку, признаю, полезное свойство.

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

В условном «питоне» (или php, ruby, не важно) у тебя в любом месте, где написано def foo(ip_port), дальше придётся ставить assert, который проверяет что: 1) ip_port вообще число; 2) ip_port число в корректном диапазоне. И это всё равно никак не спасёт от того, что foo() вместо номера порта в рандомный момент времени получит сводку с прогнозом погоды под Хабаровском.

Аналогично и для случая ip_port = bar().

Если же у нас есть foo(ip_port: IpPort), то вызывающая сторона заведомо передаёт число в нужном диапазоне.

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

да, я тебе показал как в питоне оно работает

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

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

Какому еще «пользователю»?

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

И это всё равно никак не спасёт от того, что foo() вместо номера порта в рандомный момент времени получит сводку с прогнозом погоды под Хабаровском.

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

И вот еще в дополнение.

Что делать, если ip_port в def foo(ip_port) оказался мусором? Кидать исключение? Вызывать Abort? Жаловаться в stderr и как-то продолжать работу на костылях?

Любой вариант очень хлипок из-за отсутствия чёткого контракта.

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

Всё это замечательно

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

но совершенно не отменяет претензии «проверяется, не то что нужно, а то, что проще проверить»

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

Кидать исключение? Вызывать Abort? Жаловаться в stderr и как-то продолжать работу на костылях?

Это решать программисту. Мы же (и компилятор тоже) не знаем зачем он этот порт открывет. Если это веб-сервер, то программа должна сделать сепукку, бо без открытия порта её жизнь не имеет смысла. А если она метрики для мониторинга через этот порт предоставляет, то ругнуться в логи и жить с этой болью дальше.

Супер. Вот именно за этим и нужен тип.

Но этого мало. В случае статической типизации у нас, условно, два варианта:

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

2. Мы упарываемся типами, пытаемся сделать настоящие контракты, всю программу строим вокруг типов … и что мы за это получаем? Автоматическую напоминалку не забыть проверить (самостоятельно) входные данные, т.е. то, что достигается минимальным уровнем самодисциплины (и у маломальски опытных питонистов-пэхапэшников делается автоматом). Это жульничество, настоящее жульничество.

Вы знаете более продвинутый способ работы с контрактами и инвариантами при разработке программы?

Тестирование.

Это решать программисту. Мы же (и компилятор тоже) не знаем зачем он этот порт открывет. Если это веб-сервер, то программа должна сделать сепукку, бо без открытия порта её жизнь не имеет смысла. А если она метрики для мониторинга через этот порт предоставляет, то ругнуться в логи и жить с этой болью дальше.

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

Совсем другое дело, когда алгоритм соврешенно точно, однозначно, предназначен работать с IpPort. И его никак не перепутать с Optional<IpPort>.

Но этого мало.

Мало для чего?

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

Fixed: неплохо защищает от опечаток, неплохо помогает делать refactoring.

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

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

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

Применять самодисциплину ВМЕСТО инструментов, а не ВМЕСТЕ с инструментами – как происходит этот логический сбой?

достигается минимальным уровнем самодисциплины (и у маломальски опытных питонистов-пэхапэшников делается автоматом)

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

Теперь бинго для типичной темы ЛОРа по статической типизации собрано.

Тестирование.

И это тоже. Это предпоследний пункт для бинго. Что мешает использовать тестирование ВМЕСТЕ, а не ВМЕСТО системы типов?

Вы знаете более продвинутый способ работы с контрактами и инвариантами при разработке программы?

Тестирование.

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

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

Вот вы говорите:

На случай если беседа примет оборот «а вот мы сделаем класс и в конструкторе всё проверим»

Перефразируем для данного примера: «а вот мы сконвертируем строку в число, будем передавать Integer в функции»

сразу контртезис: а) это проверяется на этапе работы, т.е. в динамике

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

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

Ну и что, собственно? Главное, что контракт зафиксирован.

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

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

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

https://clojure.org/guides/spec

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

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

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

Ну надо передать массив как аргумент, а не кортеж :)

В Си и Си++ не гарантирован порядок вычислений внутри арифметического выражения.

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

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

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

Что будет эквивалентно созданию частной системы типов под данную задачу.

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

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

Не любой. Только такой, где некоторый результат анализа гарантирован.

Например, разные проверки по эвристикам и угадывание ошибочных паттернов, как это делают тулзы типа cppcheck, под это не попадают.

gcc -fanalyzer тоже.

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

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

Кстати, насколько я помню, для чисел с плавающей точкой всё-таки порядок вычислений внутри арифметического выражения гарантирован.

А вот для них как раз сложение не коммутативно. Поэтому и.

Ну надо передать массив как аргумент, а не кортеж :)

А в массиве нельзя хранить значения разных типов.

Не любой. Только такой, где некоторый результат анализа гарантирован.

Хорошо. Любой детерминированный.

gcc -fanalyzer тоже.

Почему? Чем

warning: double-‘free’ of ‘ptr’ [CWE-415] [-Wanalyzer-double-free]

отличается от того, что значение ptr является линейным типом относительно использования в free?

Почему?

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

Кроме того, она еще и сырая в настоящее время, у меня false positive даёт.

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

Коммутативна, но не ассоциативна и не дистрибутивна в арифметике с переполнением.

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

В Haskell тоже постоянно вводят что-то новое или переделывают старое. Там тоже не строгая система типов?

Кроме того, она еще и сырая в настоящее время, у меня false positive даёт.

Сырость компилятора не аргумент против системы типов.

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

вычеты-шмычеты вообще тут не причем

Сырость компилятора не аргумент против системы типов.

Тут дело такое, что это не core feature языка, а приделка сбоку.

Если же какой-то большой проект действительно будет завязан на такую систему типов как на существенную фичу, то все false positive и false negative оттуда бы быстро вычистили.

А так, конечно, штука хорошая.

Коммутативна, но не ассоциативна и не дистрибутивна в арифметике с переполнением.

Почему не ассоциативна?

A+B+C даёт одинаковый результат при любом порядке вычисления.

Кстати, было бы весьма интересно, если бы линейные типы официально добавили в спецификацию Си.

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

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

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

Вот есть функции для работы со списками: car, cdr, map, filter, …

Если язык динамический, то в первой строке каждой из них надо проверить, что переданный аргумент нужного типа. Или не проверить и тогда пользователь вместо осмысленной ошибки «в вызове map(f, 1) второй аргумент должен быть списком» получит что-то вроде «в вызове map(f, 1) первый аргумент функции car не является списком». Причём ошибка будет при выполнении программы.

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

А при выполнении функции ни одного такта не будет потрачено на проверку того, что данные переданы верно, так как это уже проверено при компиляции.

Тут дело такое, что это не core feature языка, а приделка сбоку.

Liquid Haskell не система типов? И многочисленные расширения Haskell?

Если же какой-то большой проект действительно будет завязан на такую систему типов как на существенную фичу, то все false positive и false negative оттуда бы быстро вычистили.

Они не всегда устранимы.

A+B+C даёт одинаковый результат при любом порядке вычисления.

Предположим, их тип значения -127..128.

А = -120, B = 120, C = 120

(A + B) + C = (-120 + 120) + 120 = 0 + 120 = 120

A + (B + C) = -120 + (120 + 120) = -120 + переполнение(240 не является допустимым значением) = переполнение.

Это ровно та причина, почему в Си для unsigned выбрана семантика переполнения, для signed выбрана семантика UB, и ни для одного типа не выбрана семантика checked.

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

1. Результат помещается в разрядную сетку.
2. Результат математически правильный.

А вот если использовать checked int, то операция сложения перестает быть коммутативной и ассоциативной. В ней появляется явным образом специфицированный побочный эффект в виде броска исключения или порождения Not-a-Number.

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

Ладно, попробуем что нибудь придумать

А вот если использовать checked int, то операция сложения перестает быть коммутативной и ассоциативной. В ней появляется явным образом специфицированный побочный эффект в виде броска исключения или порождения Not-a-Number.

Коммутативной остаётся. a + b == b + a.

Это ровно та причина, почему в Си для unsigned выбрана семантика переполнения, для signed выбрана семантика UB, и ни для одного типа не выбрана семантика checked.

Для Си во главу угла поставлена скорость. Для Си++ Zero-cost Abstraction. Если же кому-то очень надо, то https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html

Коммутативной остаётся.

Да. Сначала отправил, потом подумал.

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

Плохо, что они не стандартизированы.

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

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