Типы как гражданин первого класса

Исходя из опыта C ++, я не понимаю, зачем нужны типы / выражения типов как первоклассный гражданин? Единственный язык, который я знаю, который поддерживает эту функцию, это Aldor.

Есть ли у кого-нибудь литература о типах как первоклассном гражданине или есть причины, почему это полезно?

Типы первого класса включают то, что называется зависимой типизацией . Это позволяет программисту использовать значения типов на уровне типов. Например, тип всех пар целых чисел является обычным типом, в то время как пара всех целых чисел с левым числом, меньшим, чем правое число, является зависимым типом. Стандартный вводный пример этого - списки с закодированной длиной (обычно называемые Vectorв Haskell / Idris). Следующий псевдокод представляет собой смесь Идриса и Хаскелла.

-- a natural number
data Nat = Zero | Successor Nat

data Vector length typ where
  Empty : Vector Zero typ
  (::)   : typ -> Vector length typ -> Vector (Successor length) typ

Этот фрагмент кода говорит нам о двух вещах:

• Пустой список имеет нулевую длину.
• consвставка элемента в список создает список длины n + 1

Это выглядит очень похоже на другую концепцию с 0 и n + 1не так ли? Я вернусь к этому.

Что мы получаем от этого? Теперь мы можем определить дополнительные свойства используемых нами функций. Например: Важным свойством appendявляется то, что длина результирующего списка является суммой длин двух списков аргументов:

plus : Nat -> Nat -> Nat
plus          Zero n = n
plus (Successor m) n = Successor (plus m n)

append : Vector n a -> Vector m a -> Vector (plus n m) a
append Empty  ys = ys
append (x::xs) ys = x :: append xs ys

Но в целом эта техника не кажется полезной в повседневном программировании. Как это относится к сокетам, POST/ GETзапросам и так далее?

Ну, это не так (по крайней мере, не без значительных усилий). Но это может помочь нам другими способами:

Зависимые типы позволяют нам формулировать инварианты в коде - правила о том, как должна вести себя функция. Используя их, мы получаем дополнительную безопасность в отношении поведения кода, аналогично предварительным и постусловиям Eiffel. Это чрезвычайно полезно для автоматического доказательства теорем, который является одним из возможных применений Idris.

Возвращаясь к приведенному выше примеру, определение списков с закодированной длиной напоминает математическую концепцию индукции . В Идрисе вы можете сформулировать концепцию индукции в таком списке следующим образом:

              -- If you can supply the following:
list_induction : (Property : Vector len typ -> Type) -> -- a property to show
                  (Property Empty) -> -- the base case
                  ((w : a) -> (v : Vector n a) ->
                      Property v -> Property (w :: v)) -> -- the inductive step
                  (u : Vector m b) -> -- an arbitrary vector
                  Property u -- the property holds for all vectors

Этот метод ограничен конструктивными доказательствами, но, тем не менее, очень мощный. Вы можете попытаться написать appendиндуктивно в качестве упражнения.

Конечно, зависимые типы - это только одно использование типов первого класса, но это, пожалуй, один из самых распространенных. Дополнительное использование включает, например, возврат определенного типа из функции на основе ее аргументов.

type_func : Vector n a -> Type
type_func Empty = Nat
type_func v     = Vector (Successor Zero) Nat

f : (v : Vector n a) -> type_func v
f Empty = 0
f vs    = length vs :: Empty

Это бессмысленный пример, но он демонстрирует то, что вы не можете подражать без первоклассных типов.