Практика 4. Введение в Haskell

Почему Haskell

• NB Совет: непонятное редуцируйте руками на простом примере, а чтобы осознать что-то — реализуйте это самостоятельно

λ-исчисление ↔︎ Haskell

Техника аккумулирующего параметра

fac' n = go 1 n
  where
    go acc n'
      | n' <= 1 = acc
      | otherwise = go (acc * n') (n' - 1)

Злополучный Фибоначчи

• Реализация по определению имеет экспоненциальную сложность

fib :: Int -> Int
fib n = go 1 1 n
  where
    go prev curr n'
      | n' <= 1 = ________
      | otherwise = go ________ ____________ (n' - 1)

    go prev curr n'
      | n' <= 1 = prev
      | otherwise = go curr (prev + curr) (n' - 1)

Расставьте скобки

infixr 9 .
infixr 8 ^
infixl 7 *
infixl 6 +, -
infixr 0 $
-- применение функции сильнее любого оператора и группируется влево

Конструирование реализаций

($) :: (a -> b) -> a -> b
(&) :: a -> (a -> b) -> b
(.) :: (b -> c) -> (a -> b) -> a -> c
f :: Int -> a -> a
g :: Int -> Double
h :: Int -> Double -> Int

example x = f 1 $ g $ h 2 x          -- (а)
example x = (f 1 . g . h 2) x        -- (б)
example   = f 1 . g . h 2            -- (в): η-шаг
example x = x & h 2 & g & f 1        -- (г): слева направо, как конвейер
example x = let x1 = h 2 x in
            let x2 = g x1 in
            f 1 x2                   -- (д): именуем промежуточные вычисления

Предскажите тип

• Типы с маленькой буквы — типовые переменные
• Могут принимать разные значения в зависимости от контекста

Предскажите тип

const :: a -> b -> a
flip  :: (a -> b -> c) -> b -> a -> c

Читаем сообщения GHC

ghci> :t const True 'a' 'b'
error: [GHC-83865]
    • Couldn't match expected type ‘Char -> t’ with actual type ‘Bool’
    • In the first argument of ‘const’, namely ‘True’
      In the expression: const True 'a' 'b'

Типовые дыры

В П3 мы населяли тип композиции, ставя дырку \square и подписывая её тип. В Haskell дырка — это _, и её тип подписывает компилятор.

compose :: (b -> c) -> (a -> b) -> a -> c
compose f g x = _

• Found hole: _ :: c
• Relevant bindings include
    x :: a
    g :: a -> b
    f :: b -> c

Населяем тип по шагам

compose :: (b -> c) -> (a -> b) -> a -> c
-- контекст:  f :: b -> c,   g :: a -> b,   x :: a

Что вы теперь умеете

• Читать Haskell как λ-исчисление с типами: \x -> M, a -> b, const — это \mathbf{K}
• Судить о рекурсивной функции: завершается ли она и что копится, пока она считает
• Писать рекурсию с аккумулятором
• Собирать функции через $ и . и убирать точку η-шагом
• Предсказывать тип выражения и переводить сообщение компилятора
• Строить функцию по её типу, спрашивая компилятор дырками

В следующих сериях: сегодня все данные были числами и парами — дальше соберём собственные типы данных

Что нового в инструментах ⚙

• Домашка 4 живёт в знакомом шаблоне, но make repl теперь открывает GHCi с вашим кодом на Haskell
• В GHCi: :t — тип выражения, :i — сведения об имени и приоритет оператора, :r — перечитать файл после правки
• make check перед тестами запускает линтер hlint
• NB Линтер на этом курсе обязателен: его подсказки учат идиомам языка
• NB Форматтер на этом курсе запрещён: он переписывает файл целиком, а нам нужны минимальные диффы

Компилятор GHC ⚙

• Единственный компилятор Haskell
• Язык развивается в основном расширениями компилятора
  • Подключение прагмой в начале файла {-# LANGUAGE ... #-}
  • Или ключами компиляции (в конфигах проекта)
  • Добавляют синтаксический сахар (LambdaCase, ImplicitParams)
  • Обогащают систему типов (RankNTypes)
  • Добавляют фичи (MultiParamTypeClasses, GADTs)
  • Добавляют экспериментальные фичи (LinearTypes)
• https://ghc.gitlab.haskell.org/ghc/doc/users_guide/index.html

Системы сборки ⚙

• По конфигурации проекта правильно вызывают компилятор

Cabal — Common Architecture for Building Applications and Libraries

• Система сборки + библиотека; на этом курсе пользуемся ей
• Компилятор нужной версии ставит ghcup, версия записана в cabal.project
• cabal build — собрать проект
• cabal test — запустить тесты
• cabal repl — REPL с загруженным проектом
• В домашках эти команды завёрнуты в make build, make check, make repl

Stack — надстройка над cabal, которая сама скачивает компилятор; встретится в чужих проектах

REPL, GHCi ⚙

REPL (read-eval-print-loop)

Интерактивное окружение, исполняющее вводимые в него высказывания и тут же демонстрирующее результат.

• Компилятор работает долго, а GHCi — быстро
• Пишем код, загружаем в интерпретатор: make repl
• Основные возможности
  • Исполнить выражение
  • :r (reload) — перезагрузить интерпретатор
  • :t (type) — посмотреть тип выражения
  • :i (info) — посмотреть документацию функции, приоритет оператора
  • :set — установить расширения языка и флаги компиляции

Другие тулы ⚙

• Линтер (hlint) помогает находить ошибки в программах
• Очень помогает в обучении
• NB На этом курсе обязателен к использованию!
• Форматтер автоматически форматирует код: ormolu, fourmolu
• Обязателен к использованию во многих языках: экономит время и повышает консистентность кода
• В Haskell не всегда удовлетворительно работает
• NB На этом курсе запрещён: он переписывает файл целиком, а нам нужны минимальные диффы

LSP ⚙

• LSP — Language Server Protocol — это протокол взаимодействия между движками IDE и текстовыми редакторами
• Есть language server для большинства языков
• Есть для Haskell, работает только для той же версии ghc
• Большинство редакторов кода поддерживает LSP и с его помощью почти превращается в IDE

IDE для Haskell на примере vscode

• Ставите haskell-language-server через ghcup — он подберёт сборку под ваш компилятор
• Устанавливаете в систему hlint
• Ставите плагины: Haskell (может поставить и остальные), Haskell Syntax

Полиморфные функции ✱

• ✱ То, что типизация остаётся валидной после подстановки в тип — теорема метатеории

  Лемма подстановки типа для \lambda_\to

  \begin{array}{ll} \Gamma\vdash M : A \Rightarrow [\alpha\mapsto B]\ \Gamma\vdash \phantom{[\alpha\mapsto B]\ }M : [\alpha\mapsto B]\ A & {\color{blue}(\lambda_\to \text{ по Карри})} \\ \Gamma\vdash M : A \Rightarrow [\alpha\mapsto B]\ \Gamma\vdash {\color{red}[\alpha\mapsto B]\ }M : [\alpha\mapsto B]\ A & {\color{red}(\lambda_\to \text{ по Чёрчу})} \end{array}

• Если мы в языке разрешим приписывать типы термам, мы потеряем гибкость:

  \begin{array}{l} \mathbf{K} : \alpha \to \beta \to \alpha \\ \mathbf{K}\ \mathtt{1} : {\color{red}\text{cannot match } \alpha \text{ with } \mathrm{Int}} \end{array}

• Введём в теорию абстракцию на типах и аппликацию термов к типам!

  \begin{array}{l} \mathbf{K} : \forall \alpha\ \beta.\,\alpha \to \beta \to \alpha \\ \mathbf{K}\ @\mathrm{Int} : \forall \beta.\,\mathrm{Int} \to \beta \to \mathrm{Int} \\ \mathbf{K}\ @\mathrm{Int}\ @\mathrm{Float}\ \mathtt{1} : \mathrm{Float} \to \mathrm{Int} \end{array}

• Теперь выбор конкретного типа происходит на стороне пользователя функции

• Такие функции называются полиморфными — умеют работать с различными типами

Полиморфные функции в Haskell ✱

• Haskell неявно приписывает forall по всем типовым переменным:

  ghci> :set -fprint-explicit-foralls
  ghci> :t const
  const :: forall a b. a -> b -> a

• Типовые переменные всегда начинаются с маленькой буквы (a), в отличие от типовых констант (Int — конкретный тип)

• Типовые применения компилятор выставляет автоматически неявно

• Иногда бывает полезно типовые применения указывать вручную (TypeApplications)

  • ghci> :t const @Int
    const @Int :: forall b. Int -> b -> Int

  • В C++-like языках синтаксис примерно такой:

    fun <A, B> const(x: A, y: B): A
    const<Int, Float>(1, 2)

Что посмотреть в транспорте

• Vitaly Bragilevsky - The clear path to Haskell complexities
• Podlodka #211 – Haskell | Александр Вершилов
• Property-based testing в Haskell — так тестируются наши домашки

Полезные ссылки

• Hoogle — типизированный поиск по документации библиотек
• Отладка принтами: Debug.Trace
• GHC docs — про компилятор и расширения языка
• Typeclassopedia
• ghcup и Cabal User Guide
• The Haskell Execution Model
• I know kung fu: learning STG by example

Серьёзные материалы

• Will Kurt «Get Programming with Haskell»
• Две части курса Дениса Николаевича на степике: раз и два
• (youtube) Лекции Дениса Николаевича на МКН
• Vitaly Bragilevsky «Haskell in depth»
• (youtube) Компилятор GHC языка Haskell: теория языков программирования в работе
• (youtube) Continuation-passing style, defunctionalization, and associativity.