На этом шаге мы перечислим эти аксиомы.
Пусть знак "≡" обозначает семантическую эквивалентность фрагментов программного кода.
Существуют три аксиомы монад.
1. Аксиома согласованности операций return и (>>=):
return x >>= f ≡ f x
Другими словами, если выполнить монадное вычисление параметра с помощью функции return, то эффект будет таким же, как если бы параметр был просто передан второму вычислению.
2. Ассоциативность операции (>>=):
((x >>= f) >>= g) ≡ (x >>= (\y -> f y >>= g))
Другими словами, не нужно заботиться о расстановке скобок в последовательности операций (>>=).
3. Аксиома правой единицы:
x >>= return ≡ x
Можно переписать эту аксиому так:
x >>= \a -> return a ≡ x
Другими словами, связывание монадного вычисления x с вычислением, зависящим от параметра и просто-напросто возвращающим этот параметр, есть тождественная функция.
- Определение.
- Монадным вычислением x будем называть вычисление типа (m x).
На следующем шаге мы рассмотрим стандартные монады.
