тайские хроники


* * *

допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 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 9 2 - полноправный элемент типа Nat. не число в привычной нам форме, не результат вычисления функции mul, а само выражение

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

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

     

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

    и вот эти элиминаторы (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
    

    то доказать их равенство, не только definitional, но даже propositional, мы не сможем! "Но это же одно и то же!"

     

    для этого нам требуется 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

    
        {-# 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]
    
    слева и справа от стрелки не конкретные типы, вроде Int, а выражения с переменной-типом, куда можно подставить конкретный тип и получить какой-то другой, т.е. это функции тип -> тип, т.е. функторы. получается, стрелка из функтора в функтор, естественное преобразование

    все полиморфные функции, вроде 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 на самом деле может отобразить [] в bot=0, что он с успехом и делает, бросая при этом исключение, каковое мы и видим

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

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

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

    * * *

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

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

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

    в Java генерики не работают с "примитивными" типами. все остальные типы в Java - это всегда указатель на объект, в терминах Си - void* (реже - void **)
    в каждом объекте по фиксированному смещению лежит указатель на дескриптор класса
    в дескрипторе класса по фиксированному смещению лежит указатель на таблицу виртуальных функций реализаций (с интерфейсами сложнее, т.к. для них есть множественное наследование).
    кстати, конструкторов в этой таблице нет и поэтому нельзя вызвать конструктор для параметризованного типа
    поскольку JIT'ы никогда не хранят скомпилированный код на диске, а только статистики выполнения, проблемы бинарной несовместимости не возникает
    таким образом, генерик-функция работает фактически с одним типом - void* с пришпиленными таблицами, по которым процессор может найти нужные ООП функции

    это в первом приближении, а во втором JIT-компилятор может создать сколько угодно экземпляров генерик-функции с заинлайненными вызовами и это поведение контролировать на уровне исходного кода нельзя. следствие - что генерики в Java бесполезны без ООП (ООП = все, что использует виртуальные функции или эквивалент. Страуструп сказал в 80-х: "вам не нужен С++, если вы не используете виртуальные функции")

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

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

    * * *

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

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

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

    Agda2 - точно да

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

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

        data Ha f where Se :: f a -> Ha f  
    параметр типа может быть конструктором типа. далее возникают всякие частичные применения и тп, которые приводят к типам высших порядков

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


    в C++ нет полиморфизма порядка выше 1
    темплейты — это вообще не типы. темплейты — это макросы на стероидах
    полиморфизм в плюсах — это наследование и только наследование

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

    какая связь?

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

    нет.

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

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

        template<template<class>,int> class    
    вполне себе тип шаблона; или, что то же самое, сами по себе являются значениями этих типов

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

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

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

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

    ну по такой логике и 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
    
    собственно единственное семнтическое различие - тонкое довольно - в Caml специализация функции, как значения, по ее типу запрещена, в плюсах - это практически единственный способ реализации. но единственная разница в семантике между этими реализациями обнаруживается оператором == благо referential transparency нет ни там ни там

    так. ещё раз. по буквам.

    семантика темплейтов определена единственным образом: как порождаемое ими AST в языке "C++ без темплейтов". только так и никак иначе. у вас просто не получится определить семантику темплейтов иначе - как бы вам ни хотелось "вынести всё в вэтэйблы"

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

    семантика типов в хаскеле другая, она определена через то, что происходит в рантайме. Вы НЕ сможете определить её через раскрытие типов высших порядков (если не хотите получить программу бесконечной длины). НЕТ двух принципиально разных этапов, первый из которых при компиляции генерит какое-то AST, уже не содержащее типов высших порядков. и не может быть

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

    и нет, в C++ НЕТ параметрического полиморфизма. есть макросы, которые более-менее этот полиморфизм эмулируют, протекая в некоторых местах

    ну как это нету - когда они и есть. причем практически haskell-style. собственно отображение почти 1 в 1 за исключением двух пунктов:

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

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

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

    > в чём проблема? "Литерал '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)
    это как раз то, для чего абстракции выделяют - возможность работать единообразно
    выделяем абстракцию и имеем бесплатно кучу высокоуровневых полезных функций. иначе нам пришлось бы их писать для каждого отдельного типа

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

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

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

    > replicateM 3 [False , True]

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

    > sequence [Just 1 , Just 2 , Just 3]

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

    > sequence $ Just [1 , 2 , 3]

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

    > runState (sequence [gets (\x -> x + 2) , state (\x -> (x + 1 , x + 20))]) 1

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

    > runState (replicateM 12 $ modify (\x -> x + 2)) 1

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

    > sequence [(\x -> x + 2), (\x -> x * 4), (\x -> x + x + 1)] 7

    и т.д.

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

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

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

    >>>для них бесплатны также функции, работающие для функторов и аппликативных функторов.
    в Хаскеле? нет, не имеем :)
    надо сперва сделать что-то функтором, потом аппликативом и уж только потом можно инстанс монады добавить. никакой халявы :)

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

    >>> внятными терминами оперировать, а не "связывание вычислений блаблабла"
    а что делать, если они таки "просто связывают вычисления блаблабла"?
    пусть у вас есть функция a -> b и тайпкласс m. с тайпклассом у вас получаются еще такие варианты функций:

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

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

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

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

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

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

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

    автор Идриса так и объясняет выбор: если результат одинаковый, а о потреблении ресурсов рассуждать проще, нафига тут ленивость?

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

    про идрис... первое, я привык к ленивости. а в моих задачах, частенько, можно и не думать над расставлением аннотаций строгости, и так будет всё более-менее. ну и когда надо (если поток по объёму большой) думать, это как-то всегда очень просто проходит. второе, вот что совсем неудобно и прям ломает, это по сравнению с хаскелём, почти полное отсутствие вывода типов. и связанные с этим невозможности написать удобные вещи, ну или даже точнее, что думать больше приходится. вот в where по поводу каждой мелочи типа m = n `mod` 2 типы писать убалтывает. ну и например, тупловые или списковые паттерны не получится использовать

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

    с выводом типов там правда фигово, но помогает 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;
    } ;
    
    ещё есть параметры владения, уникальности, константности. более того, есть итераторы, со своей классификацией (включая инпут-итераторы и т п), которые тоже можно спутать со списками (но не путают, потому что они абсолютно неюзабельны в качестве замены списков). а ещё есть циклические списки, списки, поддерживающие указатель на хвост (и соответственно, конкатенацию за O(1)), списки на деревьях и т.д. и параметры могут комбинироваться (но не произвольно)

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

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

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

    научить людей отличать алгебры от коалгебр - тяжелейшая задача

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

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

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

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

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

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

    у меня подозрение, что все эти итераторы появились из-за отсутствия функций высших порядков. чтобы в C++ можно было хоть как-то более-менее циклы писать. в языках, где есть ФВП, итераторы как-то не приживаются. особенно, если еще есть ленивые вычисления. те же Data.Foldable - это type class для операций, а не итераторы
    >в Хаскелле (да и в Окамле) нет традиции абстрагировать структуры данных или какие-то итераторы

    по-моему, во всех расширенных стдлибах Окамла (ExtLib, Batteries, Core) (а без них никто и не пишет, ибо совсем мучительно) есть итераторы, через которые со всеми коллекциями удобно работать. я сам все время ExtLib и его Enum использовал. в первую очередь Enum'ы нужны, чтобы спокойно делать композиции map'ов и filter'ов без создания промежуточных списков и массивов (то что в хаскеле выходит автоматически), плюс не нужно всем структурам реализовывать большой набор комбинаторов, вроде "отмапить и сфолдить множество ключей хэштаблицы" - достаточно уметь отдавать такой итератор, а комбинаторы к нему уже готовы. сложность операций выходит на практике очень понятная и приятная - работать в О(1) памяти всегда приятно

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

    * * *

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

    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 :: 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 | ...
    
    а все программы -- это моноиды

    ликбез по видам типизации:

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

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

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

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

    кстати, как раз эта цитата из TAPL не в вашу пользу. она говорит, что типы классифицируют "выражения языка", а не значения в рантайме. какой тип у выражения (+ a b)? как раз, примерно как приведен выше отцом Максимом. вот у рантайм-значения будет какой-то тип, о котором говорите вы, но это уже другая плоскость - не та, что описывается в TAPL

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

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

    
    data Term = Num   Float
              | Atom  String
              | Tuple [Term]
              | List  [Term]
              | Fun   ([Term] -> Term)
              ...
    
    в Erlang возможно задавать арность функций и проверять это на этапе компиляции. рассмотрим две функции:
    
    sqr (X) -> X * X.
    
    hypot (X , Y) -> math:sqrt (sqr(X) + sqr(Y)).
    
    а вот какие они имеют типы:
    
    sqr :: Term -> Term
    
    hypot :: Term -> Term -> Term
    
    очевидно, что они разные. получается в Erlang не один тип, а целое семейство, задаваемое рекуррентной формулой:
    
    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)).
    
    scope checking, проверка области видимости, является неотъемлемой частью статической типизации; далеко не все динамически типизируемые языки используют проверку области видимости во время компиляции

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

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

    Python, Lua, Ruby, PHP, JavaScript -проверка области видимости в runtime. scope checking - это атрибут любого языка, просто в Python это происходит в рантайме, а в Haskell - на этапе компиляции

    >> "в динамически типизированном языке все объекты имеют один единственный тип"
    это ложное утверждение. возьмем BASIC. есть переменная A = 20, есть B = "FOOBAR". одно можно поделить на 2, второе - нет. о каком единственном типе речь? интерпретатор по типу значения определяет, что можно, а что нельзя сделать с данным объектом. это означает, что рядом с самим значением лежит ссылка (код, номер) на тип (интерфейс работы со значениями данного типа). т.е. мы имеем своего рода boxed value. в динамически типизированном языке реализация скрывает от нас множество типов, лежащих этажом ниже. поэтому создается иллюзия, что тип якобы один

    это уже второстепенное. первостепенное - можете ли вы у объекта спросить его ссылку на поддерживаемые интерфейсы на этапе компиляции. в динамически типизорованных языках на этапе компиляции у вас нет доступа к списку поддерживаемых объектом интерфейсов. типизация, проверка типов, а значит и сами типы есть ТОЛЬКО НА ЭТАПЕ КОМПИЛЯЦИИ. в рантайме все - значения. может показаться, что и типы тоже есть, но это всего лишь список поддерживаемых интерфейсов, и этот список уже представляется в виде значения. система типов определяется тем, что известно на этапе компиляции

    * * *

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

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

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

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

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

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

    * * *

    в Charity есть индуктивные (конечные типы данных) и коиндуктивные, которые могут быть использозованны для бесконечных типов данных, отложенных вычислений. для индуктивных типов существуют операции case, fold и mapL, а для кониндуктивных соотвественно их ко-операции record, unfold и mapR

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

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

    в "просто типизированной лямбде" 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 должно быть два типа:

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

    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
    
    первый тест компилируется, тогда как второй нет. это и понятно, но самое интересное, что для определения типа нужно полностью выполнить функцию provide. то есть окончательный тип результата, с которым можно хоть что-то полезное делать, появляется только после выполнения самой функции. если еще раз пристально всмотреться в этот код можно увидеть следующее:
    
    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()
    
    и это не шутка :) даже несмотря на смайл :-D

    единственная принципиальная разница — это то, когда именно выполняется 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. и в процессе построения просто проверяется можно ли это сделать. удобно и мощно

    * * *

    нам надо exist , а мы пишем forall , но они эквивалентны и это доказывается

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

    
    F  : Set → Set
    T  : Set
    C₁ : (∃ α. F α) → T
    C₂ : ∀ α. (F α → T)
    
    Set ─ это так обозначается множество типов. нужно доказать, что C₁ и C₂ эквивалентны. докажем это в смысле, что с C₁ можно получить C₂, и наоборот, то есть:
    
    (Exist → Forall) ∧ (Forall → Exist)
    
    где:
    
    Exist = (∃ α. F α) → T
    Forall = ∀ α. (F α → T)
    
    ∀ представим в типизированном лямбда исчислении следующим образом:
    
    Forall = (α : Set) → F α → T 
    
    но для ∃ ничего подобного нету. но что значит существование в интуиционистской логике? "если утверждаешь существование чего-то, предъяви это". то есть, например, доказательством ∃x. x>1 может быть число 3 и доказательство, что 3>1. а на языке типизированного лямбда исчисления это есть ни что иное как зависимое произведение, то есть произведение в котором тип второго элемента зависит от значения первого.

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

    
    Exist = Σ (α ∶ Set) (F α) → T
    
    где Σ (α ∶ Set) (F α) ─ это тип из двух элементов: первый имеет тип Set, а второй тип F α, где α ─ значение первого элемента

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

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

    
    Exist ≡ Forall : (Exist → Forall) × (Forall → Exist)
    Exist ≡ Forall = curry , uncurry
    
    тут curry и uncurry ─ функции из стандартной библиотеки

    boxed vs. unboxed types

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

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