Значения, типы, операции

a : A
						

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

\func inc(i : Int) : Int => i + 1
							

• значения - во время исполнения, типы - во время компиляции (и частично - во время исполнения)

\data List (A : \Type)
  | nil
  | cons A (List A)
						

• обычный список с элементами типа A

\func reverse{A : \Type}(as : List A) : List A
  => reverse0 as nil
  \where
    \func reverse0{A : \Type}(as accum : List A) : List A \elim as
      | nil       => accum
      | cons a as => reverse0 as (cons a accum)
							

• пример обычной функции

a : A
A : \Type
\func Function1(A B : \Type) : A -> B
\func ListType(A : \Type) : List A
						

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

вектор фиксированной длины

\data Vec (A : \Type) (n : Nat) \elim n
  | 0     => fnil
  | suc n => fcons A (Vec A n)
						

• можно смешивать значения и типы и выполнять операции

\func vec (A : \Type) (n : Nat) : \Type => Vec A n
\func prepend {A : \Type} {n : Nat} (v : vec A n) (a : A) : vec A (n + 1) =>
  fcons a v
\func head {A : \Type} {n : Nat} (xs : Vec A (suc n)) : A
  | fcons x _ => x
\func tail {A : \Type} {n : Nat} (xs : Vec A (suc n)) : Vec A n
  | fcons _ xs => xs
						

доказательство свойств: длина списка

\func length' {A : \Type} (xs : List A) : Nat
  | nil       => 0
  | cons _ xs => length' xs
						

• что-то здесь не так

\func length'==0 {A : \Type} (xs : List A) : length'(xs) = 0
  | nil       => 0 ==< idp >== 0 `qed
  | cons _ xs => length'==0(xs)
						

• то есть мы смогли доказать, что наше определение length' тождественно равно 0 для любых списков

свойство: если длина списка = 0, то список пуст

`length = 0 -> xs = nil`

\func length=0->nil {A : \Type} (xs : List A)
                    (length-xs=0 : length(xs) = 0) : xs = nil \elim xs
  | nil        => nil ==< idp >== nil `qed
  | cons _ xs  =>
   \let  suc=0 => suc (length xs) ==< length-xs=0 >== 0 `qed
   \in   suc/=0 suc=0
						

• это доказательство не работает для length'

\func length {A : \Type} (xs : List A) : Nat
  | nil       => 0
  | cons _ xs => suc (length xs)
						

• исправили ошибку

Обсуждение

язык не является полным по Тьюрингу!

• нет неограниченной рекурсии (и бесконечных циклов)
• все программы завершаются

зачем?

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

когда?

• тенденция переноса современных/новейших технологий
  • Haskell -> Scala
  • streaming -> Java
  • DOT -> Scala
• Dotty (Scala 3) будет иметь улучшенную поддержку зависимых типов
• наличие библиотек с доказанными алгоритмами, например, WhyML - http://toccata.lri.fr/gallery/why3.en.html

кому?

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

Профессиональная ответственность

• дорогие ошибки
  • смерть из-за рентгеновского аппарата
  • авария на дорогом космическом аппарате
  • смерть в результате ДТП с автопилотом
  • поражение в сражении в результате багов ПО
• (Р.Мартин, 2012): драконовские меры со стороны законодателей
  • ограничение на профессию
  • профессиональные стандарты
  • дресс-код