�ݺ�ߣ

Краткий экскурс в системы типов или
как избежать дезинтеграции
Денис Редозубов, @rufuse
June 22, 2015

Martian Climate Orbiter Distaster
ˆ 1998 - спутник NASA Martian Climate Orbiter сгорел в
атмосфере марса из-за программной ошибки.
Figure: Martian Climate Orbiter

Martian Climate Orbiter Distaster (2)
Ошибка заключалась в том, что выполнялась арифметика
с единицами из разных систем измерения.
due to ground-based computer software which
produced output in non-SI units of pound-seconds
(lbfÖs) instead of the metric units of
newton-seconds (NÖs) specified in the contract
between NASA and Lockheed — Wikipedia
Этого можно было бы избежать, если бы разработчики
утилизировали систему типов

Часто приоритеты таковы что
Correctness is dog
Figure: performance is tail
(C) @runarorama

Что такое тип?
В первом приближении - множество применимых
вычислимых выражений.

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

Что такое система типов? (2)
Неформально - система мер, направленная на исключение
возможности для программы перейти в противоречивое
или абсурдное состояние.

Статическая типизация
ˆ Языки программирования, в которых тип каждого
выражения может быть определен статически(обычно
на одном из этапов компиляции), называются
статически типизированными.(Scala, Haskell, Ocaml)

Статическая типизация
ˆ Языки программирования, в которых тип каждого
выражения может быть определен статически(обычно
на одном из этапов компиляции), называются
статически типизированными.(Scala, Haskell, Ocaml)
ˆ Языки, в которых проверка типов на согласованность
происходит во время выполнения называются
динамически типизируемыми. Более верным
термином можно считать "динамически
проверяемые", т.к. нет никаких гарантий что типы в
программе будут согласованы.(Lisp, Clojure)

Сильная/слабая типизация
ˆ Сильная типизация(strongly typed) - свойство языков,
в которых типы всех выражений согласованы(Haskell,
Common Lisp)

Сильная/слабая типизация
ˆ Сильная типизация(strongly typed) - свойство языков,
в которых типы всех выражений согласованы(Haskell,
Common Lisp)
ˆ Слабая типизация(weakly typed) - милое название для
отсутствия типизации. Отсутствие мер против
написания абсурдных программ.

Явность типизации
ˆ Явно типизируемыми называются языки в которых
программист должен явно указывать тип каждого
выражения(Java, C)
ˆ Неявно типизируемыми называются языки, в которых
тип выражения может быть выведений из выражений,
его использующих. Неявная типизация требует
реализации механизма выведения типов и может быть
как полной, так и неполной.(Haskell, Scala)

Многообразие программ
A
B
ˆ A - корректно-типизированные(well-typed) программы
ˆ B - работающие программы

Сохранение инвариантов
ˆ Инвариант - свойство выражений оставаться
непротиворечивыми в результате изменений.
ˆ Для каждого выражения его тип является
инвариантом.
ˆ Цель типизации - сделать неверное состояние
невозможным для представлени в программе.

Соответствие Карри-Говарда (1934 - 1969)
ˆ Наблюдение о связи логических доказательств и
алгебры вычислений. Это означает, что
доказательство в терминах достаточно сильной
системы типов является доказательством
корректности программы.
ˆ Под "достаточно сильной системой типов" я имею в
виду систему типов, способную выразить необходимые
инварианты.

Перенос части проблем из runtime в compile
time
ˆ Не требует запуска программы и кучи интеграционных
мероприятий для проверки кода
ˆ Быстрее запуска test-suite на проектах, которые
больше чем тривиальные

Рефакторинг и поддержка кода
ˆ unsound программа просто не будет компилиться,
после несогласованных или неполных изменений.
ˆ Позволяет сразу увидеть все места, где изменения в
программе ведут к поломке.
ˆ Позволяет меньше опираться на тесты, которые
устаревают, ломаются и требуют постоянной
поддержки. Кроме того, тесты не дают никаких
формальных гарантий, т.к. за ними нет научных
теорий.
ˆ Не требует знать и любить все костыли в огромных
системах - все тайное становится явным.

Рефакторинг и поддержка кода (2)
x
f(x)
f(x) = 1
20ex

Хорошо типизированная программа является
самодокументируемой
ˆ Пример плохо типизированной программы
f :: Double
-> Double
-> String
-> Double

Хорошо типизированная программа является
самодокументируемой
ˆ Пример плохо типизированной программы
f :: Double
-> Double
-> String
-> Double
ˆ Пример хорошо типизированной программы
f :: Commission
-> Commission
-> CombinationStrategy
-> Commission

Строгость системы типов напрямую связана с
корректностью программ
ˆ Все хотят спокойно спать по ночам
ˆ Бизнес, а иногда и человеческие жизни, зависят от
правильности кода

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

Типы-суммы
ˆ aka Sum-types, Union-types, disjoined union
ˆ Представляют собой непересекающиеся объединения
"меток"
ˆ примеры(слева - конструктор типа, справа -
конструкторы данных):
data Direction = Forward | Backward
data Movement = Step Direction
| Jump Direction
| Dash Direction

Pattern-Matching
ˆ например
move :: Movement
-> GameState
-> Character
-> GameState
move (Step direction) s c = step direction s c
move (Jump direction) s c = jump direction s c
move (Dash direction) s c = dash direction s c

Pattern-Matching (2)
ˆ Никто не любит писать много, поэтому записывают
так:
move :: Movement
-> GameState
-> Character
-> GameState
move (Step d) = step d
move (Jump d) = jump d
move (Dash d) = dash d

Типы-пересечения
ˆ aka Product-types
ˆ Пары
ˆ Кортежи
ˆ Рекорды
ˆ Объекты
data Color = RGB { red :: Value
, green :: Value
, blue :: Value }

Алгебраические типы данных
ˆ aka Algebraic Data Types(ADT)
ˆ Объединяют в себе свойства типов-сумм и
типов-пересечений

Лямбда-куб
Figure: Lambda Cube
λ - простое типизированное лямбда-исчисление

Параметрический полиморфизм
ˆ Открывает возможность для создания абстрацкий
ˆ Самые банальные примеры - всем известные
контейнеры
data List a = Nil | Cons a (List a)

ad-hoc полиморфизм
Интерфейсы/тайпклассы/трейты
class Eq a where
(==), (/=) :: a -> a -> Bool
instance Eq a => Eq (List a) where
Nil == Nil = True
Nil == _ = False
_ == Nil = False
(Cons h1 t1) == (Cons h2 t2) = h1 == h2 && t1 == t2

Type functions/operators
Возможность описывать преобразования типов
class Add a b where
type SumTy a b
add :: a -> b -> SumTy a b
instance Add Float Integer where
type SumTy Float Integer = Float
add a b = a + fromInteger b
instance Num a => Add a a where
type SumTy a a = a
add = (+)

Зависимые типы
Типы, зависимые от термов
data Nat = Z | S Nat
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

Как сделать, чтобы система типов была
помощью и опорой?
ˆ Делаем неверные состояния невозможными для
представления в программе
ˆ Выносим на уровень типов то, что имеет смысл для
нормальной работы программы
ˆ Если что-то можно статически гарантировать -
почему бы это не сделать?

И снова Martian Orbiter Disaster
ˆ Как такие ошибки происходят?
data Distance = Distance Decimal
-- Oops! Так можно сложить метры и ярды!
add :: Distance -> Distance -> Distance
add (Distance x) (Distance y) = Distance (x + y)

И снова Martian Orbiter Disaster (2)
newtype Metric = Metric { fromMetric :: Decimal }
newtype Imperial = Imperial { fromImperial :: Decimal }
data Distance a = Distance a
class Unit a where
fromValue :: a -> Decimal
toValue :: Decimal -> a
instance Unit Metric where ...
instance Unit Imperial where ...
add :: Unit a => Distance a -> Distance a -> Distance a
add (Distance x) (Distance y) = Distance wrapped
where wrapped = toValue added
added = fromValue x + fromValue y

Требования добавляются
ˆ Необходимо представить разные единицы измерения в
разных системах измерения
ˆ Необходимо уметь складывать единицы измерения в
пределах каждой из систем, в результате сложения
размерностью становится большая единица
ˆ Можно складывать дистанцию только в одинаковой
системе измерения

data Metric = Meter Decimal | Kilometer Decimal
addMetric :: Metric -> Metric -> Metric
addMetric = ...
data US = Inch Decimal | Yard Decimal
addUS :: US -> US -> US
addUS = ...
data Distance = MetricDistance Metric | USDistance US
-- ... см. 4.2

И снова Martian Orbiter Disaster (3.2)
safeAddDistance :: Distance
-> Distance
-> Maybe Distance
safeAddDistance (MetricDistance x) (MetricDistance y) =
Just (MetricDistance (addMetric x y))
safeAddDistance (USDistance x) (USDistance y) =
Just (USDistance (addUS x y))
safeAddDistance _ _ =
Nothing

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
-- Unit code skipped
data Measurement = MetricUnit | USUnit
data Distance :: Measurement -> * where
MetricDistance :: Metric -> Distance ’MetricUnit
USDistance :: US -> Distance ’USUnit
addDistance :: Distance a -> Distance a -> Distance a
addDistance (MetricDistance x) (MetricDistance y) = ...
addDistance (USDistance x) (USDistance y) = ...

Average
import Data.Foldable (sum)
average :: Fractional a => [a] -> a
average xs = sum xs / fromIntegral (length xs)

Обобщенный Average
average можно обобщить!
import Data.Foldable (sum, toList)
average :: (Fractional a, Foldable t) => t a -> a
average xs = sum xs / len
where len = fromIntegral . length . toList $ xs

Конкретизированный Average
Предыдущие реализации average вернут 0 от пустого
листа. Что если это неприемлимо? Что если пустой лист
уже является ошибкой?
import Data.Foldable (sum)
import qualified Data.List.NonEmpty as NE
-- data NonEmpty a = a :| [a]
average :: Fractional a => NE.NonEmpty a -> a
average xs = sum xs / NE.length xs

Функции на типах (1)
data family Array a
data instance Array Int =
IntArr UnboxedIntArr
data instance Array Bool =
BoolArr UnboxedBitVector
data instance Array (a,b) =
PairArr (Array a) (Array b)
data instance Array (Array a) =
ArrArr (Array Int) (Array a)

Функции на типах (2)
Servant
type HackageAPI =
"users" :> Get ’[JSON] [UserSummary]
:<|> "user" :> Capture "username" Username
:> Get ’[JSON] UserDetailed
:<|> "packages" :> Get ’[JSON] [Package]

Функции на типах + TH (acid-state)
type Key = String
type Value = String
data KeyValue = KeyValue !(Map.Map Key Value) deriving

Функции на типах + TH (acid-state) 2
insertKey :: Key -> Value -> Update KeyValue ()
insertKey key value = do
KeyValue m <- get
put (KeyValue (Map.insert key value m))
lookupKey :: Key -> Query KeyValue (Maybe Value)
lookupKey key = do
KeyValue m <- ask
return (Map.lookup key m)
$(makeAcidic ’’KeyValue [’insertKey])

Функции на типах + TH (acid-state) 2
main :: IO ()
main = do
...
update acid (InsertKey key val)
...

Есть ли минусы?
ˆ Вы все равно сможете писать отстойный код, даже с
хорошей системой типов. Градус остойности,
вероятно, будет ниже, но тем не менее.

Есть ли минусы?
ˆ Вы все равно сможете писать отстойный код, даже с
хорошей системой типов. Градус остойности,
вероятно, будет ниже, но тем не менее.
ˆ Не стоит думать что наиболее мощная система типов
подойдет для вашей задачи. Coq или Agda запросто
могут быть оверкиллом.

Какая система типов нужна вам?
Главный фактор - цена доказательства.
Что стоит больше для ваc/компании: отвергнутая
компилятором корректная программа или принятая
неверная?

Куда копать дальше
ˆ "Types and Programming Languages" и "Advanced
Topics in Types and Programming Languages" -
Benjamin C. Pierce
ˆ "Homotopy Type Theory" - Univalent Foundations
Program

Контакты
ˆ twitter: @rufuse
ˆ email: denis.redozubov@gmail.com
ˆ http://denisredozubov.com
ˆ Ссылка на слайды https://www.dropbox.com/s/
37l2pa2yek9qssm/TS-ruhaskell.ru.pdf?dl=0

�ݺ�ߣ

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

More Related Content

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