Как в Lisp передать функцию ссылку на объект?

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

Пусть он заставляет написать ветку if(total>x) ... Но что в этой ветке делать?

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

ты эта простветись чтоли о стандарте представления ieee плавающих чисел.

Статическая компиляция не избавит ото всех ошибок. Но от ошибок вида «ой, забыли tonumber()» она избавит точно.

Можно статически проверить (пусть в агде)?

postulate
  _div_ : (x y : ℕ) → ℕ
  -- ^ unsafe in y ≡ 0, maybe compiled to something with COMPILED* pragma

-- safe:
f : (x y : ℕ) {witness : x + y ≢ 0} → ℕ -- two explicit and one (dependent on first two) implicit argument
f x y = 1 div (x + y)

test₁ = f 1 2 { λ () } -- absurd witness (1 + 2 ≡ 0 is absurd, so that 1 + 2 ≢ 0)
-- d.t. = ℕ
-- n.f. = 1 div 3
-- type checked, compiled

test₂ = f 0 0 { {!!} } -- ?0 : 0 + 0 ≡ 0 → ⊥ proof required, how come?
-- d.t. = ℕ
-- n.f. = 1 div 0
-- but no way from the type checker

Да, должны быть какие-то фильтры — если парсер, например, читает число из строки (из IO, допустим), то он должен уметь предоставлять (just _или_ as is) число _и_ свидетель (witness) его свойств _или_ ничего (nothing _или_ исключение, если они есть).

Например:

read-from-io : IO String
parse-non-zero-nat-from-string : String → Maybe (Σ[ x ∈ ℕ ] x ≢ 0) -- dependent product, развитие идеи обычного кортежа

понятно, что теперь можно читать из IO, парсить положительное натуральное из строки в just, передавать из под just в f безопасно, возвращать nothing из парсера если в строке не то что нам нужно (и тогда в f уже нечего передавать).

Обычный парсер это вырожденный случай который возвращает число _и_ refl : x ≡ x в качестве канонического (и поэтому необязательного) свидетеля.

З.Ы. refl и, собственно, propositional equality / identity type-path:

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

такой тип можно (кое-как) написать и в хаскеле.

Если да, то что произойдёт при x = 10 и total = 1?

Опять же, не readInt а

readWhatYouWant :: IO (Maybe Double)

или, раз уж пошёл такой разговор

Probability = Σ[ p ∈ Double ] d 0 ≤ p × p ≤ d 1

readWhatYouWant : IO (Maybe Probability)

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

readWhatYouWant :: IO (Maybe Double) это, очевидно, хаскель — пусть возвращает Just дабл, где дабл _уже_ в нужных границах (алгоритм парсера всё узнаёт про свойства числа непосредственно при разборе строки), либо Nothing иначе. Остальное — агда.

А вообще, парсер ведь читает в формате [+|-]?\d+\.\d*, поэтому его лучшее представление это (знак : Bool, целая : Nat, дробная : Nat) + свойства числа выявленные во время разбора (как простейший Maybe или что-то более сложное как в агде), для probability — знак = +, целая = 0, дробная >= 0 или > 0 (если = 0.0 не нужно далее по control flow). Дальше можно сделать рациональное (знак * (целая + дробная / 10)) и его считать, либо грузить таки в SSE.

Maybe - это, конечно, хорошо, как и Either. Но почему-то с «особыми условиями» (conditions) получается обычно проще.

Но почему-то с «особыми условиями» (conditions) получается обычно проще.

if (x > 10 && x < 100)
    fun(x); // fun is partial and wants x to be in (10 .. 100)

«проблемы» тут две — fun может быть частичной, то есть падать, например, функция div такая, зато такие функции проще писать; другая проблема в пригодности этих самых conditions — тут всё держится на честном слове, вроде как в ветке if x находится в границах (10 .. 100), и, допустим, оно const, так что, вроде как, всё хорошо.

Maybe это полумера в решении данных проблем — во-первых, можно превратить частичную div :: Integer -> Integer -> Integer, которая бросает исключения, в тотальную div :: Integer -> Integer -> Maybe Integer без исключений, но можно ли сделать тотальную div :: Integer -> Integer -> Integer? Можно, если будет контекст из которого известно, что знаменатель не есть ноль, например, через implicit argument которым передаётся доказательство этого факта, которое должно быть traceable системой типов через весь control flow (то есть раскрашенный типами граф). Второй момент — Maybe никак не позволяет писать в conditional стиле, да, то есть, если мы взяли Maybe в результате, то нам условия на аргументы уже не нужны (функция тотальна), условия на аргументы нужны если функция частична и как-то ограничена на своём домене — она снова будет тотальной если типы сузить до точных, но для этого система типов должна быть выразительной, зависимые типы должны быть логическими утверждениями параметризованными другими логическими утверждениями, тогда conditions возможны как зависимый паттерн-матчинг с уже гарантированным предоставлением доказательств этих параметров в разных ветвях control flow.

В агде всё это решается тотальностью функций по умолчанию и с помощью with expression (зависимый паттерн-матчинг как обобщение обычного) + decidable predicates для conditional кода — написать разумный div : Integer → Integer → Integer просто не получится, нужен либо Maybe, либо явное или неявное доказательство (всё равно его нужно будет передавать, так что не важно, просто по идее это может быть контекст с элементами автоматического поиска доказательств озвученных утверждений) про нужное утверждение, то есть параметризованный тип (: ... → Set), который уже можно использовать с decidable predicates техникой и with expression, например:

data _≤_ : ℕ → ℕ → Set where
  ...

_≤?_ : (x y : ℕ) → Dec (x ≤ y)
...

f : ℕ → ...
f n with n ≥? 5
... | yes proof = тут n гарантированно >= 5, так что его можно передать вторым аргументом div вместе с proof (которое тот div хочет получать)
... | no proof = тут обратно (и доказательство этого факта тоже в proof)

Из настоящего (в Set) предиката обычный «предикат» в булевый тип получается просто, например:

_<=_ : ℕ → ℕ → Bool
x <= y with x ≤? y ; ... | yes _ = true ; ... | no _ = false

Для местных (ко)индуктивных вещей, например, для чисел в форме zero : ℕ; suc : ℕ → ℕ, легко писать настоящие предикаты вроде _≤_ в форме relation type и _≤?_ как Decidable type/predicate для него, для инородных (примитивных) вещей с примитивами сравнения нужна некоторая магия, точнее, возможность принимать нечто на веру (вводить аксиомы), например, в агде финитные строки примитивны (не [Char] как в хаскеле — в агде это Costring), поэтому чтобы вывести настоящий предикат равенства из примитивного (постулируемого) _==_ : String → String → Bool нужно вводить аксиомы:

_≟_ : Decidable {A = String} _≡_
s₁ ≟ s₂ with s₁ == s₂
... | true  = yes trustMe -- тут
... | false = no whatever
  where postulate whatever : _ -- и тут

tl;dr

Короче, если функция действительно не должна принимать каких-то значений аргументов, то её сигнатуру можно оставить прежней добавив в неё только каких-то ограничивающих утверждений — дальше будет conditional (dependent pattern-matching) код _в_ эту функцию, и уже с гарантиями, что, да, в этой ветви вещи обладают ровно теми свойствами что хочет та функция и что мы просили — система типов знает про это. Но вот в случае парсера всё это не нужно, так как только он знает как отсеять ненужные String и разобрать нужные, поэтому просто принимает String и возвращает Either (привет, parsec) в результате, то есть _из_ — по нему уже идут условия при передаче его куда-либо. То есть, in / out — то (абзацами выше), либо другое (Maybe, etc.).

P.S. Видимо, именно «простота» тут — явно не цель :) С одной стороны, для простоты нужно брать какой-нибудь Python, с другой — когда в «простом» питоне начнётся структурная сложность, где будет его простота?

С одной стороны, для простоты нужно брать какой-нибудь Python, с другой — когда в «простом» питоне начнётся структурная сложность, где будет его простота?

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

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

Если перевести пример в привычный синтаксис

void fun(int x)
    requires (x > 10 && x < 100) // дополнение к сигнатуре
{
    ...
}

void test()
{
    int x;

    ...

    if (x > 9 && x < 100) {
        // тут у x уже известный подтип типа int -- (9 .. 100)
        fun(x); // который не есть подтип (10 .. 100), так что не скомпилируется
    }

}

С++ concepts, axioms, static if — не совсем, но туда же.

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

Я знаю — но никто не мешает написать такую агду, какую нужно :) И если нужно.

Кстати, все, описанное тобой на агде, легко делается в любом статическом и динамическом ЯП

anonymous уже говорил мне об этом, всё свелось к тому, что оно «компилируетсо!1» (забыл добавить ", сцуко, японская девочка").

Все описанные вещи не связаны с системой типов, они связаны с модульностью.

Система типов это синтаксический (читай, раннего действия) фреймворк выявления корректности (как-то так, (с) TAPL).

То, что ты пишешь на агде, отвечая на мое сообщение, выглядит безусловно интересным, но проблема в том, что я не знаю этого языка и, честно говоря, не знаю, нафига он мне нужен. Это как некоторые не знают, зачем им нужны лисп, хаскель, си++, ява, или питон. Да, парадокс Блаба :)

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

Кстати, агда это proof assistant, то есть нужна она для формальных рассуждений про формальные математические модели математикам, просто она основана на теории типов, поэтому там есть те же лямбда-термы и их нормальные формы, может быть вычислитель и компиляция — если моделями становятся переменные, конкурентность или система эффектов, то можно расширить тот компилятор чтобы он подбирал вещи из моделей, превращая их во что-то подходящее в своём бакенде, так что агда становится ЯП общего назначения. К тому же, подмножество Agda2 очень похоже на хаскель. Но использовать в том качестве в котором используются лисп, хаскель, си++, ява, или питон её (сейчас) явно нельзя — простейший аргумент в том, что с malonzo бакендом в стандартном модуле IO течёт память, а альтернативный agda-system-io просто не собирается :) (хотя, github.com/larrytheliquid/Lemmachine, но там всю работу делает хаскель).

Я знаю — но никто не мешает написать такую агду, какую нужно :)

Это голословное утверждение. Никто не доказал, что такую агду написать _можно_ :)

Система типов это синтаксический (читай, раннего действия) фреймворк выявления корректности (как-то так, (с) TAPL).

Тут ситуация простая - вот апологеты статики кричат об ошибках, которые статика исправляет, а динамика - нет, но практика показывает, что эти ошибки в динамике не становятся проблемой. Вопрос - почему? Ответ - да просто в динамике архитектура приложение изначально строится так, чтобы было невозможно (или чрезвычайно сложно, через work around'ы типа unsafePerformIO) допускать ошибки определенного класса. То есть те ошибки, что статика находит, программист на динамической ЯП просто не допускает.

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

Никто не доказал, что такую агду написать _можно_ :)

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

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

Метрика тут ранние (статические) / поздние (динамические) assert-ы / контракты. Если всё сдвигать в сторону динамических, то это требует обязательного тегирования всех объектов (хотя всё больше реализаций языков и так это делают, но не все), а возникновение самих коллизий растягивается на неопределённое время. Сдвиг всего в сторону статики, наоборот, нетривиален (смотрим на теории типов от Рассела и до сего дня).

Круто! У меня была идея добавить статические контракты для pure C(или подмножестве), но я так до ума даже идею не довел. Ты не подскажешь, куда копать? Меня еще волнует вопрос, не много ли контрактов придется писать? Насколько получится отловить все варианты, чтобы корректно определять контексты?

Благодарю за разъяснения.

Метрика тут ранние (статические) / поздние (динамические) assert-ы / контракты.

Еще раз - там, где программист на статике пишет портянку в надежде, что компилятор даст ему ошибку, программист на статике пишет код, в котором этой ошибки просто _не может быть_ by design. Соответственно, и ловить ничего не надо - потому что нечего. Можно так сказать, что ошибка в динамике отлавливается на стадии проектирования, до рантайма, до компиляции и вообще до написания кода :)

Если всё сдвигать в сторону динамических, то это требует обязательного тегирования всех объектов

Тестирование логики _всегда_ требуется, вне зависимости от того, статика у тебя или динамика.

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

Да.

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

Меня еще волнует вопрос, не много ли контрактов придется писать? Насколько получится отловить все варианты, чтобы корректно определять контексты?

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

Еще раз - там, где программист на статике пишет портянку в надежде, что компилятор даст ему ошибку, программист на статике

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

Ты не подскажешь, куда копать?

Именно для Си в Inria делаются Frama-C (Jessie — http://www.lri.fr/~marche/moy09phd.pdf) и CompCert. Но там (во Frama-C) программы на Си отдельно, спецификации — отдельно в комментариях (что хорошо), так что это несколько отличается от зависимых типов в которых спецификации это просто типы, а программы — уже их доказательства, в примере который я написал есть какой-то сахар, но с точки зрения языка с зависимыми типами это _уже_ полностью (не)валидная программа, а её (не)валидность (тот факт что программы-доказательства действительно (не)доказывают свои типы-утверждения) проверяется тем же тайпчекером (его fail-ом). То есть в одном случае это внешние средства для обычного языка Си — они существуют, в другом — сам язык должен проектироваться так, чтобы его вещи могли за собой следить, как это в Coq или Agda, которые, конечно, далеко не Си — максимум предполагают code extraction куда-нибудь (в OCaml, Haskell или JS, например). Вот, но CompCert написан в большей степени на Coq, нежели на OCaml — code extraction может быть вполне неплох.

Меня еще волнует вопрос, не много ли контрактов придется писать?

Контракты ведь опциональны, их можно не писать — тогда это будет обычный частичный код. Если их где-то писать, то, да, может быть сложно — в том же Frama-C потом нужно будет перепоручить доказательство автоматическому пруверу и если он не справится, то писать самому на Coq — http://toccata.lri.fr/gallery/MyCosineACSL.en.html.

Насколько получится отловить все варианты, чтобы корректно определять контексты?

Если брать приведённый пример, то это адаптация такого кода на агде:

infix 3 _and_ ; _and_ = _×_
infix 3 _&&_ ; _&&_ = _×-dec_

f : (n : ℕ) {_ : 10 ≤ n and n ≤ 100} → ℕ
f n = n ∸ 10

t₁ : ℕ → ℕ
t₁ n with 10 ≤? n && n ≤? 100 ; ... | yes p = f n {p} ; ... | _ = {!!}

t₂ : ℕ → ℕ
t₂ n with 9 ≤? n && n ≤? 100 ; ... | yes p = f n {p} ; ... | _ = {!!}
-- ^ 9 != 10 of type ℕ
--   when checking that the expression p has type 10 ≤ n × n ≤ 100

t₃ : ℕ → ℕ
t₃ n with 10 ≤? && n ≤? 100 ; ... | yes p = f (n + 1) {p} ; ... | _ = {!!}
-- ^ n != n + 1 of type ℕ
--   when checking that the expression p has type 10 ≤ n + 1 × n + 1 ≤ 100

то есть

nat f(nat n, and<less_equal<10, n>, less_equal<n, 100>> proof)
    // ^ Тут and<less_equal<10, n>, less_equal<n, 100>> это тип зависимый от
    //   первого значения n, я использую синтаксис шаблонов C++, proof это
    //   значение этого типа представляющее собой любое доказательство данного
    //   факта про n.
    //
    //   То есть второе утверждение связано (зависит от) с первым значением --
    //   нельзя передать значение одно, а доказательство -- про другое.
    //
    //   А requires с более наглядным синтаксисом это уже сахар.
{
    return n - 10;
}

nat t1(nat n)
{
    switch (10 <= n && n <= 100) {
    // ^ if -- частный случай switch, тут switch более общего вида, по любым
    //   паттернам с любыми конструкторами:
        case yes { proof } : return f(n, proof);
        // ^ then ветвь, передаём свидетеля свойств (proof) явно вместе с его
        //   значением (n).
        case no { proof } : ...;
        // ^ else ветвь, тут proof свидетельствует что n не лежит в [10 .. 100]
    }
}

не вдаваясь в рассказ про то по чему именно switch тут осуществляет матчинг — в данном случае (формы if и switch) каждый case вводит доказательство свойств связанное с n, поэтому всегда возможна неявная передача в виде

switch (10 <= n && n <= 100) {
    case yes : f(n); // в текущем контексте с n связано свойство которое хочет f

и

if (10 <= n && n <= 100) {
    f(n); // и тут

Так в агде с переходом от implicit к instance arguments можно передавать простые доказательства неявно из глобального или локального контекста:

f : (n : ℕ) ⦃ _ : 10 ≤ n and n ≤ 100 ⦄ → ℕ
f n = n ∸ 10

t₁ : ℕ → ℕ
t₁ n with 10 ≤? n && n ≤? 100 ; ... | yes _ = f n ; ... | _ = {!!}

t₂ : ℕ → ℕ
t₂ n with 9 ≤? n && n ≤? 100 ; ... | yes _ = f n ; ... | _ = {!!}
-- ^ No variable of type Σ (10 ≤ n) (λ x → n ≤ 100) was found in scope.
--   when checking that n are valid arguments to a function of type (n₁ : ℕ) → {{10 ≤ n₁ × n₁ ≤ 100}} → ℕ

t₃ : ℕ → ℕ
t₃ n with 10 ≤? n && n ≤? 100 ; ... | yes _ = f (n + 1) ; ... | _ = {!!}
-- ^ No variable of type Σ (10 ≤ n + 1) (λ x → n + 1 ≤ 100) was found in scope.
--   when checking that (n + 1) are valid arguments to a function of type (n₁ : ℕ) → {{10 ≤ n₁ × n₁ ≤ 100}} → ℕ

другие случаи нужно отдельно смотреть.

Ещё, если идти от теории типов, с автоматическим поиском есть проблемы преобразования доказательств, например:

if (11 <= n && n <= 99) {
    f(n);

код хороший, но нужно преобразование из типа 9 ≤ n && n ≤ 99 в тип 10 ≤ n && n ≤ 100 — если передавать вручную, то его можно сделать вручную, точно так же m == n и n == m это разные вещи — поиск в контексте должен осуществляться с учётом множества теорем про разные типы — equality/isomorphism, subtyping relation и т.п.

З.Ы. в контексте математики с её аксиомами и теоремами доказательство FLT это тоже такой поиск в контексте, на тему того когда подобный поиск вообще возможен — http://en.wikipedia.org/wiki/Decidability_(logic)#Some_decidable_theories и ниже. У автоматических пруверов логика обычно ограничена первым порядком а процесс поиска доказательств semidecidable (так что по таймаутам запускается).

Да.

А чем системы вершины лямбда куба принципиально отличаются от обычной полиморфной лямбды (которая в такие системы ещё и встраивается бесшовно)?

И опять же. Пусть он заставляет написать ветку if(total>x) ... Но что в этой ветке делать? Никакого разумного значения вероятности дать нельзя. Надо бросать исключение или использовать какой-то другой механизм, позволяющий или запустить отладчик или сообщить пользователю, что «при чтении файла ... в строке ... встретились неверные данные: ...».

when придумали трусы? Either/Maybe придумали идиоты?

ну и какая мне польза от статической типизации, если ошибка ввода рушит программу и компилятор никак не предупреждает, что эта ситуация необработана (в Java хоть throw заставляют описать)?

тебе - никакой, т.к. ты в языке разбираться не собираешься.

import Control.Applitive
import Safe

main = do
  x <- readMay "parse error <$> getLine
  case x of
    Left a -> putStrLn $ "error: " + a
    Right x -> print (x+1)

на тему того когда подобный поиск вообще возможен

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

а процесс поиска доказательств semidecidable

Ну любая полная теория semideciable обычным перебором по длине вывода. Это только ничего не дает полезного.

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

Например, они неразрешимы?

when придумали трусы? Either/Maybe придумали идиоты?

Исключения - это и есть Either/Maybe, но встроенные в ядро языка и имеющие стандартизированный протокол, в отличии от. Ручное применение Either/Maybe - это вообще говоря кривой костыль и применять его надо как можно меньше, лучше кидать исключения там, где можно.

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

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

Для теории типов — честно говоря и не нужно, не считая простейших случаев ради чисто синтаксических удобств (они особых накладок не дают). Это как с выводом типов :)

Это только ничего не дает полезного.

Есть множество semideciable автоматических пруверов для FOL которые вполне полезны.

Например, они неразрешимы?

Речь про intensional type theory / CIC. Ну и не обязательно чтобы все рекурсивные функции можно было использовать из тайпчекера — потенциально незавершимым функциям и IO явно нечего делать в type expressions.

Исключения - это и есть Either/Maybe

throw :: Exception e => e -> a

Throw an exception. Exceptions may be thrown from purely functional code, but may only be caught within the IO monad.

Хаскель-проблемы?

Ручное применение Either/Maybe - это вообще говоря кривой костыль и применять его надо как можно меньше, лучше кидать исключения там, где можно.

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

Хаскель-проблемы?

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

тебе - никакой, т.к. ты в языке разбираться не собираешься.

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

Хаскель-проблемы?

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

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

Любой код с исключениями изоморфен коду с Either, один к другому приводится простейшей трансформацией и они совпадают по семантике. Но преимущества исключений следующие:

1. не мусорится тип (то есть если мы выкинули в ф-и исключение или обрабатываем его, не надо перепидорашивать тип)

2. немного синтаксического сахара

2. с Either придется городить монадическую лапшу в do, с исключениями - нинужно (если они нормальные), можно писать обычный код (де-факто все внутри try-блока поднимается в Either-монаду автоматически, в этом основной плюс исключений).

3. Обеспечивается стандартный протокол, при помощи которого указывается точный тип исключения, матчинг по нему и т.п., с Either - пидорасим руками.

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

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

Еще раз - исключения _полностью_ эквивалентны Either. Это синтаксический сахар над Either (автомутическое поднятие в монаду) + стандартизированный протокол его использования. Спрашивая о семантике исключений, ты спрашиваешь о семантике Either.

Так я могу и на лиспе писать.

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

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

Твоя программа некорректна? Если ты используешь небезопасные нетотальные функции из Prelude, то ты сам себе злой буратино. То, что в haskell есть нетотальные функции (преимущественно для скорости работы) это не минус.

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

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

То, что в haskell есть нетотальные функции (преимущественно для скорости работы) это не минус.

Погоди, то есть использование тотальных ф-й мою производительность как программиста не повысит (раз для скорости работы надо применять нетотальные)? Ну и нахуй оно нужно тогда?

В лучших традициях сишных сегфолтов. Успешной отладки.

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

orly? хочу видеть асинхронный Either! И наверное мы говорим только о случае использования Maybe/Ether/исключений для уведомления об ошибках, иначе это просто смешно. Исключения эквиватентны Ether только там где последовательность вычислений детерминировано (поскольоку в haskell это монады), т.е. в Either[T] монаде, там - да. Однако Either может использоваться и в чистых вычислениях, ну и нести дополнительную смысловую нагрузку.

1. не мусорится тип (то есть если мы выкинули в ф-и исключение или обрабатываем его, не надо перепидорашивать тип)

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

2. немного синтаксического сахара

errors и тот же сахар

В целом исключения это круто, но утверждение, что их надо использовать когда только можно вместо Either/Maybe, нужно понимать, что «когда только можно» это не очень часто :)

Исключения эквиватентны Ether только там где последовательность вычислений детерминировано (поскольоку в haskell это монады), т.е. в Either[T] монаде, там - да.

Ну а как еще ты Either можешь использовать? Только в монаде. А try-блок - это просто указание компилятору автоматически поднять в монаду все внутренние вычисления.

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

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

В целом исключения это круто, но утверждение, что их надо использовать когда только можно вместо Either/Maybe, нужно понимать, что «когда только можно» это не очень часто :)

Да вобщем-то всегда, когда используется Either/Maybe как монада (то есть выполняется композиция операций) надо заменять это на исключения. То есть практически всегда :)

Ну а как еще ты Either можешь использовать?

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

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

ну пока так не сделано (не знаю к сожалению или нет), даже в haddock не все описывают, вот это точно к сожалению.

Да вобщем-то всегда, когда используется Either/Maybe как монада (то есть выполняется композиция операций) надо заменять это на исключения. То есть практически всегда :)

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

везде, а что?

Что значит «везде»? Ты если используешь Either - значит ты поднялся в соответствующую монаду, то есть не поднимаясь в монаду ты его использовать не можешь.

ну пока так не сделано (не знаю к сожалению или нет), даже в haddock не все описывают, вот это точно к сожалению.

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

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

Почему, нет. Результат должен быть Either, а не IO (конец try-блока).

а вот с исключениями придется делать catches при этом в монадическом исключении.

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

Что значит «везде»? Ты если используешь Either - значит ты поднялся в соответствующую монаду, то есть не поднимаясь в монаду ты его использовать не можешь.

Похоже тут вопрос определений.. Если я сделаю:

data E a b = L a | R b

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

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

по остальному ок.

он изоморфен Either, монаду не образует, во всяком случае инстансов нет.

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

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

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

isException :: a -> Bool
isException !x = ?

pureCatch :: a -> a -> a
pureCatch x y = if isException x then y else x

isException' :: NFData a => a -> Bool
isException' !!x = ?

pureCatch' :: NFData a => a -> a -> a
pureCatch' x y = if isException' x then y else x

не мусорится тип

А нужно.

у вас где-то что-то упало, но неизвестно где и что

Ничего не упало. Для примера — Maybe Config -> ..., Maybe BackendConnection -> ..., Either LocalCache RemoteCache -> ..., это же самое внутри структур в data, ... -> Either Int Double, ... -> Either ParserResult ParserError.

Только в последнем случае можно променять Either на исключение, но не нужно — ни в хаскеле (так как это сразу заставит клиента окунаться в IO), ни где-то ещё — return codes и exceptions это две разные вещи, одно локально и должно работать ровно на стыке двух функций, другое — может работать нелокально через весь стек вызовов разных функций.

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

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