допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9 - "Но ведь это одно и то же!". а вы, будучи подкованы в современных веяниях науки, отвечаете так: "Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории"

в теории типов у нас есть базовые суждения:

• "нечто является типом A"
• "нечто является термом a"
• "такой-то терм a имеет такой-то тип A" ( a : A )

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

• "если A тип и В тип, то A -> B тоже тип"
• "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В"

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

и вот тут первый ключевой момент

если у нас есть терм

         mul : Nat -> Nat -> Nat 

         mul 9 2 : Nat 

и терм mul 2 9 тоже имеет тип Nat, но и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы.

а еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны: они "равны". что это значит?

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

• если есть конструирование натуральных чисел, есть и их элиминатор, рекурсор
• если есть создание пары (,), есть и разбирающие ее на части fst и snd
• если есть конструирование списка cons, есть и его разбор на части, head и tail

и вот эти элиминаторы (fst snd head tail etc.) обычно сопровождаются суждениями о равенстве термов. мы не только говорим, что ежели р : (А , В) то fst p : A, но сопровождаем правилом:

         fst (a , b) = a 

именно тут появляется равенство по определению, definitional equality . именно оно позволяет утверждать, что fst (18 , 3) = 18, именно благодаря ему и именно в этом смысле мы говорим, что термы fst (18 , 3) и 18 равны

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

получается такая картина, что в том же типе Nat у нас куча разнообразных термов, и некоторые из них связаны между собой равенствами. связанные термы образуют направленные графы (с т.з. вычислений definitional equality связывает термы в определенном направлении - что во что вычисляется). если мы не успели наделать в теории глупостей (вроде некоторых вредных аксиом), то каждый такой граф будет сходиться в одной точке, канонической форме. это хорошее свойство, оно позволяет компилятору без труда убедиться, что термы mul 2 9, mul 9 2 и fst (18, 'x') равны по определению, достаточно каждый из них вычислить, пробежавшись по графу до канонической формы, и убедиться, что получился тот же терм (с точностью до переименования переменных - если они в нем есть)

более того, компилятор даже понимает, что 0 + x = x, но вот что x + 0 = x он уже не понимает, термы x + 0 и x не definitionally equal, не равны в этом смысле, их не связывает путь в том графе. потому что сложение у нас определено матчингом по первому аргументу; когда первый аргумент Z или S n , у нас есть какие-то равенства на этот счет, но когда первый аргумент - переменная: все, приехали. тем более выражения x * y и y * x не равны definitionally. "Но ведь это одно и то же!"

чтобы выразить эту однуитужесть, придумали propositional equality

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

так вот, мы можем выразить утверждение "x = y" в виде типа, так называемого identity type. терм такого типа будет доказательством, конструктивным обоснованием почему x = y

однако если мы возьмем две функции

f : Nat -> Nat
f x = 2 * x

g : Nat -> Nat
g x = x * 2

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

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

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

можно его просто в явном виде ввести как аксиому

можно пойти чуть в обход и, аксиоматизировав uniqueness of identity proofs (UIP), сделать теорию типов экстенсиональной, там function extensionality уже выводится.

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

однако есть и другой способ получить function extensionality, не постулируя ее и сохраняя теорию интенсиональной - гомотопическая теория типов (HoTT)

- папа, ты сейчас с кем разговаривал?

кстати говоря, учителка ругается не на (*) : Nat -> Nat -> Nat, а на (*) : Foo Nat -> Bar Nat -> FooBar Nat
девять женщин по две сумки у каждой - это не то же самое, что две женщины по девять сумок. в первом случае - шопинг, во втором - безумный шопинг

согласен - 2 мужика * 9 литров водки != 9 мужиков * 2 литра :)
однако как быть с выражением:
2 мужика * 9 литров == 9 литров * 2 мужика

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

...но при этом совершенно спокойно (*) : Bar Nat -> Foo Nat -> FooBar Nat

там было не столько 9*2, сколько 9*2.0
что не то же самое 9.0*2 или 2.0*9
с точки зрения классической нотации верен как раз зачёркнутый вариант
операция "*" здесь может означать не умножение в алгебраической структуре, а "лексический макрос" для многократного суммирования. у нас в кольце может быть своё умножение ×, или вообще у нас просто аддитивная группа без всяких умножений
запись n*x всё равно будет иметь смысл (здесь n натуральное, а x элемент структуры) как сокращалка для x + x + ... n раз (а именно так, возможно, в школе и рассматривается "умножение")
а запись x*n подобного общепринятого в алгебре смысла не имеет

или даже в некотором контексте 9*2 может вообще озанчать умножение скаляра 9 на вектор 2

* * *

программирование типов с помощью функций называется Church encoding. Haskell:

    {-# LANGUAGE RankNTypes #-}

    type Product a b = forall c. (a -> b -> c) -> c

    pair :: a -> b -> Product a b
    pair a b = \destruct -> destruct a b

    fst :: Product a b -> a
    fst p = p $ \a b -> a

    snd :: Product a b -> b
    snd p = p $ \a b -> b

    type Sum a b = forall c. (a -> c) -> (b -> c) -> c

    inl :: a -> Sum a b
    inl a = \l r -> l a

    inr :: b -> Sum a b
    inr b = \l r -> r b

    type Boolean = forall a. a -> a -> a

    true  = \a _ -> a
    false = \_ b -> b
    test b t e = b t e

    type List a = forall b. (a -> b -> b) -> b -> b

    nil = \ _ nil -> nil
    cons x xs = \ cons nil -> x `cons` xs cons nil
    foldr lst cons nil = lst cons nil

для арифметики на лямбдах задействуем числа Черча: число k представляется функцией, которая берет другую функцию и ее аргумент, и применяет ту функцию n раз. так, единица применяет данную функцию f один раз:

         one f x = f x 

чтобы увеличить n на 1, нужно применить f на один раз больше, чем это делает n:

         inc n f x = f (n f x) 

умножение a на b делается применением b a раз:

         mul a b f x = a (b f) x 

* * *

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

произведение обычное: a × b (первое и второе)
обобщение: a₁ × ... × aₙ (для индекса есть значение)
зависимое произведение: ∏ a P (ты ему индекс (i : a), а он тебе результат - P i)

сумма обычная: a + b (одно или другое)
обобщение: a₁ + ... + aₙ (индекс и какое-то значение)
зависимая сумма: ∑ a P (ты ему индекс (i : a), а он тебе значение - P i)

о, можно ещё так попробовать:

зависимый тип B : A → Type - это на самом деле семейство типов. так вот, "произведение ∏" и "сумма ∑" - имеются в виду произведение и сумма всех типов данного семейства

тогда, элемент типа ∏(x : A) B(x) - это кортеж из A значений типов семейства B, по одному B(x) на каждое x:A - декартово произведение B(x) для всех x:A

эквивалентно выражается в виде проекций кортежа для каждого индекса x:A - функция

  πi : (xi : A) → B x  

тогда, элемент типа ∑(x : A) B(x) - это элемент disjoint union значений типов семейства B. если вспомнить, как пишется disjoint union (∏ вверх ногами, ∐) и как он определяется (как тупль из значения и индекса, указывающего, из какого множества семейства значение взято), то это и есть сигма, ∑. disjoint union иногда так и записывают, через ∑, а не ∐

грубо говоря, для простого union достаточно было бы указать значение типа B(x) для некоторого x:A, а для disjoint union нужно ещё указать и само x:A, индексирующее тип из семейства B - "номер" инъекции, индекс конструктора. так что, это сумма в том же смысле, в каком disjoint union можно было бы назвать суммой множеств

* * *

у всех функций вроде

  head    :: [a] -> a
  tail    :: [a] -> [a]
  reverse :: [a] -> [a]
  concat  :: [[a]] -> [a]
  return  :: a -> [a]

все полиморфные функции, вроде head и tail для списков, fst и snd для туплов, - это естественные преобразования. они работают с формой структуры данных, не трогая ее наполнение, не зная конкретного его типа, т.е. превращают один функтор в другой

как head отображает пустой список в a? как вот такие вот не-тотальные функции вообще "переводят" в стрелки?

а откуда head возьмет пустой список?

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

функтор списка отображает типы в списки элементов этих типов путем создания одноэлементных списков. head производит обратную операцию - из одноэлементного списка достает значение. функтор не отображает что-то путём создания одноэлементных списков. он не ставит в соответствие точкам X точки F(X). этим занимается естесвенное преобразование - которое не всем точкам F(X) что-то находит в X

откуда берутся более длинные списки? функтор просто отображает алгебраическую структуру: "этот тип ведёт себя точно так же, как тип в другой категории". т.е. даже если бы мы могли поставить в соответствие точкам X какие-то точки F(X), алгебра над типом X будет выполняться для всех точек F(X). так что, пустой список в образе [a] существует

другое дело, что в Хаскеле foreach A, A = A + 0, т.е. другими словами, ⊥ = 0 является в Хаскеле частью любого типа. так что, head на самом деле может отобразить [] в ⊥=0 , что он с успехом и делает, бросая при этом исключение, каковое мы и видим

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

ну вот возьмем натуральные числа в качестве объектов

если мы скажем, что стрелка соединяет А и В, когда А >= B, то все отлично, это годная категория (и id там есть A >= A). но вот если мы скажем, что стрелка соединяет А и В, когда А > В, то это хоть и будет похоже на категорию, но id там не будет. и просто так "добавить морфизм объекта в самого себя и заявить" не получится, ведь это будет означать, что мы постулируем А > А

* * *

полиморфизм:                    разные типы, один интерфейс
ad-hoc полиморфизм:             разные типы, один интерфейс, разные реализации
параметрический полиморфизм:    разные типы, один интерфейс, одна реализация

в Haskell есть все три вида полиморфизма (параметрический, статический/compile-time ad-hoc и динамический/run-time ad-hoc), а в плюсах - только два ad-hoc-а

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

> если типов нет в языке, это не значит, что их нет вообще
и откуда тогда В ЯЗЫКЕ возьмутся полиморфные типы?

> таким образом, генерик-функция работает фактически с одним типом - void* с пришпиленными таблицами , по которым процессор может найти нужные ООП функции
это всё - исключительно детали реализации, которые никого не волнуют. вопрос не в том, что там происходит в бинарнике, вопрос в том, какие возможности у ЯЗЫКА

* * *

при всей своей эклектичности С++ обладает одной из самых развитых систем типов. C++ это язык с полиморфной системой типов порядка выше 1. темплейты могут быть параметрами темплейтов. Scala - точно нет. Agda - не поручусь - но вроде тоже нет

подождите, что-то мне подсказывает, чт.е. языки с порядком полиморфизма в бесконечности ;)

есть конечно - Haskell тому пример. дурное дело нехитрое :)

Agda2 - точно да

а где в Агде типы высших порядков? мне казалось, там фактически ML + dependent types

ML и зависимые типы - в ATS, a в Agda2 - Haskell и зависимые типы
поскольку в Агде есть конструкторы типов, есть и типы высших порядков:

    data Ha f where Se :: f a -> Ha f  

да, круто, не знал про это. спасиб

>> темплейты - это макросы на стероидах

какая связь?

темплейт - тип

нет

да, хоть и станный

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

 template<template<class>,int> class  

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

в чём проблема? "литерал '1' языка C не является типом, но сам язык C типизирован"
> если шаблон является значением некоторого типа - то значит существует этот самый "некоторый" тип шаблона
конечно, и я даже привёл пример (а вы его процитировали). шаблон имеет тип
только
1) не надо говорить, что шаблон ЯВЛЯЕТСЯ типом - не является; и
2) не надо путать эти типы с такими типами как int или какой-нибудь MyClass - они живут в разных системах типов

то что вы называете "типом шаблона" - это в точности то, что в Haskell называется kind. а сами шаблоны таки и есть типы

ну по такой логике и Haskell - не один язык, а два: типовых систем там точно две - по тем же причинам, что и в С++. и если спецификации параметров классов - это точный аналог haskell-ых kind's - то собственно темплейты - это как раз параметрический полиморфизм и есть и пока речь не заходит о предикатах - аналог точный (только обязтельна явная квантификация):

     template <typename [...] a , >
     template <typename a , typename b> a apply (a x , b f (a)) { return f (x) ; }

     let apply : 'a 'b . 'a -> ('a -> 'b ) -> 'b = fun x f -> f x

ну как это нету - когда они и есть. причем практически haskell-style. собственно отображение почти 1 в 1 за исключением двух пунктов:
1) малосущественный - приняты другие решения на тему разрешения конфликтов при перегрузке (хотя по haskell эти варианты тоже обсуждались и что-то даже у ghc как extensions есть)
2) существенный - отсутствие явных предикатов. что несколько увеличивает вероятность конфликтов. в принципе - концепты, которые было хотели в стандарт добавить, но забоялись - оно и есть

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

> в чём проблема? "Литерал '1' языка C не является типом, но сам язык C типизирован".
если литерал 1 принадлежит к какому-то типу - то значит существует такая вещь, как "тип '1'"
про шаблоны Вы утверждали обратное

> про шаблоны Вы утверждали обратное
лжёте

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

> только 1) не надо говорить, что шаблон ЯВЛЯЕТСЯ типом - не является; и 2) не надо путать эти типы с такими типами как int или какой-нибудь MyClass - они живут в разных системах типов

ага, значиццо так. в Си (и С++) существуют примитивные типы, производные типы "первого порядка" - struct, union, указатель и массив и (только в C++) - class ну и enum в какой-то степени

эти типы существуют в отдельном пространстве от примитивных типов - более того, в Си у них даже пространство имён разное. (В C++ вроде тоже, хотя я и не проверял)

шаблоны существуют в ещё одном "отдельном" пространстве, отделённом от предыдущих типов

в чём проблемы?

> да, я знаю, что здесь наличествует некоторая "нечёткость" естественного языка - но, с другой стороны - я не вижу, почему дальнейшее уточнение не является схооластикой
я не понимаю, как уточнение нечёткости (которая есть) может оказаться схоластикой

> шаблоны существуют в ещё одном "отдельном" пространстве, отделённом от предыдущих типов
в каком языке?
в языке шаблонов сами шаблоны являются не типами, а значениями
а всякие int, struct, enum, etc. - вообще литералами
в языке "С++ без шаблонов", который из него получается, шаблонов просто нет

> в чём проблемы?
в вашем утверждении, что "шаблон - это тип". шаблон - ровно настолько же тип, насколько строка "число 146" является типом

а код на C++ полностью разворачивается и генерирует код на Си без классов и прочих плюсовых заморочек

это вы про семантику или про реализацию? семантика C++ определена не в терминах трансляции в C. реализация - ну, может, та, которой вы пользуетесь, и переводит в C, не знаю. в принципе, такие были. переходите на современную

а что, семантика шаблонов в этом смысле радикально отличается?

от чего? от семантики остального C++? да, радикально. семантика шаблонов - то, какой C++-код они порождают

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

* * *

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

• берём конкретный монадический тип (1 … M)
• берём функцию из Control.Monad (1 … N)
• смотрим, что означает применение выбранной функции на выбранном типе

если действительно хотим разобраться - проходим полностью этот двойной цикл

пример: возьмём пару функций и несколько монад

List: у нас есть готовая функция, возвращающая все списки заданной длины, состоящие из заданных элементов:

Maybe: нам не надо писать функцию, преобразующую список опциональных значений в опцию списка этих значений

(кстати, можно и наоборот)

тот же sequence для State вернёт список всех промежуточных значений

replicateM для State изменит состояние заданное число раз

replicateM в общем-то бесполезен для функций, но sequence позволяет применить один аргумент сразу к нескольким функциям и вернуть результат в виде списка

и т.д.

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

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

когда я вижу у себя m >>= \x → return (f x) я переписываю это в f <$> m не задумываясь о том, в какой именно монаде я сейчас нахожусь. это тоже шире монад и касается вообще всех алгебраических структур. для монад же мы имеем ещё и то, что для них бесплатны также функции, работающие для функторов и аппликативных функторов. халява, сэр!

  a -> m b
  m a -> b
  m a -> m b
  m (a -> b)

чтобы сполна прочувствовать всю эту историю с монадами, это надо на Хаскеле писать, и много. можно еще на Идрисе, но там своя атмосфера. а для начала можно на Elm'e что-то поделать, там и несложно, и результат наглядный, и даже для пользы можно сразу применить. в процессе вкус к pure FP впитатется. в Elm все то, за что большевики сейчас так любят React, сделано просто образцово

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

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

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

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

с выводом типов там правда фигово, но помогает the - пишешь the Int $ n `mod` 2 и уже не надо лишнюю строчку тратить

* * *

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

template <typename T>
struct cons
{
    T data;
    cons<T>* next;
} ;

template <typename T>
struct list
{
    cons<T> *list;
} ;

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

template <typename T>
struct boxed_list
{
    cons<void*> *list;
} ;

template <typename T>
struct pointer_list
{
    cons<T*> *list;
} ;

template <typename T>
struct vector_list
{
    std::vector<T> list;
} ;

Хаскель же добавляет свой зоопарк функциональных списков, в котором хаскельщики зачастую не разбираются сами, в основном из-за того, что стандартные списки [a] умеют мимикрировать под "классическую сишную структуру односвязного списка". интриги добавляет то, что в реальном коде они мимикрируют редко, так что дискуссия превращается в попеременное тыкание пальцем в небо всеми участниками

в первом приближении, есть

• настоящие списки, похожие на них свёртки и алгебры
• косписки и похожие на них развёртки и коалгебры

и всё это может быть сделано

• либо из данных (алгебраиками),
• либо из кода (кодировка Чёрча),
  • с явной рекурсией
  • или неявной

да на "людей" я и не надеюсь: даже научить их выбирать между foldl и foldr - тяжелейшая задача. я тут ищу методологические ошибки преподавания ленивости, из-за которых возникают глупейшие предложения типа "давайте сделаем всё на стримах". нужны хорошие контрпримеры против всех дебильных предложений отказа от ленивости

> в Хаскеле (да и в Окамле) нет традиции абстрагировать структуры данных или какие-то итераторы

а Data.Foldable - это что? шахматы? абстрагирование на каждом углу, как и итераторы

* * *

Строгость и нищета списков

Map и структурная рекурсия

Применить функцию к каждому элементу списка - это просто:

map _ []     = []
map f (x:xs) = f x : map f xs

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

Но есть одна проблема: в случае spine-strict списка такая функция не работает для хоть сколько-нибудь значительной длины списка. Строгость конструктора по второму аргументу преградила нам простой и естественный путь к цели. Что мы можем противопоставить этому вызову? И, (это, собственно, и является темой этого поста) что противопоставили этому авторы библиотек энергичных функциональных языков?

Игнорирование реальности

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

std-lib/list.ml

let rec map f = function
    [] -> []
  | a::l -> let r = f a in r :: map f l

Но это скучное решение. Наш рассказ о веселом:

Говоря о преимуществах ленивости обычно упоминают о модульности, возможности работы с бесконечными списками и обработки списков, занимая в каждый момент времени меньше памяти, чем занимает весь список. При этом как-то забывают, что даже если оставить за рамками обсуждения удобство использования списка как control-structure, то эффективная работа с обыкновенным конечным списком является в энергичных языках нетривиальной проблемой, которая, забегая вперед, для иммутабельных списков и не решается вовсе. Для иллюстрации проблем мы приведем реализации функций map в разных библиотеках и на разных языках, объединенных одним свойством - энергичностью по-умолчанию. Нужно заметить, что проблемы эти касаются не только map, но и любых других функций для работы со списками за исключением левой свертки и хорошо ложащихся на левую свертку (reverse, length, sum - почти полный их перечень).

Встречаем реальность с открытыми глазами

Авторы библиотек, поставляющихся с SML/NJ , постеснялись оставлять программиста наедине с холодным безразличием солипсизма. Они продемонстрировали теплоту и заботу, показали, что им не все равно:

init/pervasive.sml

fun map f = let
      fun m [] = []
        | m [a] = [f a]
        | m [a, b] = [f a, f b]
        | m [a, b, c] = [f a, f b, f c]
        | m [a, b, c, d] = [f a, f b, f c, f d]
        | m (a :: b :: c :: d :: r) = f a :: f b :: f c :: f d :: m r
      in m
      end 

Толку от этого, правда, мало. Имеющие более крепкое сцепление с реальностью идут другим путем.

CPS-преобразование

let map_cps f l' =
    let rec go l c =
        match l with
        | [] -> c []
        | (x::xs) -> go xs (fun xs' -> c (f x :: xs'))
    go l' (fun x -> x)

Двойной проход

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

basic/list.sml

fun revMap (l, f) = fold (l, [], fn (x, l) => f x :: l)

fun map (l, f) = rev (revMap (l, f)) 

rev_map есть и в библиотеке OCaml:

std-lib/list.ml

let rev_map f l =
  let rec rmap_f accu = function
    | [] -> accu
    | a::l -> rmap_f (f a :: accu) l
  in
  rmap_f [] l

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

Комбинированное решение из ocaml-core

core/lib/core_list.ml

let map_slow l ~f = List.rev (List.rev_map ~f l)

let rec count_map ~f l ctr =
  match l with
  | [] -> []
  | [x1] ->
    let f1 = f x1 in
    [f1]
  | [x1; x2] ->
    let f1 = f x1 in
    let f2 = f x2 in
    [f1; f2]
  | [x1; x2; x3] ->
    let f1 = f x1 in
    let f2 = f x2 in
    let f3 = f x3 in
    [f1; f2; f3]
  | [x1; x2; x3; x4] ->
    let f1 = f x1 in
    let f2 = f x2 in
    let f3 = f x3 in
    let f4 = f x4 in
    [f1; f2; f3; f4]
  | x1 :: x2 :: x3 :: x4 :: x5 :: tl ->
    let f1 = f x1 in
    let f2 = f x2 in
    let f3 = f x3 in
    let f4 = f x4 in
    let f5 = f x5 in
    f1 :: f2 :: f3 :: f4 :: f5 ::
      (if ctr > 1000
        then map_slow ~f tl
        else count_map ~f tl (ctr + 1))

let map l ~f = count_map ~f l 0

На этом этапе у нас есть важный результат - работающая функция map. Радоваться, впрочем, пока рано - такая реализация делает много лишней работы, а следовательно и работает медленно. Как можно с этим справиться? Ну, чтоб получить результат лучше, у списка нужно переписывать хвост. Просто так взять и сделать односвязный список мутабельным нежелательно. Мы ведь позиционируем его иммутабельность и персистентность как преимущество, верно? Так что мутабельность все-таки следует ограничить.

Волшебные функции.

Некоторые функции равнее других - они, например, находятся с определением списка в одной сборке и имеют доступ к его protected полю, как в F#:

  (* optimized mutation-based implementation.
  This code is only valid in fslib, where mutation of private
  tail cons cells is permitted in carefully written library code. *)

let inline setFreshConsTail cons t = cons.(::).1 <- t
let inline freshConsNoTail h = h :: (# "ldnull" : 'T list #)

let rec mapToFreshConsTail cons f x =
    match x with
    | [] ->
        setFreshConsTail cons [];
    | (h::t) ->
        let cons2 = freshConsNoTail (f h)
        setFreshConsTail cons cons2;
        mapToFreshConsTail cons2 f t

let map f x =
    match x with
    | [] -> []
    | [h] -> [f h]
    | (h::t) ->
        let cons = freshConsNoTail (f h)
        mapToFreshConsTail cons f t
        cons

Пример из этой же категории - list comprehensions в Nemerle, которые также переписывают хвост списка за кадром.

Отлично! Теперь у нас есть быстрый map и некоторые другие функции для работы со строгими списками. Но есть и проблемы. Дело в том, что такое решение требует поддержки от авторов стандартной библиотеки - стороннему программисту в этой парадигме писать быстрые функции не полагается - нужно довольствоваться тем, чт.е.. Предполагается, что всем необходимым избранные всех остальных обеспечат. На практике, разумеется, они этого не делают. Напоминаем также, что некоторые разработчики языков и библиотек не собираются обеспечивать вообще ничем. Что остается делать практичному программисту на языке, авторы которого находятся, скажем так, на противоположном конце спектра практичности? Ответ очевиден:

Хак-хак-хак!

Проблемы, не решаемые в рамках правил, часто можно решить выйдя за эти рамки. Так и поступили авторы "Батареек" - альтернативной стандартной библиотеки для OCaml. Нам нужен мутабельный список? Не вопрос, объявляем:

(* Thanks to Jacques Garrigue for suggesting the following structure *)

type 'a mut_list =  {
    hd: 'a;
    mutable tl: 'a list
}

Теперь можно писать изменяющий хвост map:

batList.ml

let map f = function
    | [] -> []
    | h :: t ->
        let rec loop dst = function
        | [] -> ()
        | h :: t ->
            let r = { hd = f h; tl = [] } in
            dst.tl <- inj r;
            loop r t
        in
        let r = { hd = f h; tl = [] } in
        loop r t;
        inj r

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

external inj : 'a mut_list -> 'a list = "%identity"

Спасибо, Жак. Чумовая идея!

* * *

все типы, определенные с помощью data, естественным образом задают равенство, если равенство задано для всех компонент. а именно: любому выражению "X y z ..." соответствует тупль (тэг конструктора, y, z, ...), и тогда равенство двух значений типа A - это равенство таких туплей покомпонентно. скорее всего, deriving Eq делает примерно то же. скорее всего, в типы, для которых равенство определить "инженерно" нельзя, входят только функции. ну и напоследок - я ж не претендую на ответ. я скорее интересуюсь у спецов (zeit-raffer, maxim, nponeccop) - разве не является существование такой вот процедуры собственно определением равенства в Хаскеле. ну или как, например, равенство задано в Агде? там тайп-чекер может проверить, являются ли значения равными. и проверяет ровно по такой же схеме. так задано ли равенство в Агде? и если да, то разве не задано оно и в Хаскеле точно таким же образом? если не является, то и было бы хорошо услышать разъяснений, в чем там существенное различие

1) то, что в тайпечере - это называется definitional равенство. это единственное равенство, без которого не обойтись
2) то, что покомпонетно сравнивает в рантайме - это рантайм равенство A->A->Bool, у нас оно генерируется макросами, так как универсальный терм для всех типов построить нельзя
3) propositional равенство строится легко и вычисляется с помощью элиминатора J, выразимого в чистом CoC
4) есть еще гомотопическое равенство, действующее в нетранкейтнутых вселенных, обычно называют его Path
это если кратко. как оно в Хаскеле я не знаю, как оно в Agda и Coq - можно легко найти и показать строчку при желании, с этим у них проблем нет

это я понимаю. однако, deriving Eq и строит definitional равенство (точнее, пользуется definitional равенством). я ж о том и говорю, что существование механизма говорит о том, что definitional равенство в Хаскеле есть

deriving (Eq) - это runtime равенства. Это 2) тип. definitional равенства не может не быть ни в одном языке программирования :-) остальные могут не быть. например у нас их нет. ну runtime конечно под вопросом, мы его макросами генерируем, но в ядре точно нет. все остальные равенства - это у нас обычные программы

ну, для иллюстрации. Агда видит, что foldr f z (x::r) - это то же самое, что f x (foldr f z r). т.е. я могу подставить любое из этих выражений. потому что тайпчекер может увидеть, что в обоих случаях будет использован одинаковый конструктор и конструктору будут переданы definitionally равные значения. deriving Eq делает то же самое: строит функцию, которая проверит, одинаковый ли конструктор у обоих значений, и равны ли компоненты, переданные одному и другому конструктору. то, что в рантайме Eq может быть определен по-другому, это понятно. я лишь о том, что существование механизма deriving Eq - это способ выдать на поверхность definitional равенство. значит, оно существует

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

я не говорю о рантайме. я говорю о том, как строится функция для рантайма. алгоритм там тот же, что в definitional равенстве у тайпчекера в Агде

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

это из разных песен. в теории типов (и использующих ее языках) могут быть разные равенства. Eq - это decidable равенство, оно используется в рантайме. во всяких там новомодных HoTT или классических интенсиональных/экстенсиональных теориях с зависимыми типами есть propositional равенство, которое живет на уровне статических типов. а есть еще равенство в метатеории (это с точки зрения ТТ оно так выглядит) - judgemental равенство, и теор-категорное равенство ему примерно соответствует, с той разницей, что в ТК оно существует внутри теории, а не в мета-. и вот именно его не хватает для структуры категории на Hask, причем не любого, а соответствующего семантике Хаскелля и аксиомам категории одновременно

* * *

нету никакой системы типов в динамических языках, там один тегированный тип

    data Tag = Int | String | Float | ...

ты не понимаешь разницы между наличием типизации и системой типов

>>> разница между динамической типизацией и статической предельно проста: в динамически типизированном языке все объекты имеют один единственный тип; в статически типизированном типов может быть много

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

data Term = Num   Float
          | Atom  String
          | Tuple [Term]
          | List  [Term]
          | Fun   ([Term] -> Term)
          ...

sqr (X) -> X * X.

hypot (X , Y) -> math:sqrt (sqr(X) + sqr(Y)).

sqr :: Term -> Term

hypot :: Term -> Term -> Term

Type  =  Term  |  Term -> Type

variable 'X' is unbound. многие видели это сообщение, прерывающее компиляцию. значит это, что переменная не определена (кэп). но откуда компилятор знает об этом? все просто - проверка области видимости - компилятор о каждом имени точно скажет где оно определено (bound) и места где оно используется. то же самое (проверка области видимости) происходит и с функциями компилируемого модуля, и с явно импортированными функциями - компилятор для каждой функции ищет место ее объявления и места ее использования. более того в местах использования происходит проверка арности, чт.е. не что иное как проверка типа:

% imported function declaration
% sqrt :: Term -> Term
-import (math, [sqrt/1]).

% module function declaration (and definition)
% sqr :: Term -> Term
sqr (X) -> X * X.

% references to declared functions and arity (type) checking
weird_id (X) -> sqr (sqrt (X)).

компилятор Erlang проверяет на этапе компиляции область видимости локальных переменных;
компилятор Erlang проверяет на этапе компиляции область видимости для явно импортируемых функций и функций компилируемого модуля;

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

* * *

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

• "список, состоящий из пяти строк",
• "сообщение, подписанное Василием";

типом функции может быть, например, "А меньше Б, Б меньше В, значит А меньше В" или "сообщение отправлено некоторому пользователю, значит данному пользователю доступно данное сообщение"; доказательством тогда становится тело функции, которое просто должно вернуть значение заданного типа, а проверка доказательства - это и есть проверка типов

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

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

разбор и составление текстовых/бинарных форматов: может быть формально доказано, что любые составленные строки разбираются в исходные данные, а разобранные данные - составляются в исходные строки

* * *

интуитистическая теория типов (Мартина-Лёфа, или конструктивная теория типов) успешно заменяет теорию множеств. основные положение заключается в том что типы конструируются из существующих типов

базовы типы - это

• Σ-типы - зависимые пары
• П-типы - типы функций
• конечные типы
• типы сравнения
• индуктивные конструктивные типы
• коиндуктивные конструктивные типы

в "просто типизированной лямбде" product type - это туплы, а sum type - это варианты, но dependent product и dependent sum они совсем другие, тут легко перепутать

тип Set в Coq стал предикативным только в версии 8.2

Prop импредикативный, а в Agda нету такого различения как в Coq между Prop и Set

* * *

ПРИТЧА О КОЛОБКЕ

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

"куда тебя парить? чем ты это сказал?"

потом, воспользовавшись тем, что вот это:

>> просто мемори буфер между физическими очередями ну и со своим async протоколом

это и есть актор [на самом деле нет, но имплементация до боли похожа], авторы акки наколбасили свои стримы таким образом. на акторах тривиально сделать backpressure (да что там, даже паксос на акторах пишется за пятнадцать минут, только пальцы наслюнявить), поэтому фигак-фигак, да и в продакшн. так родились akka-streams1.0, которыми даже кто-то пользовался, несмотря на 1:1 мэппинг стейджей в акторов (акторы дёшевы). потом, поколбасившись, запилили и fusion. нынче это state of the art

в отличие от акторов, стримы типизированы, т.е. и сношательное, и говорительное отверстие у каждого колобка (Inlet[T] и Outlet[T] в терминах акки) специфицированы в компайл-тайме. но! того и другого может быть максимум по одному. это нас не устраивает, потому что хочется-то многочасовой тантрической оргии (MPMC), а не скучного миссионерского секса. суровые шведы (благо опыт есть) подумали и сделали хак в виде Graph DSL. суть такова: берём несколько колобков, насаживаем их друг на друга, оставляем открытыми нужное количество отверстий, слепляем их в одного мега-колобка посредством GraphDSL, и оба-на! тантрический типизированый колобок готов (typed multi-input, multi-output stage). внутри он специфицируется посредством тех же самых stream combinators

казалось бы, бери и радуйся! но проблемы две

а) в скале нет dependent types, поэтому мы не можем автоматически типизировать колобка по количеству и видам входных и выходных отверстий. количество хаков, которым решается этот вопрос, поражает воображение (отдельно GraphShape и GraphLogic, материализаторы, итдитп), но большая часть проверок всё равно происходит в рантайме. а рантайм - это плохо, потому что никогда не знаешь заранее, каким именно венерическим заболеванием конкретно данный колобок тебя наградит. можно также взять Shapeless, где хотя бы есть полноценные generics, прям как в новом хаскеле, но к каждому, кто потащил Shapeless в продакшн, приходил демон и использовал в качестве колобка

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

по хорошему нужен join calculus

именно! join calculus - внутренний язык симметричных моноидальных категорий, операционная семантика линейных и аффинных типов!

я считаю, что лучше день потерять, зато потом за 5 минут долететь. надо ставить на что-то, что будет актуально через 5 лет и стараться мыслить чуть чуть вперед. так как все уже разобрались с ССС, пора взяться за SMC и построить наконец модель которая будет по DSL отвечать на вопрос: а какая емкость у этого элемента сети? на вопрос, на который ответили и без join calculus

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

минмальный набор join calculus сводится к пяти комбинаторам и SPMC, на которых можно строить уже MPSC, MPMC, Эрланги и типизированные самолеты

фьюжин проблему не решит, если у тебя вдруг откуда не возьмись появился третий актор. акторов в Pi-calculus должно быть два типа:

MPMC - это N * SPMC + N редюсеров (т.е. паралельных потоков выполнения, которые могут быть прямо в скедулере, в системе не может быть потоков больше чем ядер - иначе это уже еба-архитектура)

никаких третьих лиц быть не должно

one more thing: твоя оптимизация очередей работает только когда имеющиеся ресурсы более-менее константны (т.е. нужна RTOS, FPGA или там bare metal unikernel). в светлом будущем так и будет, но что-то надо уже сейчас

люди, запомните!

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

акторы осуществляют обмен асинхронными сообщениями между собой и измененяют свои состояния в ответ на эти сообщения. т.е. без способности актора изменять свое состояние и возможности обмениваться АСИНХРОННЫМИ сообщениями с другими акторами - нет и вообще никакой собственно модели акторов

аппликативные функторы сообщениями не обмениваются и состояний своих не меняют :) и аппликативы НЕ ТРЕБУЮТ последовательной композиции - вот поэтому они и подходят для параллельной композиции

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

* * *

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

в исчислении зависимых типов мы принципиально не можем отличить тип Int->Int (обычный функциональный тип) от forall (x:Int) . Int (полиморфный тип, в котором x - шаблонный параметр). в случае зависимых типов это один и тот же тип по определению П (x:Int) Int

именно в этом-то и суть зависимых типов - взаимопроникновение компайлтайма и рантайма

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

поэтому зависимые типы есть в Идрисе, но нету в Плюсах

* * *

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

давайте рассмотрим пару функций на Агде (объектами типа Set в Агде являются простые типы, такие как Int, String, etc.):

      Provider : String → Set
      Provider "Nat" = ℕ
      Provider "String" = String

      provide : (s : String) → Provider s
      provide "Nat" = 42
      provide "String" = "Hello world!" 

    len : String → ℕ
    len = ...
    
    test₁ = len (provide "String")
    test₂ = len (provide "Nat") -- Type error: ℕ != String 

    def provide(s):
      if (s == "int"):
        return 42
      elif (s == "str"):
        return "Hello world!"

    test1 = len(provide("str"))
    test2 = len(provide("int"))              # TypeError: object of type 'int' has no len()

единственная принципиальная разница - это то, когда именно выполняется provide: на Агде - во время компиляции программы, а на Питоне, соответственно - во время ее выполнения. но и там и там проверка типов при вызове функции len осуществляется уже после выполнения функции provide

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

      sub : (n m : ℕ) → m ≤ n → ℕ
      sub n .zero z≤n  = n
      sub (suc n) (suc m) (s≤s p) = sub n m p

зачем вообще нужны доказательства?

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

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

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

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

      Sub : ℕ → ℕ → Set
      Sub n zero = ℕ
      Sub zero (suc m) = ⊤
      Sub (suc n) (suc m) = Sub n m

      sub : (n m : ℕ) → Sub n m
      sub n zero = n
      sub zero (suc m) = _
      sub (suc n) (suc m) = sub n m

      x₁ : ℕ
      x₁ = sub 3 3 -- Ok

      x₂ : ℕ
      x₂ = sub 2 3 -- Type error: ⊤ != ℕ

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

данный подход является очень мощным, поскольку дает возможность проверять, а не доказывать. такой себе Пролог. все вычисления происходят во время компиляции. например, сначала строится Haskell style TypeRep (т.е. undecidable, НЕ типозависимый), так как это проще, а далее из этого TypeRep строится Decidable TypeRep. и в процессе построения просто проверяется можно ли это сделать. удобно и мощно

* * *

есть у нас такое:

F  : Set → Set
T  : Set
C₁ : (∃ α. F α) → T
C₂ : ∀ α. (F α → T)

(Exist → Forall) ∧ (Forall → Exist)

Exist = (∃ α. F α) → T
Forall = ∀ α. (F α → T)

Forall = (α : Set) → F α → T

в Agda то, что нам надо, запишется так:

      Exist = Σ (α ∶ Set) (F α) → T 

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

поэтому доказательство следующее (мы помним, что логическое "и" в нашей интерпретации ─ это тоже произведение):

      Exist ≡ Forall : (Exist → Forall) × (Forall → Exist)
      Exist ≡ Forall = curry , uncurry

boxed vs. unboxed types

различие не трудно распознать, если вы кодили на C, C++ или на Java (а в Perl все - boxed)

boxed-обьект распологается на хипе (выделяемом с помощью malloc/free [C] или new/delete [C++]) и достижим через указатель. unboxed-обьект распологается на стеке