Типове, типчета и типажи

Публикувано вторник, 30 октомври 2018, 22:34

Досега си говорихме главно за функции. Истината е, че функциите са просто един тип от данни или по-точно един клас от типове данни. Използвайки функциите като основа, в предишната публикация, си дефинирахме други типове, като числа, например.

Сега нека помислим за един език от гледна точка на типовата му система. Също, какво е типова система? Какво ни дава и отнема една типова система? Защо има толкова много различни типови системи?

В началото беше смятането

Ако се върнем към Алонсо Чърч и неговото ламбда смятане, от което водят началото си функционалните езици за програмиране, ще разберем, че то има множество дефиниции. През 1940 година, Чърч измисля ламбда смятането с прости типове (simply typed lambda calculus), като така дефинира една доста проста типова система. И преди това има идеи за смислено използване на типовете на данните при дефиниране на нотации за решаване на проблеми, като “теориите за типа” на Ръсел, които са били предлагани от него между 1902 и 1908, но ние ще се съсредоточим върху типовите системи, които са близки или срещани в модерните езици за програмиране.

Нека да видим как изглежда това ламбда смятане:

e ::= x | λx:τ.e | e e | c

Този израз (term) дефинира езика ни. Можем да имаме израз (е), който е:

Или променлива (x).
Или абстракция, тоест дефиниция на функция (λx:τ.e), което може да се разбира като функция, която взима аргумент x от типа τ и има тяло израза е.
Или апликация, което е извикване на израза (който може да се сведе до функция) e с параметър израза e.
Или константа.

Към тази дефиниция, можем да си прибавим множество допълнения, като дефиниране на променливи, типове и данни:

e ::= x | λx:τ.e | e e | c | c:τ | let x:τ in e | ...

Точно това и ще направим, също така няма да ползваме този синтаксис, а различни примери написани на различни, съвременни езици.

Дефиниции и класификации

Нека започнем с няколко дефиниции, които са достатъчно известни, но е полезно да се споменат, а и често са бъркани.

Можем да разделим езиците за програмиране на статично типизирани и динамично типизирани. Езици със статична проверка на валидността на типовете в програмата, проверяват тази валидност по време на компилация. При тях често трябва при дефиниции на променливи и функции да задаваме типа на данните. Това са езици като Java, C++, Haskell, Rust, като цяло ML семейството от езици, GO и други. Динамични са езици, в които валидността на данните се проверява (или не) по време на изпълнение. Това са езици като Elixir, Ruby, JavaScript, Python, Erlang, Common Lisp и други.

Защо бихме ползвали въобще динамични езици, когато статично типизираните идват с проверка на валидността на типовете на данните по подразбиране? Има голяма полемика на тази тема, но е въпрос на вкус и производителност.

Друго деление на езиците, спрямо как оперират типовете помежду си, е на езици със силни (strong) и слаби (weak) типове. При езиците със слаби типове, операции между различни типове са възможни, като един тип се преобразува автоматично към друг, когато има нужда. Пример е JavaScript:

"5" + 4
//=> "54"

[] + 0 // Тук заради плюса, [] се преобразува към празния низ и плюса става на конкатенация
//=> "0"

{} + 4 // !!
//=> 4

Пример за слабо-типизиран, но със статична валидация на типовете език би бил C/C++:

#include <string>
#include <iostream>

using namespace std;

int main() {
  string s = "bla";
  s += 83;

  cout << s << endl;
}

//=> blaS

В Erlang това ще доведе до грешка:

5 + "4".

Което прави Erlang динамично и силно типизиран, както и Elixir, Ruby и Python. Примери за статично и силно типизирани езици са Rust, Java, Haskell.

Нека сега разгледаме следната класификация на типовете, която води началото си още от ламда смятането с прости типове. Алонсо Чърч смята типовете за съществена (intrinsic) част от семантиката (смисъла) на езика. Без типовете, зададени като част от изразите, езикът би се държал неопределено или безсмислено. Можем да кажем, че програмата без зададени типове не би могла да се компилира, защото не би имала смисъл за компилатора. Това прилича на езиците със статична валидация на типовете, нали?

От друга страна ги има и типовете на Хаскел Къри, също известни като несъществени (extrinsic) типове. При тях се приема, че типовете не са част от семантиката на езика, а имат смисъл при самото изпълнение на програмата. Тази идея прилича на динамичното типизиране.

Интересно е, че от толкова рано в развитието на типовете ги има тези две идеи. Разбира се, това е просто гледна точка към тях. Също така, в по-развитите типови системи, типовете често не се задават при повечето изрази, защото системата за проверка на валидността на типовете може да си ги изведе (inference). Може да се каже, че истината е някъде по средата.

Дали език A е по-силно или по-слабо типизиран от език B и има ли това значение? За някои хора може и да има (да речем, хората, които представят JavaScript като извращение), за други - не толкова. В тази публикация ние няма да се вълнуваме от това, просто искахме да дефинираме какво приемаме за силно/слабо статично/динамично типизиран език. От тук нататък всеки език работи с данни, тези данни имат някакви свойства, които можем да опишем с типовете им. Дали тези типове се проверяват по време на компилация или по време на изпълнение ще е важно, само и единствено, ако това ни носи важна информация в дадения момент.

От бяло платно до типова система

Какво представляват програмите?

Обикновено това е логика, която използва начални данни, преобразува ги някак или смята резултат на база тези данни, отново преобразувайки ги и връща резултат. Програмата може да живее дълго или кратко, но в крайна сметка работи с данни. Дълго живеещите програми могат да четат данни от някъде по заявка и да връщат резултати, като например сървърите. Друг пример е програми, които в реално време да приемат данни от потребител и променят нещо - игри, комуникационни системи, десктоп приложения. Кратко живеещи програми биха могли да взимат някакви начални данни, да смятат, трансформират, филтрират и да връщат резултат, след което да приключват. Да речем скриптове. Но винаги работим с данни, дали зададени вътре в самата програма или извън нея, работим с информация.

Информацията има форма и свойства. Програмата ни трябва да знае за тези форма и свойства за да знае, какво е възможно да се изпълни върху тези данни.

Пример са целите числа. Ако знаем че дадени данни са числа, ще знаем, че можем да ги събираме, изваждаме, делим, сравняваме и така нататък.

Основни типове

Да си представим, че имаме статично типизиран език като Haskell. Нека знаем синтаксиса за указване, че дадена стойност е от даден тип:

value :: T

-- Или нещо такова:

let x = value :: T in x

В Rust можем да си зададем променлива така:

let x:Т = value;

Както и в Java:

T x = value;

Но нямаме никакви типове, идващи с езика. Имаме синтаксиса за задаване на тип, но множеството от възможните типове е празно.

Числа

Можем да си представим множеството от възможни типове в нашите езици като множество от множества, като всеки елемент на това ‘множество от типове’ е множество, съдържащо всички възможни стойности за даден тип. При числата, това означава, че множеството-тип Int съдържа всички възможни цели числа. То може да е безкрайно или крайно, в зависимост как са имплементирани числата. Можем да имаме няколко типа, като да речем в Rust : u32, i32, u16, …

Да речем в Haskell можем да си дефинираме числата (на теория!) така:

data Integer = ... | -2 | -1 | 0 | 1 | 2 | 3 | ...

Няма значение как е дефиниран самия тип, важното е, че го имаме и можем да:

int x = 5;

или

5 :: Integer

Много е хубаво, че можем да кажем, че дадена стойност е число. Това значи ли, че нашият език може да работи с данни от тип цели числа?

Отговорът (засега) е не. Това е така, просто защото още не сме дефинирали възможните операции над типа цели числа.

Прости функции

Нека да дефинираме операцията за промяна на знака : -. Това е операция, която взима число и връща число с обърнат знак:

let x = 4 :: Integer in -x
-- => -4

Какво представлява тази операция? Няма значение, как е имплементирана, важното е, че можем да си я представим като функция, която взима число и някак връща същото число с обърнат знак:

let negate = |n: i32| -> i32 { -n };
let val: i32 = 84;

println!("{}", negate(val));
// => -84

Можем да си представим функцията като някаква трансформация/стрелка излизаща от множеството на числата и връщаща се пак в него. От стойност в множеството Int получаваме стойност в множеството Int.

Но в горния пример ние си дефинирахме променлива negate със стойност функцията за обръщане на знака. Какъв е типът на тази стойност? Всъщност в примера можем да си дефинираме negate и така:

let negate: fn(i32) -> i32 = |n: i32| -> i32 { -n };

// По нотацията за променлива и тип в Rust:
// let x: T = value;
// Или тук имаме let x: fn(i32) -> i32 = value;

Можем да зададем подобен тип и в по-новите версии на C++:

#include <functional>
#include <iostream>

using namespace std;

int main() {
  function<int(int)> negate = [](int n) -> int { return -n; };
  // function<int(int)> е функция която връща int и има един аргумент от тип int.

  int x = 56;
  cout << negate(56) << endl;
}

Можем да заключим, че функциите от типа Int -> Int (взимащи цяло число и връщащи цяло число) са стойности на тип. Тип, който можем да наречем функции взимащи число за параметър и връщащи число. Това означава, че всички тези стрелки от типа цели числа към типа цели числа са стойностите в това множество - тип. По този начин, вече имаме два типа в нашето множество от типове. Всъщност това множество от типове е почти категория с обекти типове и стрелки функции, но теорията на категориите не е предмет на тази публикация…

Няколко неща, върху които можем да помислим:

Действията са вид данни.
Можем да дефинираме стойности от типа функции взимащи число за параметър и връщащи число използвайки синтаксиса на езиците за дефиниране на функции или анонимни функции.
Всичко това ни дава възможност за абстракции.
В императивни езици като C++ и Java това не беше възможно преди време, но сега е възможно.

Защо в миналото нямаше функции-като-стойности в обектно-ориентирани езици като Java? На този въпрос можем да си отговорим с няколко разсъждения…

Какво са класовете в тези езици? Класовете задават структура по която се създава обект. Нещо като нов тип, за което ще си поговорим малко по-късно.
Какво са обектите в тези езици? Данни, които могат да променят състоянието си с операции вързани към тях. Тези операции имат достъп до тези данни, затворени в обекта. Можем да си предаваме обекта насам-натам, предавайки неговите операции и данни.
Какво са анонимните функции (ламбдите)? Функции, които може да са обвързани с данни, дали от средата в която са дефинирани, или от начина, по който са построени, които можем да си предаваме насам-натам.

Можем да ползваме така-наречените клоужър-функции по много подобен начин на този, по който използваме обектите в обектно-ориентираните езици. Много, да ги наречем “промишлени” програмисти се опитват да избягат от математиката, но тя ги намира. Всичките абстракции, които те строят за да се предпазят от математическите абстракции, всъщност могат да се сведат до точно тези математически абстракции. Често това бягане от математиката усложнява доста езика и средата - да речем глобално, променливо (mutable) състояние облечено в обвивката на обект…

Но нека да се върнем на функциите върху числа. Можем да имаме безкрайно много функции от типа Int -> Int, но какво да кажем за функции на два аргумента като събирането:

let plus a b = a + b;;

plus 4 5;;
- : int = 9

Тук ползваме OCaml, но подобен пример би бил и в Haskell. Ако разгледаме типа на тази функция, той всъщност излиза като plus : int -> int -> int, или Int -> Int -> Int. Тоест функция, която взима цяло число и връща функция, която взима цяло число и връща функция.

В език като Java:

import  java.util.function.*;

public class Funcs2 {
  public static void main(String[] args) {
    BiFunction<Integer, Integer, Integer> plus = (a, b) -> a + b;
    Function<Integer, Function<Integer, Integer>> pluss = (a) -> (b) -> a + b;

    System.out.println(plus.apply(1, 2));
    // => 3
    System.out.println(pluss.apply(1).apply(2));
    // => 3
  }
}

Поведението на plus и pluss са еквивалентни. Повече за това може да прочетете тук, но идеята е че функции от типа Int, Int -> Int можем да кажем, че имат тип: Int -> Int -> Int. В езици като Haskell има ‘синтактична захар‘ за маскиране на това и винаги имаме функции на просто един аргумент скрити отдолу.

От гледна точка на нашето множество от типове можем да си представим такива функции като стрелка, която тръгва от множеството цели числа и отива към множеството функции взимащи число за параметър и връщащи число. Но множеството от такива стрелки е отново тип и може да се представи като множество в нашата типова система функции взимащи число за параметър и връщащи функция взимаща число за параметър и връщаща число.

Подобни разсъждения можем да имаме и за функции на множество параметри числа, връщащи числа. Типовата система е множество от множества със стелки (действия/функции) между тях, определяща поведението на данните.

И тази идея може да моделира типовата система както на статично-типизирани, така и на динамично-типизирани езици. В този модел никъде не указваме, дали проверяваме валидността на зададените типове и стойностите по време на компилация или по време на изпълнение.

Още основни типове

Ако типовете са множества, кой често използван тип би бил множество със дамо два елемента? Това е булевият тип Bool. Има само две стойности true и false. Край него можем да добавим още типове, като Bool -> Bool, член на който е функцията not или пък типа Bool -> Bool -> Bool, член на който са дизюнкцията и конюнкцията (or и and). Можем да имаме и тип от функции Int -> Bool, да речем even и odd, както и Int -> Int -> Bool, като >, < и други.

Както виждате можем да имаме безкрайно много типове от функции, само като имаме няколко прости типа.

Кой е типът само с един елемент? Това би бил типа известен като unit или в някои езици void. Той има една единствена стойност, често представяна като (). Този тип е интересен, защото ни позволява да си дефинираме функции, които връщат стойност, без да взимат стойност:

let f () = 5;;
val f : unit -> int = <fun>

Това е функция от типа Unit -> Int. При използване на клоужър функции, върнати от други функции, такова нещо има смисъл. Също може да се ползва като резултат от функции със странични ефекти при езици позволяващи това. Да речем принтиращи функции, макар че дори от тях е добре да очакваме смислен резултат дали действието е било успешно.

Интересно наблюдение за функциите Unit -> X е, че всеки тип може да се представи като функция по този начин, да речем числата ще са Unit -> Int, всичко може да е функция!

Разбира се може да има много типове с по две стойности или само с по една стойност. Ние разглеждаме типове, с които езиците често идват “опаковани”.

А има ли празен тип? Има празно множество, защо да няма тип без стойности?

В Rust можем да си дефинираме функция със следния тип:

let junk: fn(i32) -> ! = |_: i32| -> ! { panic!() };

Типът е fn(i32) -> !, което просто означава, че това е функция, която приема стойност, число, но никога не връща резултат, програмата не завършва с резултат а с паника.

В Haskell можем да си дефинираме:

data Empty

Тип без стойности. Ако го ползваме някъде, програмата би се ‘счупила’. Това са примери за типа без стойности, известен като Bottom или ⊥. Все пак функциите при програмирането не са математически функции. Те се пресмятат спрямо данни отвън със всякаква форма, докато се изпълняват, така че могат и никога да не върнат резултат. Всеки тип съдържа и ⊥ типа, защото всяка функция, да речем Int -> Int е възможно да не се пресметне никога.

Лесно можем да си представим атоми, низове, символи, числа с плаваща запетайка и други подобни прости типове като множества в нашата типова система, но е време да разгледаме някои други често срещани типове, които се градят на основните.

Алгебра и типове

При функционалните езици, данните са непроменими, което прави възможно дефинирането на алгебрични типове данни, или типове от данни съставени от други типове от данни.

Произведение

Има множество типове-произведение. Да речем в Elixir, имаме tuple типовете:

{1, 4}

Това е тип, който е съставен от два различни типа, може да има толкова стойности колкото стойностите на тип1 умножени по стойностите на тип2. Можем да го представим и като декартово произведение на множества в нашата типова система. Обикновено типовете-произведение имат две функции:

fst :: (a, b) -> a
fst (x, y) = x

snd :: (a, b) -> b
snd (x, y) = y

Ако си ги представим като стрелки, fst, ще сочи от типа-произведение към типа на първия елемент на двойката, а snd към втория.

Можем да си дефинираме класове Pair<A, B> за да постигнем подобен тип в Java или C++. Разбира се можем да имаме и произведения от по три, четири, N типа.

Обикновено типа с един елемент, Unit се реализира като празено произведение, или празен tuple. Той е и нещо като единичен елемент в произведението, защото ((), Int) има същият брой елементи като Int, който се смята така : 1 * N(Int) = N(Int).

Сума или копродукт

Типът сума също се среща често:

data Either a b = Left a | Right b
type BoolInt = Either Bool Integer

Left True :: BoolInt
Right 5   :: BoolInt

Тук имаме тип BoolInt чиито стойности от ляво могат да са всички възможни Bool стойности (2), а от дясно всички възможни числа (N(Int)). В даден момент стойност от този тип може да е или Left val или Right val. Което значи, че общо възможните стойности в BoolInt са 2 + N(Int). От там тип-сума.

Във функционалните езици имаме pattern matching. Така можем да си дефинираме функция, която приема стойност от сумарен тип и спрямо от кой от съставните му типове е съответната стойност, се изпълнява определена имплементация.

falsy :: BoolInt -> Bool
falsy (Left False) = True
falsy (Left True)  = False
falsy (Right 0)    = True
falsy (Right _)    = False

Разбира се case/match-оператор би могъл да се ползва по подобен начин. Всъщност ако се замислим, всеки тип може да се представи като сума от възможните си стойности.

data Bool = True | False

Друга известна сума е Maybe:

data Maybe a = Just a | Nothing

Като тук Nothing е единствената стойност на тип - нищо.

В Rust можем да видим подобни типове:

enum Either {
    Left(bool),
    Right(i32)
}
// Можем да ползваме и Result

let val = Either::Left(true);


match val {
    Left(false) => true,
    Left(true)  => false,
    Right(0)    => true,
    Right(_)    => false
}

Да, enum в Rust не е същото като енумерациите в C++ и Java. Всъщност дефинира tagged union или това, което наричаме сумарен тип.

В езици като C++ и Java не получаваме такива типове, но можем да си ги построим, като си поиграем с интерфейси, класове, виртуални методи и тн. Шаблонът известен като Visitor също помага. Всъщност с подобни похвати може да се емулира и в GO.

В езици от типа на JavaScript, Python и Ruby можем лесно да напишем функции, приемащи стойност и с правилните if-else разклонения да имитираме pattern matching.

Макар и динамично-типизирани, Erlang и Elixir имат нотация за типове и инструмент за статична проверка на валидността им, наречен dialyzer. Поддържат и pattern matching, затова следното е възможно:

@spec falsy(val :: boolean | integer) :: boolean
def falsy(false), do: true
def falsy(true), do: false
def falsy(0), do: true
def falsy(n) when is_integer(n), do: false

# Или

@spec falsy(val :: boolean | integer) :: boolean
def falsy(b) when is_boolean(b), do: not(b)
def falsy(n) when is_integer(n), do: n == 0

Експоненти

Ако си спомняте, функциите представяхме като стрелки от тип към тип. Но даден тип стрелки, тип функции, също образуваше тип. Често наричаме тези функции-типове експонентни типове.

Колко стойности има типа Bool -> Int? Можем да имаме два случая за функция, относно аргумента от тип Bool - False и True. От там за всеки от тези два случая имаме толкова стойности колкото имаме стойности в Int типа. Или общо N(Int) x N(Int), което е N(Int)².

Функция-типовете A -> B имат точно N(B)^N(A) възможни стойности.

Рекурсивни типове

Ако можем да си дефинираме нещо в ламбда смятането с прости типове, то задължително ще се изпълни с резултат. Но този език е ограничен, с него не можем да изразим всяка програма, която можем да изразим с turing complete език като тези, които ползваме в реалния живот.

Досега си добавяхме типове, които могат да се опишат като допълнения към ламбда смятането с прости типове. Сега ще си добавим още едно допълнение : рекурсивни типове.

Такива типове можем да дефинираме с помощта на самите тях, точно като при дефиницията на рекурсивни функции. И с помощта на такива типове можем да си дефинираме безкрайни или повтарящи се структури, като списък:

type intlist = Nil | Cons of int * intlist;;

Или пък други рекурсивни типове като дърво:

data Tree a = Leaf a | Node (Tree a) (Tree a)

И в Rust, Java, C++ можем да си дефинираме типове/класове, които имат полета от тип себе си.

Записи, речници и произволни типове

Записи

Някои езици ни предоставят записи (records), това са tuple типове, като всеки елемент на произведението е с етикет - име.

-record(person, {name = "", id}).

По този начин можем да си правим собствени типове. Ако добавим и етикет-име на самия тип, като в горния пример, можем да си именоваме типа.

Речници

Друга структура, която можем да ползваме за произволни типове е речника. Повечето езици идват с такива типове, които в зависимост от езика могат да бъдат имплементирани с променима или непроменима структура - хешмап, трай, други.

В доста езици имаме и структури, които са именовани речници представляващи такъв тип:

defmodule Person do
  defstruct [:age, name: ""]
end

dali = %Person{name: "Dali", age: 4}
#=> %Person{age: 4, name: "Dali"}

inspect(dali, structs: false)
#=> "%{__struct__: Person, age: 4, name: \"Dali\"}"

В горния пример на Elixir, структурата-‘тип’, Person, е просто речник с таен ключ името ѝ.

Произволни типове

В много езици ги има тези структури, с които си дефинираме произволни типове. В обектно-ориентираните обикновено има класове, но можем да си ги представим като такива структури, криещи състоянието си. Някои от ключовете им - полета са скрити, други сочат към функции, имащи достъп до скритото състояние. Обектите са просто стойности от този тип.

По този начин можем да сведем доста идеи за типове, дефинирани от потребителя на езика до речници или нещо подобно. А речникът е просто тип, който е дефиниран с помощта на синтаксиса на езика, както дефинирахме произведение, списък, сумарен тип… някакво допълнение към този синтаксис.

И така, нашето множество от типове е безкрайно и потребители на езика могат да добавят нови типове, използвайки синтаксиса на езика. Нека за малко разгледаме идеята за полиморфизъм.

Полиморфизъм

С прост pattern matching и структури, можем да си дефинираме прост полиморфизъм в някои езици:

base_airan_s_krastavitsi = [
  krastavitsi: 1, kiselo_mliako: "300ml", voda: "300ml",
]

defmodule AiranSKrastavitsi do
  defstruct [
  {:drink, {__MODULE__, :drink}} | base_airan_s_krastavitsi
  ]

  def drink(%AiranSKrastavitsi{}), do: "Айранче!!!"
end

defmodule Tarator do
  defstruct [
    {:drink, {__MODULE__, :drink}} |
    [{:chesun, 2} | base_airan_s_krastavitsi]
  ]

  def drink(%Tarator{}), do: "Друго си е то!"
end

defmodule HumanNeeds do
  def drink(%{drink: {m, f}} = what) when is_atom(f) do
    apply(m, f, [what])
  end
end

HumanNeeds.drink(%AiranSKrastavitsi{})
HumanNeeds.drink(%Tarator{})

Тук използваме pattern matching за да ползваме нещо, което има функция drink. Всеки map, който има такава функция, отговаря на този интерфейс. Това можем да наречем inclusion полиморфизъм.

Също забележете, че речник с ключ foo е над-тип на всички речници с този ключ и някакви други ключове, защото можем да дефинираме функция коят pattern match-ва за този ключ. По тази логика празният речник е над-тип на всички речник-типове.

Това прилича малко на наследяването в език като Java.

Интерфейсите в GO задават нещо подобно на pattern matching шаблона в Elixir примера. При Elixir има и по-хубав начин за подобен полиморфизъм, наречен протоколи.

Ако пък множество типове имплементират дадена функция и спрямо типа, с който се извиква функцията имаме различно поведение, ние overload-ваме тази функция. В примерът с Elixir с помощта на apply правим нещо такова. Този тип полиморфизъм, където спрямо типа имаме различна имплементация на действие е известен като Ad-hoc полиморфизъм. Подобно нещо в езици като Haskell и Rust може да се постигне чрез използване на тип-класове или типажи (traits).

Тип-класове

Използвайки тип класове, можем да пишем функции, които очакват стойности на типове изпълняващи/имплементиращи тези тип-класове.

class SomeDrink drinkType where
  drinkIt :: drinkType -> String

instance SomeDrink Tarator where
  drinkIt _ = "Good stuff!"

instance SomeDrink Antifreeze where
  drinkIt _ = "And now I'm blind..."

По този начин функцията drinkIt може да взима стойности на типове, удовлетворяващи тип-класа.

Аналогични са трейтовете в *Rust(:

trait SomeDrink {
  fn drink_it(&self) -> &'static str;
}

struct Tarator {
}

impl SomeDrink for Tarator {
  fn drink_it(&self) -> &'static str {
    "Good stuff!"
  }
}

let tarator = Tarator{};
println!("{}", tarator.drink_it());

В ламбда смятането с прости типове няма идеята за полиморфизъм, Полиморфичното ламбда смятане, още известно като ламбда смятане от втори ред или System F, всъщност е надграждане на ламбда смятането с прости типове, така че да поддържа параметричен полиморфизъм. Надграждането всъщност е идеята да имаме различни стойности в зависимост какви типове ползваме при един и същи тип функции.

Типове като параметри

В Ad-hoc полиморфизма можем да си дефинираме функции, които приемат някакъв обобщаваш тип, представящ няколко други типа, които имат нещо общо.

При езици като Haskell, имаме и параметричен полиморфизъм, когато при дефиниране на функция, типът е параметър, означаващ - всеки възможен тип:

length :: [a] -> Int
length [] = 0
length (x:xs) = 1 + length xs

В горния пример, [a] е тип-параметър в дефиницията на length. Това означава, че можем да подадем списък от каквито и да е елементи.

Можем да постигнем подобно нещо с Rust и версиите на Java след 1.4 с така, наречените generics (C++ шаблони):

fn takes_val_of_any_type<T>(x: T) {
    // do stuff with x
}

И тук стигаме до нещо интересно. В някои езици имаме нещо като функции, които работят върху типове. Функции, които взимат даден тип и връщат нов тип, базиран на подадения. Такива функции видяхме из примерите неведнъж. Те са известни като тип-конструцктори.

Тип-конструктори

Както казахме тип-конструкторите са нещо като функции, които взимат тип и връщат тип. Функции върху типове. Разбира се можем да приемем и самите тях за типове, мака и типове, които не могат да имат стойности. Но ако тип-конструкторите са типове, то те могат да връщат тип-конструктори. По този начин чрез curring можем да имаме тип-конструктори, които взимат множество типове и връщат нов тип.

Добре. Нека да видим пример:

data Maybe a = Nothing | Just a

Тук Maybe е тип-конструктор, не можем да имаме стойност която е просто Maybe. Можем обаче да имаме стойност от тип Maybe Int:

Just 42 :: Maybe Int
-- => Just 42

Ако се върнем на Either:

data Either a b = Left a | Right b

И това е тип-конструктор, но с два аргумента.

Нека да разгледаме Rust:

pub enum Option<T> {
    None,
    Some(T),
}

Типът Option е тип-конструктор.

let x: Option<u32> = Some(2);

Тук x е от тип Option<u32>. Друг пример за тип-конструктор е списъкът, да речем.

И така с помощта на generics и templates в C++ и Java имаме класове, които са нещо като тип-конструктори.

type 'a llist = Nil | Cons of ('a * 'a llist)

В ML езиците също ги имаме (Rust можем да го приемем за такъв, но синтаксиса е по-скоро generic-подобен).

В GO нямаме тип-конструктори, и следва че нямаме параметричен полиморфизъм. Могат да се правят неща с interface{} за да постигнем идеята - приема всякакви типове, като Object в по-ранните версии на Java…

И така когато имаме тип-конструктори, имаме начин да създаваме нови типове и имаме параметричен полиморфизъм. Повечето модерни статично-типизирани езици поддържат някаква форма на това.

Ако се върнем на идеята с параметричния полиморфизъм и как System F е надграждане над ламбда смятането с прости типове, при което една и съща функция може да връща различни стойности спрямо стойности от различни типове. Ако сега надградим тази система с тип-конструктори - тоест да имаме тип-функции които спрямо различни типове, връщат различни типове, получаваме System F ω.

При система System F, стойности могат да зависят от типове.
При система System F ω, добавяме и типове, зависещи от типове. Всяко такова надграждане води до по-богата типова система. Можем да изразяваме много повече неща.

Но очевидно типове като Int и даже наши си, като Tarator са по-различни от типове като Maybe a. Първите можем да ги представим лесно като множества от стойности, вторите, пораждат много такива множества от стойности. Дали не можем да говорим за типове на типовете?

Видове

Типът на даден тип се нарича вид. Всички типове, които могат да имат стойности са от вида *. Тип-конструктори с един аргумент са от вида * -> *. Подобно на функции! Тип-конструктори с 2 аргумента са от вида * -> * -> *. И така можем да продължим до безкрайност.

Забележете, че * -> (* -> *), което всъщност е като * -> * -> * е различно от (* -> *) -> *.

Изразът (* -> *) -> * означава тип-конструктор, който взима тип-конструктор и връща тип. Това е много подобно нещо на функциите от по-висок ред - функции, които могат да взимат функции като параметър.

Такива тип-конструктори, можем да наричаме тип-конструктори от по-висок ред. Както можем да си правим абстракции над често срещани конструкции и поведения с функциите от по-висок ред, можем да си правим и по-сложни и мощни абстракции чрез типове от по-висок ред.

Доста езици не поддържат такива типове. OCaml и Haskell ги поддържат, Rust да речем не. Както и Java, C#, Elm..

Именно затова с Haskell можем да си дефинираме неща като:

class Monad m where
  (>>=)  :: m a -> (a -> m b) -> m b
  (>>)   :: m a -> m b        -> m b
  return ::   a               -> m a
  fail   :: String -> m a

А какво е това? Това е тема за друга публикация, в друго време, в друг свят, или просто моноид в категорията на ендофункторите.

Заключителни мисли

Започнахме от много прост синтаксис за задаване на типове и стигнахме до видове и типове от по-висок ред. Всяка идея, с която се запознахме ни даваше по-силна типова система, с която можехме да изразяваме по-сложни действия и зависимости. С други думи правеше езика по-изразителен. Статично-типизираните езици имат нужда от по-изразителни типови системи за да мога да постигат по мощни и интересни абстракции. Да разбираме идеи от типовата система на Haskell може само да ни помогне да разбираме типовите системи на други езици, защото това е мощна типова система, силно свързана с теорията на типовете, а програмирането идва от математиката, ставайки по-изразително и мощно, то развива математиката.

Разгледахме стойности, които зависят от други стойности (функции), стойности, които зависят от типове (полиморфични функции), типове, които зависят от типове (тип-конструктори). Може би има и типове, които зависят от стойности, кой знае… (Ако се развълнувате, да - dependent types, Idris, Agda).

Разгледахме (скрито) някои от върховете на ламбда куба, даже споменахме терминът, който е обясняван хиляди пъти и никога добре - монад.

И все пак, това е нищо. Знаейки тези неща, можейки да ползваме някои от тях ни помага да пишем по-добър код и да го преизползваме. Има и толкова много неща, които не знаем.

Интересни книжки по темата

Types and Programming Languages - покрива всички неща, за които си говорихме тук и много повече.
Advanced Topics in Types and Programming Languages - допълнение към горната книга, има много различни теми, dependent types е една от тях.
Learn You a Haskell - много добро начало за научаване на основни неща в Haskell.
Category Theory for Programmers - ето това вече е доста на високо ниво, но ако имате интерес към теория на категориите, това е добро начало. Пространството от типове-множества, което строяхме е нещо като категория.