История изменений

Но почему-то с «особыми условиями» (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, с другой — когда в «простом» питоне начнётся структурная сложность, где будет его простота?

Но почему-то с «особыми условиями» (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, с другой — когда в «простом» питоне начнётся структурная сложность, где будет его простота?