часть первая алгоритмы

 

структуры

  • типы данных
  • алгебраические структуры
  • Sigma-types
  • зависимые пары, карринг и Карри-Говард
  • Dependent Records
  • Pi-types
  • зависимые типы данных
  • декартово дерево

  • Крис Окасаки

    * * *

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

    в пакете было семь леденцов. Ящерица разделила лединцы на две кучки - себе пять и два - Змее

    и тут Змея сказала: "Э, нет - это несправедливо, у тебя леденцов больше, чем у меня. Добавь-ка мне один леденец из твоей кучки". Ящерица добавила змее один леденец

    но Змея снова сказала: "Все таки - нечестно, у тебя опять леденцов больше, добавь мне еще один"

    тогда Ящерица добавила Змее еще один леденец из своей кучки и теперь у Ящерицы стало три леденца, а у Змеи - четыре. "Эй, так тоже несправедливо - теперь у тебя леденцов больше, чем у меня! Верни-ка мне один леденец"

    Змея переложила один леденец из своей кучки в кучку ящерицы и теперь уже у ящерицы в кучке было четрые леденца, а у змеи - три. "Что происходит? Теперь у тебя снова леденцов больше! Ты жульничаешь!" и началась драка

    тут случилось проходить мимо их общему другу Черепахе. Черепаха поинтересовалась причиной ссоры и Ящерица со Змеей обьяснили суть дела

    "Так, если я разрешу вашу задачку, то вы дадите мне один леденец?" спросила Черепаха. Змее и Ящерице было жаль леденца, но и драться дальше они тоже не хотели - они согласились

    Черепаха обьединила леденцы в одну кучку, взяла из нее один леденец и стала уходить

    "Эй, постой! Ты сказала, если мы дадим тебе леденец, ты разрешишь нашу задачку!" - хором закричали Ящерица со Змеей

    "Ну а я что сделала?" - ответила им Черепаха

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

    на следующий день мама Змеи дала им коробку орехов. Змея с Черепахой открыли коробку и насчитали семь орехов. "Эх!" - воскликнули они в один голос и отправились искать Черепаху


    типы данных

    Александр Рулев

    в теории типов существует следующие базовые типы / семейства типов:

     нулевой (ложный) тип

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

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

      induction_0 : P:(∅ → U) → x:∅ → P x

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

    понятно, что у Нуля нет конструкторов

     единичный (истинный) тип

    этот тип заселён одним-единственным элементом I

    принцип индукции для единичного типа принимает доказательство некого утверждения для I (элемент типа Один) и возвращает доказательство утверждения для этого единичного элемента:

      induction_1 : P:(I → U) → x:I → P x

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

    конструктор у Один только один и это

     тип суммы (непересекающееся объединение)

    семейство типов, параметризируемое двумя другими типами (левым и правым):

      + : U → U → U

    имеет два конструктора, принимающие элементы либо левого, либо правого типа соответственно:

         left  : A:U → B:U → A → A + B
         right : A:U → B:U → B → A + B

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

      induction_sum : A:U → B:U → P:(A + B → U) →
                      (x:A → P (left  A B x)) →
                      (x:B → P (right A B x)) →
                      x:(A + B) → P x

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

    тип произведения (картезианский продукт)

    семейство типов, параметризируемое двумя другими типами (первым и вторым):

      ✗ : U → U → U

    один конструктор, принимающий оба значения типов A и B одновременно (A × B):

      (,) : A:U → B:U → A × B

    принцип индукции, обрабатывающий оба элемента пары:

      induction_prod : A:U → B:U → P:(A x B → U) →
                       (z:(A x B) → P (first A B z , second A B z)

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

    тип равенства

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

      = : A:U → A → A → U

    имеет единственный конструктор:

      refl : A:U → a:A → a = a

    конструктор говорит, что если мы имеем некий элемент некого типа, то он равен самому себе

    принцип индукции:

      induction_eq : A:U → P:(a:A → b:A → a = b → U) →
                    (x:A → P x x (refl A x)) →
                    x:A → y:A → p:(x = y) → P x y p

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

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

      ap : A:U → B:U → f:(A → B) → x:A → y:A → p:(x = y) → (f x = f y)
      ap A B f x y p = induction_eq A (a b _ => f a = f b)
                                      (x => refl B (f x)) x y p

    составные типы

    комбинации из представленных выше имеют конечное количество элементов. к примеру, тип «три элемента» может быть описан как (1 + 1) + 1. можно получить тип с четырьмя элементами: (1 + 1) × (1 + 1)

    но с таким набором типов мы не можем даже описать натуральные числа, количество элементов которых бесконечно (но счётно)

    простые рекурсивные типы

    нам нужны рекурсивные типы. например, такой:

      Nat = 1 + Nat

    где left I будет означать число ноль
    а right (left I) - единицу
    а right (right (left I)) — двойку
    и так далее

    принцип индукции для такого типа будет выглядеть так:

      induction_nat : P:(Nat → U) →
                      P (left *) →
                      (n:Nat → P n → P (right n)) →
                      x:Nat → P x

    тип этой функции это математическая индукция для натуральных чисел. если мы можем что-то доказать для первого элемента P(left I), а так же для элемента n+1 P(right n), при условии что для n утверждение является истинным Pn, то мы получаем доказательство для всех элементов

    допустим, мы взяли и ввели тип Nat = 1 + Nat и вроде бы ничего плохого не произошло, только хорошее:
    - получили натуральные числа,
    - целые числа Int = ((1 + 1) × Nat),
            (правда - с двумя нулями: правым и левым :)
    - рациональные числа (Int × Nat),
            (тоже - с двумя нулями)
    - вычислимые числа (m:Nat, Nat, ((n:Nat, n < m) → (1 + 1)))
            (всего бит,
            с какого бита начинается дробная часть,
            бит на некой позиции
            знак числа)

    но можем ли мы «от балды» вводить новые типы?

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

      Boolean : U
      true, false : Boolean
    
      induction_boolean : P:(Boolean → U) → P true → P false → x:Boolean → P x
    
      
    
      SomeDualStruct : U → U
      fconstr : T:U → Nat → T → SomeDualStruct T
      sconstr : T:U → Int → SomeDualStruct T
    
      induction_someDualStruct : T:U → P:(SomeDualStruct T → U) →
                                 (n:Nat → t:T → P (fconstr T n t)) →
                                 (k:Int → P (sconstr T k)) →
                                 x:(SomeDualStruct T) → P x

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

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

      G = G → 0

    потому что тогда можно получить Ложь и моментально сделать всю нашу теорию противоречивой:

      (λ f . f f) : G = G → 0
      (λ f . f f) (λ f . f f) : 0

    на первой строчке имеем функцию, которая принимает аргументом некоторую функцию, к которой применяет саму себя. её тип, очевидно, для этого должен соответствовать маске G=G→?, где вместо знака вопроса можем подставить что хотим, например, Ложь. затем передаём этой функции саму себя. тип результата получается 0. но тип Ноль у нас был ненаселенный, а мы его тут населили - непорядок в теории

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

    тип является рекуррентным относительно типа G (будем обозначать IsRec[G]), если:

    сложные рекурсивные типы

    кроме просто рекурсивных типов, могут быть вот такие замысловатые цепочечные типы:

      A = 1 + B
      B = 1 + A

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

    универсум

    выше часто использовалось некоторое U. это тип типа, т.е. его значениями являются остальные типы … кроме его самого. сам U тоже является значением какого-то типа. и этим типом является U1. тип которого U2. тип которого U3. …

    каждый верхний универсум содержит все типы, которые содержат нижние универсумы т.е. универсумы кумулятивно вложены друг в друга. и, например, в универсуме U2 существует тип U1 + U, а в универсуме U1 такого типа нет, поскольку он не может содержать в себе самого себя

    не спрашивайте, почему так и почему универсум не может иметь тип самого себя — простого доказательства нет. ПОВЕРЬТЕ. если допустить это, то в теории появляются парадоксы

    конструктивный подход к предикатам

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

          аксиомы:
    
          
          ⊥          P x           ∀x . P X         P t         ∃x . P x   P x  => Q
        -----      --------        --------       --------      --------------------
          P        ∀x . P x           P t         ∃x . P x              Q
    
    
                       
                       
         Refl       Sym          Trans              Ext                 Subs
                       
                   s = t      r = s  s = t     ∀x . s x = t x        s = t   P s
        -----      -----      ------------     --------------        -----------
        x = x      t = s          r = t             s = t                P t
    
    
                       
    
         отношения:
                       
         ∈      ∪     ∩     ⊆
    
    
    
    

    α -> β тип функции term depending on terms
    α -> Prop -> Prop квантор всеобщности proof depending on terms
    Prop -> Prop -> Prop импликация proof depending on proofs

    пусть Prop есть множество { ∅ , {*} }, т.е. множество состоящее из двух элементов - пустого множества и синглтона (не важно с каким именно элементом)

    пусть операция обрезания ⟦⟧ для любого множества X определена как

        ⟦X⟧ : if X = ∅ then ∅ else {*}
      

    теперь:

    предикат - это n-арная функция a₁ → a₂ → ... aₙ → Prop

    квантор - это функция a → Prop с арностью 1, аргументом которой является предикат

    пусть A есть множество, B есть множество и U тоже есть множество

    пусть Σ (a : A) (B a) есть такое множество пар { (a , u)   |   a ∈ A , u ∈ U }

    тогда квантор ∃ есть ⟦Σ (a : A) (B a)⟧ и тоже является множеством

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

                      exists x . P (x)     становится        ∃x . (x  ∈  A)   /\   P (x)
    
    таким образом квантификатор ∃ становится инфиниарным аналогом \/ : будем перебирать всю (может быть - бесконечную) последовательность значений типа А и упремся наконец-таки в такое значение, которое удовлетворит предикату

    пусть Π (a : A) (B a) есть такое множество пар { (a , b)   |   a ∈ A , b ∈ A → U }

    тогда квантор ∀ есть Π (a : A) (B a) и тоже является множеством

    в конструктивной логике квантор всеобщности интерпретируется, как генерализация функций. в частности, если выбор U не зависит от A, то квантор всеобщности соответствует функции A → U

                      forall x . P (x)     становится       ∀x . (x ∈ A) -> P(x)
    
    таким образом квантификатор ∀ становится инфиниарным аналогом /\ : у нас есть (может быть - бесконечный) кортеж значений типа А, каждое из которых удовлетворяет предикату

    предположим, что есть множество D и предикат P(x) который определен для любого x ∈ D. тогда закон исключенного третьего утверждает: не важно какое именно множество D и какой предикат P мы рассматриваем, но

         ∀ x ∈ D . P(x) \/ ~ P(x)
    

    конструктивная же математика полагает, что правильность этого утверждения завистит от P. это означает, что возможно существуют такие P, для которых сама постановка вопроса "истинно ли Р(x)" не имеет смысла. самый известный пример - так называемый "парадокс" Рассела, который никаким парадоксом не является, как только мы предположим, что множество всех множеств - не множество (что Кантор задолго до Рассела и сделал - и предположил, и постулировал)

    еще один пример: если последовательность an нулей и единиц не всегда нуль, то содержит ли она едининцу?

         ~ (∀ n ∈ N . an = 0)   =>   ∃ n ∈ N . an = 1
    
    утвердительный ответ на этот вопрос называется "приципом Маркова". этот принцип основан на утверждении о всех таких последовательностях - в совокупности. хотя он и "очевиден" с точки зрения здравого смысла, но мы не можем дать убедительного доказательства сразу для ВСЕХ таких последовательностей - только для индивидуальных

    другой пример: зададимся вопросом: "если программа не выполняется вечно, то завершается ли она?". на практике гораздо важнее ответ на вопрос "если программа не выполняется вечно, то завершается ли она за время t". ответ на первый вопрос вовсе не является ответом на второй. конструктивное же доказательство первого высказывания может предоставить достаточно информации для ответа и на второй вопрос тоже

    соответствие Карри-Ховарда

    изоморфизм Карри-Ховарда устанавливает взаимно-однозначное соответствие между типами и логическими утверждениями, что в свою очередь, позовляет навести мосты между программами и доказательствами.
            ------------+------------------------
              function  |      prop
            ------------+------------------------
               A → B    |      A => B
               ¬ A      |      A => ∅        
               A ∨ B    |     ⟦A U B⟧    
               A ∧ B    |      A × B
                ∃       |    ⟦Σ (a : A) (B a)⟧
                ∀       |    Π (a : A) (B a)
            ------------+------------------------
    

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

    для доказательства истинности утверждения a v b достаточно предьявить термы соответствующих типов "по отдельности": a | b

    аксиома выбора выглядит так: Π(a:A) (⟦B a⟧) -> ⟦Π(a:A) (B a)⟧

    Агда:

    module Dependent where
          
    Π : (a : Set) → (a → Set) → Set 
    Π I V = (x : I) → V x
    
    data Σ (I : Set) (V : I → Set) : Set where
      _,_ : ∀ (fst : I) → V fst → Σ I V
    
    postulate A : Set
    data Id : A → A → Set where
      id : (x : A) → Id x x 
    
    -- TODO
    

    алгебраические структуры

    алгебра - это совокупность образующего множества и замкнутых на нем n-арных операций и отношений

    группа - это алгебра с одной бинарной операцией, единичным элементом (нуль-арная операция) и инверсией (одно-арная операция)

    моноид - это группа без инверсии, но с единичным элементом

    полугруппа - это группа без единичного элемента и, следовательно, - без инверсии

    Idris:

    implementation Semigroup Nat where
      x <+> y =  x + y
            
    data Option a = Some a | None
    
    implementation Semigroup a => Semigroup (Option a) where
      (Some a) <+> (Some b) = Some (a <+> b)
      None <+> a = a
      a <+> b = a
      
    implementation Semigroup a => Monoid (Option a) where
      neutral = None
    
    
          
    ex01 : Nat -> Option Nat
    ex01 x = Some x <+> None
    
    ex02 : Nat -> Option Nat
    ex02 x = None <+> Some x 
    
    ex03 : Nat -> Nat -> Option Nat
    ex03 x y = Some x <+> Some y 
    
    ex04 : List (Option Nat) -> Option Nat
    ex04 xs = concat xs
    
    ex05 : List (Option Nat) -> Option Nat
    ex05 xs = concatMap (\x => case x of 
                                    None => None 
                                    Some y => Some (y + 2)) xs
    
     

    λΠ> :let z List (Option Nat) = [Some (succ Z) , Some (succ Z),  Some (succ Z)] 
     defined
    λΠ> z
     [Some 1, Some 1, Some 1] : List (Option Nat)
    λΠ> ex04 z
     Some 3 : Option Nat
    λΠ> ex05 z
     Some 9 : Option Nat
    

    и вот для чего нужен Идрис:


    monoid, functor, applicative, foldable, traversable

    Идрис:

    -----------------------------------
    Semigroup
    -----------------------------------
    
        interface Semigroup x where
          (<+>) : x -> x -> x
    
    
    -----------------------------------
    Monoid
    -----------------------------------
    
        interface (Semigroup x) => Monoid x where 
           neutral : x
    
    
    -----------------------------------
    Functor
    -----------------------------------
    
        interface Functor (f : Type -> Type) where
          map : (m : a -> b) -> f a -> f b
    
            --- not obligatory -----------
        
         (<$>) : Functor f => (a -> b) -> f a -> f b
    
          
    -----------------------------------
    Applicative
    -----------------------------------
    
        interface (Functor f) => Applicative f where
          pure  : a -> f a
          (<*>) : f (a -> b) -> f a -> f b
    
            --- not obligatory -----------
    
          (<*)   : f a -> f b -> f a
          (*>)   : f a -> f b -> f b
    
          liftA  : (a -> b) -> f a -> f b
          liftA2 : (a -> b -> c) -> f a -> f b -> f c
          liftA3 : (a -> b -> c -> d) -> f a -> f b -> f c -> f d
    
          when   : Applicative f => Bool -> Lazy (f ()) -> f ()
    
    
    -----------------------------------
    Alternative
    -----------------------------------
    
       interface Applicative f => Alternative f where
         empty : f a
         (<|>) : f a -> f a -> f a
    
            --- not obligatory ----------------
    
         choice    : Foldable t => t (f a) -> f a
         choiceMap : Foldable t => (a -> f b) -> t a -> f b
    
         guard     :  Alternative f => Bool -> f ()
    
    
    ------------------------------------
    Foldable
    ------------------------------------
    
        interface Foldable (t : Type -> Type) where
          foldr : (elem -> acc -> acc) -> acc -> t elem -> acc
    
          --- not obligatory ---
    
          foldl : (acc -> elem -> acc) -> acc -> t elem -> acc
          foldl f z t = foldr (flip (.) . flip f) id t z
    
          concat : (Foldable t, Monoid a) => t a -> a
          concat = foldr (<+>) neutral
    
        ---  map-reduce
          concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
          concatMap f = foldr ((<+>) . f) neutral
    
          sum : (Foldable t, Num a) => t a -> a
          sum = foldr (+) 0
    
          product : (Foldable t, Num a) => t a -> a
          product = foldr (*) 1
    
          any : Foldable t => (a -> Bool) -> t a -> Bool
          any p = foldl (\x,y => x || p y) False
    
          all : Foldable t => (a -> Bool) -> t a -> Bool
          all p = foldl (\x,y => x && p y)  True
    
          and : Foldable t => t (Lazy Bool) -> Bool
          and = foldl (&&) True
    
          or : Foldable t => t (Lazy Bool) -> Bool
          or = foldl (||) False
    
    
    ------------------------------------
    Traversable
    ------------------------------------
    
        interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
          traverse : Applicative f => (a -> f b) -> t a -> f (t b)
    
           --- not obligatory -----------
                    
          traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
          traverse_ f = foldr ((*>) . f) (pure ())
    
          sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
          sequence = traverse id
          -- id применяется к 'a', но при этом внешняя оболочка меняется ролями с внутренней
          --    процесс сломается на первом же Nothing при аргументе List (Maybe ...) 
          --              или     на первом же Left при List (Either ... )
    
          sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
          sequence_ = foldr (*>) (pure ())
    
          for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
          for = flip traverse
    
          for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
          for_ = flip traverse_
                    
    

    и пример применения:

    data Tree : Type -> Type where
      Node : Tree a -> Tree a -> Tree a
      Leaf : a -> Tree a
    
    t : Tree Int
    t = Node (Leaf 10) (Node (Leaf 20) (Leaf 30))
    
    implementation Semigroup Int where
      x <+> y = x + y
    
    implementation Monoid Int where
      neutral = 0
    
    implementation Functor Tree where
      map f (Leaf x) = Leaf (f x)
      map f (Node x y) = Node (map f x) (map f y)
    
    implementation Foldable Tree where
      foldr f a (Leaf x) = f x a
      foldr f a (Node x y) = foldr f (foldr f a x) y
    
    implementation Traversable Tree where
      traverse f (Leaf x) = Leaf <$> f x 
      traverse f (Node x y) = Node <$> (traverse f x) <*> (traverse f y) 
    

    λΠ> t
      Node (Leaf 10) (Node (Leaf 20) (Leaf 30)) : Tree Int      
    λΠ> foldr (\x , y => x + y) 0 t
      60 : Int
    λΠ> map (\x => x + 2) t
      Node (Leaf 12) (Node (Leaf 22) (Leaf 32)) : Tree Int
    λΠ> traverse (\x => Just (x + 2)) t
      Just (Node (Leaf 12) (Node (Leaf 22) (Leaf 32))) : Maybe (Tree Int)
    


    Dependent Pairs (Sigma-Types)

    одним из базовых элементов, появляющихся с зависимыми типами, является зависимая пара - обобщение произведения типов, известное как зависимая сумма (dependent sum):

          x   ✗   P x   

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

    псевдо-код :

          Σ : A:U → (A → U) → U
          Σ (x:A) (t x)    

    вторым аргументом конструктора является λ-аппликация, нормальной формой которой является какой-либо тип, но не λ-абстракция

    но второй аргумент является не просто типом, а семейством типов для того, чтобы иметь возможность создавать утверждения «существует элемент x, для которого выполняется Y». например, утверждение «число n является чётным» является типом зависимой пары, а одним из значений может быть, например, пара (6, 6 mod 2 = 0). это очень удобно - быть способными описывать квантификатор существования таким вот образом

    но теперь мы должны полагать U не как тип, а как супертип. мы не можем утверждать, что U ∈ U, потому что это приведет к противоречивости нашей теории, поэтому мы вводим высший тип U1. так что U ∈ U1

    с названиями зависимых типов очень все запутано. попробуем разобраться

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

    ∃x . P x значит "у меня есть (пока что) неопределенное значение х и, вместе с ним, способ доказательства того, что для х имеет место свойство Р"

    таким вот образом естественным подтверждением существования х является ПАРА, состоящая из самого х и из терма, показывающего, что Р х выполнимо. поэтому Сигма-типы еще называются "зависимыми произведениями". такая структура данных просто-таки требует, чтобы ТИП второго элемента зависел от ЗНАЧЕНИЯ первого.

    с точки зрения классической логики exists x . P (x) означает, что Р(х) выполняется, но только вы точно не знаете, для какого именно значения х. таким образом вы понимаете это как наличие очень большого логического "ИЛИ" (обьединения):

             P(x0) \/ P(x1) \/ P(x2) \/ P(x3) \/ ...  

    а поскольку логическая операция "ИЛИ" тесно связана с типами "СУММА", то и Сигма-типы иногда назвают "зависимыми суммами"

    в Idris зависимая пара определа так:

        data DPair : (a : Type) -> (P : a -> Type) -> Type where
           MkDPair : (x : a) -> (pf : P x) -> DPair a P
     

    логическая интепретация такой пары звучит так: "существует такой x, для которого выполнено утверждение Р(х)". сам Σ-тип становится "заявлением" о том, что вся эта механика в целом существует, а значения этого типа - пары конкретных значений - становятся "вещдоками". в них первый элемент называется witness, свидетель, т.к. это конкретный пример того значения х, про которое мы заявляем, что оно существует, а второй элемент называется proof, т.к. он служит доказательством выполненности утверждения Р для этого х

    "свидетеля" можно вытащить на свет божий с помощью "повестки в суд":

           Prelude.Pairs.DPair.getWitness : DPair a P -> a
    

    предьявление вещдоков в зале судебного заседания осуществляется так:

           Prelude.Pairs.DPair.getProof : (x : DPair a P) -> P (fst x)
    

    есть синтаксический сахар для сигнатур: (a : A ** P)

    пример:

        ex00 : Bool -> (a -> a) -> (a -> a) -> (p : Bool ** (Bool -> (a -> a))) 
        ex00 p f g = MkDPair p (\p => if p then f else g)
    
        ex01 : Int -> Bool -> Int 
        ex01 x b = ((snd $ ex00 b (* 10) (+ 2)) b) x 
    
        ex02 : String -> Bool -> String
        ex02 s b = ((snd $ ex00 b toLower toUpper) b) s 
    

    λΠ> ex01 6 True
      60 : Int
    λΠ> ex01 6 False
      8 : Int
    λΠ> ex02 "hello" False
      "HELLO" : String
    λΠ> ex02 "hello" True
      "hello" : String
    

    зависимые пары, карринг и Карри-Говард

    Дмитрий Попов

    типы ((a , b) -> c) и (a -> b -> c) эквивалентны, т.к. мы можем описать две функции от одного к другому и обратно, композиция которых равна id, т.е. построить изоморфизмы:

    Идрис

    id1 : ((a , b) -> c) -> (a -> b -> c)
    id1 z = \x => \y => z (x , y)
    
    id2 : (a -> b -> c) -> ((a , b) -> c)
    id2 z = \p => z (fst p) (snd p)
    
    f : (Int , Int) -> Int
    f (x , y) = x + y
    
    g : Int -> Int -> Int
    g x y = x + y
    
    ex : Int -> Int -> Bool
    ex x y = id1 f x y == id2 g (x , y)
    

    давайте теперь возьмем эти изоморфизмы про обычные пары, и запишем их для зависимых пар:

    using (A : Type, B : A -> Type, C : Type)
        
      id3 : ((x : A ** B x) -> C) -> ((x : A) -> B x -> C)
      id3 h = \a => \b => h (a ** b)
    
      id4 : ((x : A) -> B x -> C) -> ((x : A ** B x) -> C)
      id4 h = \p => h (getWitness p) (getProof p)
    

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

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

         (∃x:A . B x) => C      <=>       ∀x:A . (B x => C) 
    

    это то, что позволяет в языках вроде Хаскеля и Окамла записывать экзистенциальные типы, обходясь без ключевого слова exists, а лишь квантором всеобщности forall

    еще один морфизм на ту же тему:

      id5: (x:A ** (B x -> C)) -> (((x:A) -> B x) -> C)
      id5 p = \h => (getProof p) (h (getWitness p)) 
    

    он показывает, что

        ∃x:A . (B x => C)      =>      (∀x:A . B x) => C
    

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

    A - не населенный
    C - населенный
    B - любой
    тогда функция с типом ∀x:A . B(x) => C существует,
    но значение с типом ∃x:A . ( B(x) => C ) построить нельзя,
    поскольку нельзя найти x:A

    Dependent Records

    Idris:

     import Data.Vect
    
     record Person where
       constructor MkPerson 
       fstName : String 
       sndName : String
       age     : Int
    
     record Team (k : Nat) where
       constructor MkTeam 
       students : Vect k Person 
       teamName : String
    
     addStudent : Person -> Team n -> Team (S n) 
     addStudent p c = MkTeam (p :: students c) (teamName c)
    
     zeroteam : Team 0
     zeroteam = MkTeam [] "Dream Team"
    
     oneteam : Team 1
     oneteam = addStudent (MkPerson "Bob" "Dilone" 54) zeroteam 
    
     twoteam : Team 2
     twoteam = addStudent (MkPerson "Charlie" "Mainson" 61) oneteam
    

    Type checking ./deprecs.idr
         
    λΠ> twoteam
    MkTeam [MkPerson "Charlie" "Mainson" 61, MkPerson "Bob" "Dilone" 54]
           "Dream Team" : Team 2
    λΠ> students twoteam
    [MkPerson "Charlie" "Mainson" 61, MkPerson "Bob" "Dilone" 54] : Vect 2 Person
    λΠ> age $ Data.Vect.head $ students twoteam 
    61 : Int
    
    λΠ> :let z : Team 5
    defined
    λΠ> :let z1 = addStudent (MkPerson "c" "d" 34) z
    defined
    λΠ> z1
    MkTeam (MkPerson "c" "d" 34 :: students z) (teamName z) : Team 6
    λΠ> :let z2 = addStudent (MkPerson "a" "b" 76) z1
    defined
    λΠ> z2
    MkTeam (MkPerson "a" "b" 76 :: MkPerson "c" "d" 34 :: students z)
           (teamName z) : Team 7
    
    λΠ> Data.Vect.index 1 (students z2)
    MkPerson "c" "d" 34 : Person
    λΠ> Data.Vect.index 0 (students z2)
    MkPerson "a" "b" 76 : Person
    λΠ> Data.Vect.index 10 (students z2)
    (input):1:20:When checking argument prf to function Data.Fin.fromInteger:
            When using 10 as a literal for a Fin 7 
                    10 is not strictly less than 7
    

    Dependent Functions (Pi-Types)

         x    ✗    L x 

    элементами этого типа являются пары, в которых вторым элементом являются функции, чья область значения (ее ТИП) зависит от ЗНАЧЕНИЯ (но не от типа) первого элемента пары

    псевдо-код :

       Π : A:U → (A → U) → U
       Π (z : A) (λ x . t) 

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

    но второй аргумент является не просто типом, а семейством типов для того, чтобы иметь возможность создавать утверждения «для любого элемента x выполняется Y x». это очень удобно - быть способными описывать функции, чей тип области значения зависит от значения входного параметра. например можно определить функцию целых чисел в виде \x. if (even x) then 2 else (if (x == 3) then (\x. x) else (\x. "не два"))

    но теперь мы должны полагать U не как тип, а как супертип. мы не можем утверждать, что U ∈ U, потому что это приведет к противоречивости нашей теории, поэтому мы вводим высший тип U1. так что U ∈ U1

    с названиями опять все запутано и опять попробуем разобраться

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

    в этом случае в формуле ∀x . L x переменная x пробегает весь ряд натуральных чисел

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

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

      f : nat -> foo
      f : nat -> bar
      f : nat -> baz
           ...
      f : nat -> qux
           ...
     
    т.е. таких, что тип результата (foo|bar|baz|...|qux|...) зависит от x (то есть может быть и bar, и baz, и т.д. и qux и т.д. и даже foo:)

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

    в классической логике предикатов универсальный квантификатор forall x. L(x) означает, что вы уверены в том, что L(n) выполняется для всех натуральных чисел

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

     
                L(0) /\ L(1) /\ L(2) /\ L(3) /\ ... 
    
    а поскольку операция "И" и "типы картезианского произведения" связаны, Pi-Types часто называют "зависимым произведением"

    конструкторами Pi-type являются конструкторы прочих типов, а так же
    - лямбда-конструкции, которые могут создавать функции: λ x . ?
    - применение терма-функции к терму-переменной: f a
    на месте вопросительного знака может быть подставлено другое лямбда-выражение, либо свободное значение x. в случае подставления другой «болванки функции» эти значения необходимо различать и не позволять использовать свободные значения из внутренних функций во внешних

    зависимые типы данных

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

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

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

    итак:
    1. есть определение зависимых типов, в котором четко указывается, что в Пи-тип можно подставить любой терм
    2. известно, что если ограничить подставляемые термы, то нарушится соответствие между Пи-типами и функциональными типами, которое является для зависимых типов ключевым
    3. известно, что Плюсы не удовлетворяют вышеприведенному определению
    QED

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

    декартово дерево

    // TODO
    


    Михаил Дворкин


    Михаил Дворкин