edu-fp

# Функциональное программирование

## Лекция 4, 5

## Динамическая верификация. Тестирование. <br/> Статическая верификация. Типизация. Полиморфизм

Пенской А.В., 2024

----

## План лекции

- Верификация и валидация
- Динамическая верификация (тестирование)
    - Unit/Integration тесты. Test coverage. Качество тестов
    - Часто неизвестные методы тестирования
- Статическая верификация
    - Система типов
    - Indirection. Полиморфизм
    - Certified Programming. Proof by Tactics

Применимо как ФП, так и за его пределами.

---

## Валидация. Верификация

<dl>
  <dt> validation </dt>
  <dd>  checking the system to meet the needs of stakeholders </dd>
</dl>
 
<dl>
  <dt> verification </dt>
  <dd>  checking the system for compliance with a formalized requirements. </dd>
</dl>
 
</div><div class="col">

![](figures/v-model.png)

</div></div>

> Если отладка — процесс удаления ошибок, то программирование должно быть процессом их внесения. — Эдсгер Вибе Дейкстра

Наш фокус: Verification, Validation слишком мутная

----

## Подходы к верификации

- Динамическая, осуществляется через эксперимент.
    - Быстрая и простая проверка конкретного сценария.
    - Требует детерминированности системы.
    - Доказывает наличие ошибки, а не отсутствие.
- Статическая, осуществляется через анализ кода как текста/формул.
    - Работает со свойствами, а не примерами. Общий случай.
    - Трудоёмка (если возможна) в сложных случаях.

Минутка саморекламы: [2021, Open Dais: Software Verification on the ASIP CAD Example or How to Trust Your Team and Yourself](https://ryukzak.github.io/2021/04/29/software-verification-on-CAD-example.html), [2024, Функциональный уход за Research Pet Project: NITTA, CGRA, Haskell, верификация и тестирование](https://ryukzak.github.io/2024/07/11/nitta-verification.html)

---

## Динамическая верификация <br/> (by Experiment)

Тестирование:

- **Функциональное** $\longrightarrow$
- Нагрузочное
- Стресс-тестирование
- Cтабильности
- Безопасности
- Локализации
- Совместимости

</div><div class="col">

- **Компонентное (Unit)**
- **Интеграционное**
- Системное

--------------------

- Ручное (**REPL**)
- **Автоматизированное** (открытый список):
    - Doctests
    - Golden Master Testing
    - Dynamic Race Detections
    - Fuzzy/Monkey Testing
    - Property-Based Testing

</div></div>

----

### Read-Eval-Print-Loop (REPL)

Ручное тестирование, отладка, экспериментирование, разработка

![](figures/repl-lisp.png)

- Common Lisp, Smalltalk
- Clojure
- Erlang
- нет, не Python

[Bret Victor - Inventing on Principle](https://youtu.be/PUv66718DII?si=FWKgik6RLfu5DtNR)

</div><div class="col">

1. Консоль/интерпретатор
    - и компилируемые языки
1. Редактор $\leftrightarrow$ интепретатор
    - файл
    - выражение (expression)
1. Область видимости переменных
    - структурный блок
    - lexical scope (`let`, `where`)
    - замыкания
1. Hot Code Reloading
    - без остановки процессов
    - без потери состояния
1. Отладчик: инспекция и модификация состояния

</div></div>

---

## Автоматические тесты

- Unit/Integration тесты, их кол-во
- Test coverage. Качество тестов
- Часто неизвестные методы тестирования
- Тестирование на основе генераторов

![](figures/who-test-the-tests.jpg) 
![](figures/property-based-testing-vs-unit-testing.png)

----

### Unit-tests vs. Integration Tests

```python
def f1(a, b):
    return a / b

def f2(a, b):
    return a * b

def f1_2(a1, b1, a2, b2):
    return f1(a1, b1), f2(a2, b2)
```

- signed byte (from $-2^7$ to $2^7-1$, only $2^8$ values)
- `f1` and `f2` for full verification, we need to make $2^8+2^8 = 2^9$ asserts
- `f1_2` for full verification, it is necessary to make $2^{8+8} = 2^{16}$ asserts

Разные тесты решают **разные задачи**. Необходимо **дополнять**, а не заниматься "нецелевым использованием".

----

### Test coverage как показатель качества

```python
def f(a: bool, b: bool):
    lst = [1, 2]
    i = 0
    if a: i+=1
    if b: i+=1
    return lst[i]

assert f(False, False)
assert f(False, True)
assert f(True, False)
# here we have full test coverage for fucntion `f`
# but:
assert f(True, True)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 6, in f
IndexError: list index out of range
```

- Количество тестов и уровень покрытия $\neq$ качество тестирования.
- Лучший **уровень проверки** — вдумчивое белое тестирование, но:
    - высокая стоимость написания, поддержки,
    - как обеспечить/проверить "вдумчивость"?

---

### doctest

Описание функций включает:

- текстовое описание,
- примеры использования.

Сделаем примеры исполняемыми!

- дополнительные тесты,
- авт. проверка документации.

![](figures/doctest.png)

</div><div class="col">

```python
def factorial(n):
    """Return the factorial of n,
    an exact integer >= 0.

>>> [factorial(n) for n in range(6)]
    [1, 1, 2, 6, 24, 120]
    >>> factorial(-1)
    Traceback (most recent call last):
        ...
    ValueError: n must be >= 0
............................................
```

```shell
$ python -m doctest -v example.py
Trying:
    [factorial(n) for n in range(6)]
Expecting:
    [1, 1, 2, 6, 24, 120]
ok
```

```haskell
-- | 1 + 2 is 3.
-- >>> 1 + 2
-- 3
```

</div></div>

----

### Golden Master Testing

Как тестировать если результат:

- большой ($>$ экрана текста);
- нечитаем глазами, бинарный формат?

Golden Master Testing (Characterization Test):

1. Храним "золотой" результат работы как часть тестов.
2. Проверяем соответствие фактического и "золотого" результата.

В тестирование интерфейсов: Snapshot Testing

</div><div class="col">

![](figures/golden-tests.png)

</div></div>

---

### Fuzzy and Monkey Testing

Как снизить стоимость написания тестовых наборов данных?

- Генерировать тестовые данные (Fuzzy Testing) случаным образом.
- Генерировать последовательность событий (Monkey Testing) случаным образом (отказы, сбои, неожиданный порядок запросов).
- Проверять, **устояла ли** система под их воздействием.

![](figures/fuzzing.png) 
![](figures/chaos-monkey.jpg)

----

### Race Condition Detection

```go
func main() {
    i := 0
    go func() {
        i++        // main.go:7
    }()
    fmt.Println(i) // main.go:9
}
```

1. Перебор возможных трасс доступа к данным.
2. Поиск разницы между трассами.

</div><div class="col">

```shell
WARNING: DATA RACE
Write by goroutine 6:
  main.main.func1()
      /tmp/main.go:7 +0x44

Previous read by main goroutine:
  main.main()
      /tmp/main.go:9 +0x7e

Goroutine 6 (running) created at:
  main.main()
      /tmp/main.go:8 +0x70
```

</div></div>

![](figures/dynamic-race-detection.jpeg)

----

### Property-Based Testing

- Развитие идей Fuzzy/Monkey Testing
- Замена формального доказательства свойств на экспериментальное

Примеры свойств:

- Монойд $<S, *, 1>$:
    - $(a * b) * c = a * (b * c)$
    - $a * 1 = 1 * a = a$
    - e.g.: $<str, ++, "">$; $<set, \cup, \emptyset>$; $<A, \cap, A>$
- Раскраска и балансировка red-black tree.
- Тотальность (остановка, не выбрасывает исключение)
- Эквивалентность исходной и оптимизированной программы

</div><div class="col">

![](figures/pbt.png)

1. Генератор входных данных.
1. Функция проверки свойства (не использует тестируемое).
1. "Сжатие" входных данных, в случае нарушения свойств.

</div></div>

Notes: <https://yoan-thirion.medium.com/improve-your-software-quality-with-property-based-testing-70bd5ad9a09a>

----

#### Property-Based Testing. Примеры

```haskell
prop_revapp :: [Int] -> [Int] -> Bool
prop_revapp xs ys = reverse (xs ++ ys) == reverse xs ++ reverse ys
```

```haskell
import Test.QuickCheck
import Data.List (intersperse)

split :: Char -> String -> [String]
split c [] = []
split c xs = xs' : if null xs'' then [] else split c (tail xs'')
    where xs' = takeWhile (/=c) xs
          xs''= dropWhile (/=c) xs

unsplit :: Char -> [String] -> String
unsplit c = concat . intersperse [c]

prop_split_inv xs
    = forAll (elements xs) $ \c ->
        unsplit c (split c xs) == xs

main = quickCheck prop_split_inv
```

Видите ошибку? На каком входе всё ломается?

```haskell
split 'a' "a" = [""]
unsplit 'a' [""] = ""
```

Notes: <https://www.schoolofhaskell.com/user/pbv/an-introduction-to-quickcheck-testing>

----

#### Property-Based Testing. Не серебрянная пуля

```python
from hypothesis import given
import hypothesis.strategies as st

@given(st.integers(), st.integers())
def test_ints_are_commutative(x, y):
    assert x + y == y + x
```

```python
from hypothesis import given
import hypothesis.strategies as st

def bad_add(a, b):
    return 0

@given(st.integers(), st.integers())
def test_ints_are_commutative(x, y):
    assert bad_add(x, y) == bad_add(y, x)
```

---

## Статическая верификация <br/> (by Formal Analysis)

1. Синтаксис и семантика (ЯП)
2. Lint (плохие шаблоны)
3. **Систем типов** (IO, STM, lifetime, ADT)
4. Системы доказательства теорем. Certified programming
5. Temporal logic tools. Пример: SystemVerilog Assertions
6. Model-Driven Engineering. xtUML, Switch-технология. По построению

</div><div class="col">

![](figures/fp-avoid-bugs.png)

</div></div>

---

## Система типов

- Происхождение
- Объекты первого класса
- Виды системы типов
- Неявная статическая типизация. Вывод типов
- Тотальность функций
- Полиморфизм

----

### Типы в компьютере. Происхождение*

`*` — в основном неверное и неполное.

#### На уровне процессора

1. Машина фон Неймана. Типов нет, есть только действия.
   - Сказано — складывать, буду складывать.
   - Огромное количество ошибок и уязвимостей.
1. Тегированные ЭВМ, машинное слово: `<tag><actual-data>`:
   - безопасность (нет нецелевому использованию!),
   - приведение типов, полиморфизм,
       - типизация операций, кол-во аргументов,
   - накладные расходы,
   - ошибка — отказ?
1. Интерпретатор, ВМ: тоже самое.

Может не стоит писать ошибочный код?

---

### Indirection

**Indirection** (also called dereferencing) is the ability to reference something using a name, reference, or container instead of the value itself.

![](figures/c-pointer-multiple-indirection.jpg)
![](figures/indirections.jpg)

----

#### Объекты первого класса

Элементы ЯП делятся на:

- **first-class object**:
    1. All items can be the actual parameters of functions.
    2. All items can be returned as a result of functions.
    3. All items can be the subject of assignment statements.
    4. `*` All items can be tested for equality.
- **second-class objects** — все остальные.

</div><div class="col">

Примеры:

- значения, ссылки;
- указатели на функции;
- `*` функции, замыкания;
- метка для перехода;
- break/continue;
- `*` expressions, statements (if);
- namespace/module;
- тип (зависимые типы).

`*` — проблема определения и проверки.

</div></div>

---

#### Типизация на уровне языка. Происхождение*

1. Фиксируем типы на уровне документации и сверяемся с ней.
1. Все типы известны. Имя функции включает аргументы/их типы:
    - `sort/1`, `sort/2`;
    - `ifTrue:`, `ifTrue:ifFalse:`, `ifFalse:`, `ifFalse:ifTrue:`
    - `int add(int, int)`, `float add(float, float)`
    - простейшая реализация через глобальный словарь.
1. Обобщённое программирование:
    - массивы в C — синтаксический сахар поверх машины фон Неймана;
    - параметризируемые типы — generics;
    - динамическая диспетчеризация — интерфейсы.
1. Ограничения, вывод типов, поиск поддходящих вариантов.

----

### Виды системы типов

<dl>
  <dt> Система типов </dt>
  <dd>  совокупность правил в языках программирования, назначающих свойства, именуемые типами, различным конструкциям, составляющим программу — таким как переменные, выражения, функции или модули. </dd>
</dl>
 
</div><div class="col">

![](figures/type-system-classification.png)

Наш акцент: статическая, строгая.

</div></div>

- Время: статическая $\longleftrightarrow$ динамическая
- Сила: сильная $\longleftrightarrow$ слабая

----

## Система типов и множества (поверхностно)

- Singletons: $A = \\{ a \\}$,  $B = \\{ b \\}$
- $Boolean=\\{ true, false \\}$
- Natural: $ N = \\{ 1, 2... \\}$ (определены на уровне железа)
- `enum {a, b}`
    - $=\\{ a, b \\}$
- `struct { A, B }`
    - $=A \times B= \\{ (a, b) \\}$
- `union { A, B }`
    - $= A \cup B = \\{ a, b \\}$

----

- Generics: `class Box<T>{T value;}`
    - $\equiv$ `data Box a = Box a`
    - $\equiv box(T) = T \times \\{ box \\}$
- Disjoint union: `data Either a b = Left a | Right b`
    - $\equiv either(A,B) = ( A \times \\{ left \\} ) \cup ( B \times \\{ right \\} )$
- Recursive type: `data List a = Cons a (List a) | Nil`
    - $\equiv list(A) = (A \times list(A) \times \\{ cons \\}) \cup \\{ nil \\}$
- `data Maybe a = Just a | Nothing`
    - $\equiv maybe(A) = (A \times \\{ just \\}) \cup \\{ nothing \\}$
    - `fromMaybe` — unbox;
    - `int->int->int` — use.
- `int?`$=N \cup \\{ nil \\}$
    - `int?->int?->int?`
        - run-time exception
        - cast `nil` to `0` or `1`
        - `nil` propagate `nil` (`nil + x = nil = x + nil`)

----

### Неявная статическая типизация

<dl>
  <dt> Вывод типов (type inference) </dt>
  <dd>  в программировании, у компилятора есть возможность самому логически вывести тип значения у выражения. </dd>
</dl>
 
![](figures/static-vs-dynamic-types.jpg)

</div><div class="col">

```go
func main() {
 var x float32 = 123.78
 y := 23
 fmt.Printf("%T", y + x)
} // invalid operation: y + × (mismatched types int and float32)
```

```go
func main() {
 var x float32 = 123.78
 y := 23 + x
 fmt.Printf("%T", y)
} // float32
```

```haskell
map f [] = []
map f (x:xs) = f x : map f xs
-- map :: _ -> _ -> _
-- map :: _ -> [_] -> _
-- map :: _ -> [_] -> [_]
-- map :: (_ -> _) -> [_] -> [_]
-- map :: forall a.
--        (a -> _) -> [a] -> [_]
-- map :: forall a b.
--        (a -> b) -> [a] -> [b]
```

</div></div>

----

### Тотальность функций

<dl>
  <dt> Тотальность (total function) </dt>
  <dd>  функция, определенная для всех возможных входных данных. </dd>
</dl>
 
Примеры:

```haskell
(/) :: Int -> Int -> Int
_ / 0 = error "divide on ZERO"
a / b = ...
```

`head` — взятие головы от списка. Варианты типизации:

```haskell
head1 :: [a] -> a
head2 :: [a] -> Maybe a
head3 :: NonEmpty a -> a
head4 :: [a] -> a + {nil}
```

[Maybe Not - Rich Hickey](https://www.youtube.com/watch?v=YR5WdGrpoug)

---

## Пример проблемы интерпретации типов

Из описания формата JSON:

```text
number
    integer fraction exponent

integer
    digit
    onenine digits
    '-' digit
    '-' onenine digits

digits
    digit
    digit digits

digit
    '0'
    onenine
```

</div><div class="col">

```text
onenine
    '1' . '9'

fraction
    ""
    '.' digits

exponent
    ""
    'E' sign digits
    'e' sign digits
```

</div></div>

Что такое number?

----

### Что такое number в JSON?

`number` может быть: `short`, `int`, `long`, `big-int`, `float`, `double`

### Контекст

- JavaScript — старая экосистема, разработанная для автоматизации веба "на коленке".
    - Следствие: работа с `number` как с `long` в большинстве решений.
- Haskell — язык, сделанный любителями и профессионалами от математики.
    - Следствие 1: есть `Integer` без ограничения диапазона значений.
    - Следствие 2: библиотека Aeson (стандарт для работы с JSON) интерпретирует `number` как `Integer`.
- Crypto & Blockchain mess — активное использование ключей.
    - Следствие: числа в 256 бит не предел.

----

#### Проблема

- Передача JSON из Haskell в веб.
- Сериализация `Integer` в `number` формирует очень длинное число, которое парсится в `long`.
- Hash перестаёт совпадать.

#### Решение

- предобработка текста JSON с заменой всех больших `number` на специальную строку;
- постобработка структуры с JSON с возвращением всех `number` к истинным значениям.

---

### Behavior Indirection: Polymorphism

The key control flows indirection is a polymorphism. It allows developers to write code with indirection references to its implementation.

<dl>
  <dt> Polymorphism in programming </dt>
  <dd>  is the ability to use different software entities (objects, data types, and so on) with the same interface in the same context. </dd>
</dl>
 
</div><div class="col">

![](figures/polymorphism.png)

</div></div>

----

### Виды полиморфизма

1. **Универсальный** (universal)
    1. Параметрический (parametric) — обощённые структуры и код, любые данные внутри.
    1. Наследование (subtyping) — ООП, использование наслед.
1. **Специальный** (ad-hoc)
    1. Перегрузка (overloading)
        - Ограниченный (bounded)
        - Перегрузка имён функций (func. names overloading)
    1. Приведение типов (coercion)

</div><div class="col">

![](figures/me-fp-oop.png)

Частично заимствовано тут:

- [Haskell Beginners 2022. <br/> Lecture 3: Typeclasses](https://slides.com/haskellbeginners2022/lecture-3)
- [Душкин Роман <br/> Полиморфизм в языке Haskell](https://fprog.ru/2009/issue3/roman-dushkin-haskell-polymorphism/)

</div></div>

---

### Universal. Один код, разные данные

```haskell
filterInt :: (Int -> Bool) -> [Int] -> [Int]
filterInt _ [] = []
filterInt p (x:xs)
    | p x = x : filterInt p xs
    | otherwise = filterInt p xs
```

```haskell
filterChar :: (Char -> Bool) -> [Char] -> [Char]
filterChar _ [] = []
filterChar p (x:xs)
    | p x = x : filterChar p xs
    | otherwise = filterChar p xs
```

----

#### Динамика

```python
lst = [
    {'x': 1, 'y': 3, 'z': 7},
    {'x': 2, 'y': 2, 'z': 8},
    {'x': 3, 'y': 1, 'z': 1},
]
sorted(lst, key=lambda e: e['x'])
# => [ {'x': 1, 'y': 3, 'z': 7}
#    , {'x': 2, 'y': 2, 'z': 8}
#    , {'x': 3, 'y': 1, 'z': 1}]
sorted(lst, key=lambda e: e['y'])
# => [ {'x': 3, 'y': 1, 'z': 1}
#    , {'x': 2, 'y': 2, 'z': 8}
#    , {'x': 1, 'y': 3, 'z': 7}]
```

</div><div class="col">

1. The first element of a pair
1. Reversing a list
1. List length
1. Taking 5 elements from a list
1. Function composition
1. etc.

</div></div>

----

#### Параметрический (parametric) полиморфизм /1

```haskell
filter :: forall a. (a -> Bool) -> [a] -> [a]
filter _ [] = []
filter p (x:xs)
    | p x = x : filter p xs
    | otherwise = filter p xs

-- TypeApplications: @
filter @Int :: (Int -> Bool) -> [Int] -> [Int]
filter @String :: (String -> Bool) -> [String] -> [String]
```

----

#### Параметрический (parametric) полиморфизм /2

```haskell
data Maybe a = Just a | Nothing
type MaybeInt = Maybe Int
```

```java
public class Box<T> {
    private T t;
    public void set(T t) { this.t = t; }
    public T get() { return t; }
}
```

----

#### Неприятные ограничения

```haskell
normalize :: String -> String
normalize = show . read

normalize :: forall a. (Read a, Show a) => String -> String
normalize s =
  let v :: a
      v = read s
     in show v

normalize @Int "123"
```

---

### Один интерфейс, разный код

```python
class Dog():
    def __init__(self, name):
        self.name = name

def dogSay(self):
        return 'Bork'
```

```python
class Cat():
    def __init__(self, name):
        self.name = name

def catSay(self):
        return 'Meow'
```

</div><div class="col">

```lisp
(defclass dog ()
  ((name :initarg :name)))

(defun dogSay (dog) 'bork)
```

```lisp
(defclass cat ()
  ((name :initarg :name)))

(defun catSay (cat) 'meow)
```

</div></div>

----

#### Universal. <br/> Наследование (subtyping) полиморфизм /1

```python
class Pet():
    def __init__(self, name):
        self.name = name

def say(self):
        raise NotImplemented()

class Dog(Pet):
    def say(self):
        return 'Bork'

class Cat(Pet):
    def say(self):
        return 'Meow'
```

</div><div class="col">

```lisp
(defgeneric say (obj))

(defmethod say ((obj dog)) 'bork)
(defmethod say ((obj cat)) 'meow)

(defvar pets
  (list
    (make-instance 'dog :name "Patric")
    (make-instance 'cat :name "Snowball")))

(loop for pet in pets
      collect (say pet)) ; => (BORK MEOW)
```

</div></div>

----

#### Universal. <br/> Наследование (subtyping) полиморфизм /2

```python
class MyInt(int):
    def __init__(self, x):
        self.value = x
    def __lt__(self, other): # reversed!
        return other.value < self.value

sorted([7, 8, 1]) # => [1, 7, 8]
sorted([MyInt(7), MyInt(8), MyInt(1)]) # => [8, 7, 1]
```

----

#### Universal. <br/> Наследование (subtyping) полиморфизм /3 <br/> If-Statement in Smalltalk

<div>

```smalltalk
Bool subclass: #Object !

True subclass: #Bool
  ifTrue: aBlock ifFalse: bBlock
    ^ aBlock value ! !

False subclass: #Bool
  ifTrue: aBlock ifFalse: bBlock
    ^ bBlock value ! !
```

</div><div class="col">

```smalltalk
(17 * 13 > 220).
>>>true
"17.add(13).more(220) => True"

(17 * 13 > 220)
       ifTrue: [ 'bigger' ]
       ifFalse: [ 'smaller' ].
>>>'bigger'
"17.add(13).more(220)
   .ifTrueIfFalse(
     lambda: 'bigger',
     lambda: 'smaller' ) => 'bigger'"

n := 1.
[ n < 1000 ] whileTrue: [ n := n*2 ].
n
>>> 1024
```

</div></div>

</div>

---

### Одинаковый вызов, разные интерфейсы

```java
class Sum {
    public static int intSum(int x, int y) {
        return (x + y);
    }
    public static double doubleSum(double x, double y) {
        return (x + y);
    }
    public static void main(String args[]) {
        System.out.println(Sum.intSum(10, 20));
        System.out.println(Sum.doubleSum(10.5, 20.5));
    }
}
```

----

#### Ad-Hoc. Перегрузка имён функций (overloading)

```java
public class Sum {
    public static int sum(int x, int y) {
        return (x + y);
    }
    public static double sum(double x, double y) {
        return (x + y);
    }
    public static void main(String args[]) {
        System.out.println(Sum.sum(10,   20  ));
        System.out.println(Sum.sum(10.5, 20.5));
    }
}
```

----

### Разные типы, один оператор

```python
print("number: " + str(42))  # => number: 42
print(1.5 + float(1))        # => 2.5
print(1 + 1 + int('1'))      # => 3
print(int('1') + 1 + 1)      # => 3
```

#### Ad-Hoc. Приведение типов (coercion)

```javascript
console.log("number: " + 42) // => number: 42
console.log(1.5 + 1)         // => 2.5
console.log(1 + 1 + '1')     // => 21
console.log('1' + 1 + 1)     // => 111
```

Как это реализовать без поддержки со стороны языка?

----

#### Multiple Dispatch (Julia)

```julia
add(x::Int64,  y::Int64)  = x + y
add(x::Int64,  y::String) = x + parse(Int64, y)
add(x::String, y::Int64)  = parse(Int64, x) + y
add(x::String, y::String) = parse(Int64, x) + parse(Int64, y)

add(1,   41  ) # => 42
add(1,   "41") # => 42
add("1", 41  ) # => 42
add("1", "41") # => 42
add(1,   41.0) # => ?
```

```julia
# => ERROR: MethodError: no method matching add(::Int64, ::Float64)
#    Closest candidates are:
#      add(::Int64, ::Int64) at REPL[45]:1
#      ...
```

----

#### Multiple Dispatch (Common Lisp)

```lisp
(defgeneric add (x y)
  (:method (x y)
    (error "method undefined")))

(defmethod add ((x integer) (y integer)) (+ x y))
(defmethod add ((x integer) (y string) ) (+ x (parse-integer y)))
(defmethod add ((x string)  (y integer)) (+ (parse-integer x) y))
(defmethod add ((x string)  (y string) ) (+ (parse-integer x) (parse-integer y)))

(add 1   2  ) ; => 3
(add 1   "2") ; => 3
(add "1" 2  ) ; => 3
(add "1" "2") ; => 3
(add 1.0 2  )
; => debugger invoked on a SIMPLE-ERROR in thread
;    #<THREAD "main thread" RUNNING {1001560143}>:
;      method undefined
;     ...
```

---

### Один код, разные данные с ограничениями

#### Ad-Hoc. Ограниченный (bounded) полиморфизм

```haskell
maxInt :: Int -> Int -> Int
maxInt x y = if x > y then x else y
```

```haskell
maxChar :: Char -> Char -> Char
maxChar x y = if x > y then x else y
```

```haskell
max :: forall a. Ord a => a -> a -> a
max x y = if x > y then x else y
```

----

#### Type Class

<dl>
  <dt> Type class </dt>
  <dd>  is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T. </dd>
</dl>
 
```haskell
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool

class (Eq a) => Ord a where
    compare :: a -> a -> Ordering
```

----

##### Proposal: Remove method `/=` from class `Eq`

```haskell
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
```

```haskell
class Eq a where
  (==) :: a -> a -> Bool

a /= b = not (a == b)
```

Ваше мнение?

[link](https://github.com/haskell/core-libraries-committee/issues/3)

----

#### Reference Transperency vs. Type Classes

```haskell
data Maybe a = Just a | Nothing
```

```haskell
isNothingL Nothing = True
isNothingL _       = False
```

</div><div class="col">

```haskell
isNothingR a
  | a == Nothing = True
isNothingR _     = False
```

</div></div>

Сравните эти две реализации?

<div>

```haskell
isNothingL :: _ -> _
isNothingL :: Maybe _ -> Bool
isNothingL :: forall a. Maybe a -> Bool
```

</div><div class="col">

```haskell
instance Eq a => Eq (Maybe a) where
    Nothing == Nothing = True
    Just  a == Just  b = a == b
    _       == _       = False

isNothingR :: _ -> _
isNothingR :: Maybe _ -> Bool
isNothingR
  :: forall a. Eq (Maybe a) => Maybe a -> Bool
isNothingR
  :: forall a. Eq a => Maybe a -> Bool
```

</div></div>

</div>

----

#### Экзистенциальные типы

Тип скрывающий переменную типа с заданными ограничениями.

```haskell
xs = [1, "1", 'c']
-- => <interactive>:4:14: error:
--      • Couldn't match type ‘Char’ with ‘[Char]’
--        Expected: String
--          Actual: Char
--      • In the expression: 'c'
--        In the expression: [1, "1", 'c']
--        In an equation for ‘xs’: xs = [1, "1", 'c']

data Obj = forall a. (Show a) => Obj a
xs = [Obj 1, Obj "foo", Obj 'c']

doShow :: [Obj] -> String
doShow [] = ""
doShow ((Obj x):xs) = show x ++ doShow xs
doShow xs  -- => 1"foo"'c'

instance Show Obj where show (Obj x) = show x
show xs    -- => [1,foo",'c']
```

---

## Certified Programming

Задача: разработка программного обеспечения со строго доказанными свойствами для всех входных данных.

Пример свойств:

- выполнение базовых свойств типов данных, к примеру свойства Моноида:
    - $S$ — множество элементов;
    - $*$ — бинарная операция отображения $S x S \rightarrow S$;
    - Associativity: `$(a*b)*c=a*(b*c)$`
    - Identity element: `$\exists e \in S : \forall a \in S :e*a=a*e=a$`
- алгоритм останавливается;
- эквивалентность программного кода до и после рефакторинга.

----

### Подходы к Certified Programming

1. Зависимые типы (англ. dependent type) в информатике и логике — тип, который зависит от некоторого значения.

Пример:

```agda
    data Vec (A : Set) : Nat -> Set where
        []   : Vec A zero
        _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
    head (x :: xs) = x

vmap : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
    vmap f [] = []
    vmap f (x :: xs) = f x :: vmap f xs
    ```

1. Доказательство теорем как в математике (см. далее).

---

### Coq, Proof by Tactics

#### Bool and neg

```coq
Inductive bool : Type :=
  | true
  | false.

Definition neg (b : bool) : bool :=
  match b with
    | true => false
    | false => true
  end.

Example neg_false: neg false = true.
Proof.
        (* 1 goal
        ______________________________________(1/1)
        neg false = true *)
simpl.
        (* 1 goal
        ______________________________________(1/1)
        true = true *)
reflexivity. Qed.
```

----

#### Theorem: `neg (neg x) = x`

```coq
Theorem neg_neg_is_id : forall b : bool, neg (neg b) = b.
Proof.
        (* 1 goal
        ______________________________________(1/1)
        forall b : bool, neg (neg b) = b *)
intros b.
        (* 1 goal
        b : bool
        ______________________________________(1/1)
        neg (neg b) = b *)
destruct b.
        (* 2 goals
        ______________________________________(1/2)
        neg (neg true) = true
        ______________________________________(2/2)
        neg (neg false) = false *)
- simpl. reflexivity.
        (* 1 goal
        ______________________________________(1/1)
        neg (neg false) = false *)
- simpl. reflexivity. Qed.
```

----

#### natlist, notation and app

```coq
Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Notation "[ ]" := nil.
Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).

Example list_cons: 1 :: [] = cons 1 [].
Proof. reflexivity. Qed.

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Example list_notation: [1; 2] = 1 :: 2 :: [].
Proof. reflexivity. Qed.

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | h :: t => h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).
```

----

#### Theorem: natlist associativity

```coq
Theorem natlist_assoc : forall a b c : natlist,
  (a ++ b) ++ c = a ++ (b ++ c).
Proof. intros a b c.
        (* 1 goal
        a, b, c : natlist
        ______________________________________(1/1)
        (a ++ b) ++ c = a ++ b ++ c *)
induction a.
        (* 2 goals
        b, c : natlist
        ______________________________________(1/2)
        ([ ] ++ b) ++ c = [ ] ++ b ++ c
        ______________________________________(2/2)
        ((n :: a) ++ b) ++ c = (n :: a) ++ b ++ c *)
- simpl.
        (* 2 goals
        b, c : natlist
        ______________________________________(1/2)
        b ++ c = b ++ c
        ______________________________________(2/2)
        ((n :: a) ++ b) ++ c = (n :: a) ++ b ++ c *)
  reflexivity.
        (* 1 goal
        n : nat
        a, b, c : natlist
        IHa : (a ++ b) ++ c = a ++ b ++ c
        ______________________________________(1/1)
        ((n :: a) ++ b) ++ c = (n :: a) ++ b ++ c *)
```

(continue on the next page)

----

```coq
        (* 1 goal
        n : nat
        a, b, c : natlist
        IHa : (a ++ b) ++ c = a ++ b ++ c
        ______________________________________(1/1)
        ((n :: a) ++ b) ++ c = (n :: a) ++ b ++ c *)
- simpl.
        (* 1 goal
        n : nat
        a, b, c : natlist
        IHa : (a ++ b) ++ c = a ++ b ++ c
        ______________________________________(1/1)
        n :: (a ++ b) ++ c = n :: a ++ b ++ c *)
  rewrite -> IHa.
        (* 1 goal
        n : nat
        a, b, c : natlist
        IHa : (a ++ b) ++ c = a ++ b ++ c
        ______________________________________(1/1)
        n :: a ++ b ++ c = n :: a ++ b ++ c *)
  reflexivity. Qed.
```