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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^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 вызвался один раз, явным образом

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Нет.

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

Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^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 отсортированный уже, как в статической версии).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ты видел мёртвых, великих и малых? Они стояли перед троном и перед раскрытыми книгами.

Вместо того, чтобы окучивать Variant, суёте нос в слабомутные типы IO.

Не обращайтесь к идолам и не отливайте себе богов из металла.

_$_ : ∀ {A V F T} → (Σ {A} V F ⤇ T) → (a : A) → (♭ F a ⤇ T)
inp P   $ a = ♭ P a
out b P $ a = out b (P $ a)

IO _$_ Прибыльное дело WWW3 под шконкой зарубежного сообщества :)

split? : (Byte → Bool) → Bytes ⇒ (¿ Bytes & Bytes)
split? φ = inp (♯ span φ) ⟫ π₂ {Bytes} ⟫ inp (♯ break φ) ⟫ inp (♯ nonempty)

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

⟫-resp-≃ : ∀ {S T U} {P₁ P₂ : S ⇒ T} {Q₁ Q₂ : T ⇒ U} → 
  (⟦ P₁ ⟧ ≃ ⟦ P₂ ⟧) → (⟦ Q₁ ⟧ ≃ ⟦ Q₂ ⟧) →
    (⟦ P₁ ⟫ Q₁ ⟧ ≃ ⟦ P₂ ⟫ Q₂ ⟧)
⟫-resp-≃ {S} {T} {U} {P₁} {P₂} {Q₁} {Q₂} P₁≃P₂ Q₁≃Q₂ as =
  begin
    ⟦ P₁ ⟫ Q₁ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ P₁≃P₂ Q₁≃Q₂ as ⟩
    (⟦ P₂ ⟧ ⟦⟫⟧ ⟦ Q₂ ⟧) as
  ≡⟨ sym (⟫-semantics P₂ Q₂ as) ⟩
    ⟦ P₂ ⟫ Q₂ ⟧ as
  ∎

Против кого вышел царь Рэкета? Кого ты преследуешь? Мёртвую Курочку!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Мне кажется, что преимущества F# над C# начинаются не в низкоуровневом парсинге, а где-то в районе высокоуровневых преобразований, где выводимые типы данных станут заметно сложнее. Так-то описания грамматики, подобные твоим, можно лепить и на сишных макросах — но это же не значит, что Си стал отличным языком для писания трансляторов? Ну и да, локальный вывод типов в C# играет не последнюю роль в упрощении писания кода.

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

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

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

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

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

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

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

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

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;
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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);

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

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

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

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

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

… 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())

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

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

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

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

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

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

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

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

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

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

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

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

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

И десять рогов, которые ты видел, суть десять Царей на контрактах, Which еще не получили царства, но примут власть со зверем, как Цари Рэкета по контракту, на один час.

data _⇒_ : (S T : Session) → Set₁ where
  inp : ∀ {T A V F} → ∞ ((a : A) → (♭ F a ⇒ T)) → (Σ V F ⇒ T)
  out : ∀ {S B W G} → (b : B) → (S ⇒ ♭ G b) → (S ⇒ Σ W G)
  done : ∀ {S} → (S ⇒ S)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Да.

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

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

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

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

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

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

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

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

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

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

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

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

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

Это весь UI

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

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

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