maybe : ∀ a b. b -> (a -> b) -> Maybe a -> b
Такие типы называются в теории типов “универсально квантифицированными”. Это название происходит из логики, где ∀ называется квантором всеобщности или квантором универсальности.
Синтаксис Haskell по умолчанию опускает объявление переменных типа:
Рассмотрим объявление Maybe
:
Невозможен без параметрического полиморфизма.
Типизация чистых λ-термов:
tru = λ x y. x
tru : ∀ a b. a -> b -> a
Алгебраическими типами называются типы, поддерживающие “алгебраические” операции, а именно “сложение” и “умножение”.
Более формально, мы вводим бинарные конструкторы ×
и +
, и определяем операции проекции:
fst : A × B -> A
snd : A × B -> B
и операцию case
:
case x of
left l -> v1
right r -> v2
где x : A + B
, l : A
, r : B
и v1 : T
, v2 : T
.
В рамках синтаксиса Haskell:
тип-произведение – пары (A, B)
, кортежи (A, B, C)
и т.д.
Проекции
Конструкторы значений: (,)
, (,,)
и т.д. Поддерживается синтаксис вида (x, y, z)
.
Haskell поддерживает пользовательские типы. Они могут быть типами-произведениями или типами-суммами, например:
или
Для облегчения работы с типами-произведениями – записи. Вводят тип-произведение вместе с проекциями. В случае Haskell:
Более конкретный пример:
Специальный синтаксис для значений:
Эквивалентно:
Сила алгебраических типов становится более явной, если ввести единичный тип. Это тип, который имеет ровно одно значение.
В теории типов – unit : Unit
.
В Haskell – () :: ()
.
На основе единичного типа и конструкторов суммы и произведения можно построить в принципе любой тип.
При параметрическом полиморфизме, определение функции остаётся одинаковым для всех типов.
Например:
Класс типов (так же известный как typeclass) – некий абстрактный интерфейс, которому должны удовлетворять все типы (конкретные и полиморфные), входящие в класс.
Классы типов – открытое множество, новые типы могут быть добавлены в класс “на лету”.
Добавление типов в класс производится объявлением реализации интерфейса класса (экземпляра) для какого-то типа (конкретного или полиморфного).
Один из простейших классов типов.
Соответствует множеству типов, для которых реализована операция сравнения.
Так могла бы выглядеть реализация экземпляра для типа Bool
:
Классы типов ограничивают универсальную квантификацию. Например, функция lookup
:
lookup :: (Eq a) => a -> [(a,b)] -> Maybe b
lookup _ [] = Nothing -- в пустом списке нет значений
lookup key ((x,y):xys) -- в непустом списке, берём первую пару
| key == x -- если искомый ключ равен первому элементу пары
= Just y -- возвращаем второй элемент пары (обёрнутый в Just)
| otherwise -- в противном случае
= lookup key xys -- рекурсивно просматриваем остаток списка
(реализация из стандартной библиотеки)
Можно указывать несколько ограничений через запятую.
Ограничения при объявлении экземпляров класса:
На практике, подобные определения компилятор GHC способен вывести самостоятельно. Для этого при объявлении типа используется директива deriving
:
Ограничение при объявлении класса типа:
class Eq a => Ord a where
compare :: a -> a -> Ordering
(<) :: a -> a -> Bool
(<=) :: a -> a -> Bool
(>) :: a -> a -> Bool
(>=) :: a -> a -> Bool
max :: a -> a -> a
min :: a -> a -> a
Любой тип в классе Ord
таким образом должен быть и в классе Eq
.
class Eq a => Ord a where
compare :: a -> a -> Ordering
(<) :: a -> a -> Bool
(<=) :: a -> a -> Bool
(>) :: a -> a -> Bool
(>=) :: a -> a -> Bool
max :: a -> a -> a
min :: a -> a -> a
Минимальное определение: либо (<=)
, либо compare
.
Любой тип в строку
Чтение значения из строки, полученной через show
.
Для удобства:
Безопасные варианты (модуль Text.Read
):
Использование функции read
иногда требует явного указания типа результата:
Prelude> read "4"
*** Exception: Prelude.read: no parse
Prelude> read "4" :: Int
4
Аналогичная проблема — show . read
– имеет тип String -> String
, недостаточно контекста для выбора экземпляров Read
и Show
.
Перечислимые типы
Ограниченные типы
Численные типы
Другие интересные численные классы: Real
, Integral
, Fractional
, Floating
, RealFrac
и RealFloat
. Краткий обзор в конспектах лекций.
Полугруппы
Моноиды
Типовый пример моноида – список.
Одна из основополагающих концепций в чистых ФЯП – монады.
Понятие из теории категорий.
С практической точки зрения, монада – это класс типов.
Начнём с понятия функтора.
--- списки
1 <$ [x,y,z] == [1,1,1]
1 <$ [] == []
-- Maybe a = Nothing | Just a
1 <$ Just x == Just 1
1 <$ Nothing == Nothing
-- etc
Формально,
Все экземпляры класса Functor
должны удовлетворять законам функтора:
fmap id == id
fmap (f . g) == fmap f . fmap g
Дополнительно вводится
символизирует применение функции “под функтором”.
Любой экземпляр Applicative
должен соблюдать следующие законы:
Следствие – согласованность с функтором:
Пример:
Дополнительно определяются функции
(<*>)
можно определить через liftA2
:
Аналогично:
class Applicative m => Monad (m :: * -> *) where
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
В основном интересует оператор (>>=)
(“рыбий хвост”, чаще просто оператор связывания), прочие – из Applicative
.
Использование связывания:
do-нотация – сахар для монад:
Эквивалентно
Самая часто встречающаяся монада – IO
.
Если объяснения в рамках этого конспекта недостаточно наглядные, имеет смысл ознакомиться со следующими материалами:
class Foldable (t :: * -> *) where
fold :: Monoid m => t m -> m
foldMap :: Monoid m => (a -> m) -> t a -> m
foldr :: (a -> b -> b) -> b -> t a -> b
foldr' :: (a -> b -> b) -> b -> t a -> b
foldl :: (b -> a -> b) -> b -> t a -> b
foldl' :: (b -> a -> b) -> b -> t a -> b
foldr1 :: (a -> a -> a) -> t a -> a
foldl1 :: (a -> a -> a) -> t a -> a
toList :: t a -> [a]
null :: t a -> Bool
length :: t a -> Int
elem :: Eq a => a -> t a -> Bool
maximum :: Ord a => t a -> a
minimum :: Ord a => t a -> a
sum :: Num a => t a -> a
product :: Num a => t a -> a
{-# MINIMAL foldMap | foldr #-}
Определён в Data.Foldable
. Основные экземпляры – списки, Maybe
, Either a
и (,) a
Пара примеров:
Prelude> sequenceA [Just 1, Just 2]
Just [1,2]
Prelude> sequenceA [Just 1, Just 2, Nothing]
Nothing
Prelude> sequenceA (Just [1, 2])
[Just 1,Just 2]
Prelude> sequenceA Nothing
Nothing