Хорошо, пойдем один за другим.
Ценности
Значения - это конкретные данные, которые программы оценивают и обрабатывают. Ничего особенного, некоторые примеры могут быть
1
true
"fizz buzz foo bar"
Типы
Хорошим описанием для типа является «классификатор для значения». Тип - это немного информации о том, что это значение будет во время выполнения, но оно будет указано во время компиляции.
Например , если вы скажете мне , что e : bool
во время компиляции, и я буду знать , что e
это либо true
или false
во время выполнения, ничего! Поскольку типы классифицируют значения следующим образом, мы можем использовать эту информацию для определения некоторых основных свойств вашей программы.
Например, если я когда-нибудь увижу, что вы добавляете e
и e'
когда e : int
и когда e' : String
, то я знаю, что что-то не так! На самом деле я могу пометить это и выдать ошибку во время компиляции, говоря: «Эй, это не имеет никакого смысла!».
Более мощная система типов допускает более интересные типы, которые классифицируют более интересные значения. Например, давайте рассмотрим некоторую функцию
f = fun x -> x
Это довольно ясно f : Something -> Something
, но что это должно Something
быть? В скучной системе типов мы должны были бы указать что-то произвольное, например Something = int
. В более гибкой системе типов мы могли бы сказать,
f : forall a. a -> a
То есть "для любого a
, f
карты и a
к a
". Это позволяет нам использовать f
более широко и писать более интересные программы.
Более того, компилятор будет проверять, действительно ли он соответствует заданному нами классификатору, если f = fun x -> true
тогда у нас будет ошибка, и компилятор скажет об этом!
Так как TLDR; тип - это ограничение времени компиляции для значений, которые могут быть выражены во время выполнения.
Тип Конструктор
Некоторые типы связаны между собой. Например, список целых чисел очень похож на список строк. Это почти как sort
для целых чисел, почти как sort
для строк. Мы можем представить себе своего рода фабрику, которая создает эти почти одинаковые типы, обобщая их различия и создавая их по требованию. Вот что такое конструктор типов. Это как функция от типов к типам, но немного более ограниченная.
Классическим примером является общий список. Конструктор типа для это просто общее определение
data List a = Cons a (List a) | Nil
Теперь List
это функция, которая отображает тип a
в список значений этого типа! В Java-земле я думаю, что их, возможно, называют «универсальными классами».
Параметры типа
Параметр типа - это просто тип, переданный конструктору типа (или функции). Точно так же, как в уровне значений, который мы бы сказали, foo(a)
есть параметр, a
так же как List a
и у параметра типа a
.
Виды
Виды немного сложнее. Основная идея заключается в том, что определенные типы похожи. Например, у нас есть все примитивные типы в Java int
, char
, float
... , которые все ведут себя так , как будто они имеют один и тот же «тип». Кроме того, когда мы говорим о классификаторах для самих типов, мы называем классификаторы видами. Итак int : Prim
, String : Box
, List : Boxed -> Boxed
.
Эта система дает хорошие конкретные правила о том, какие типы мы можем использовать, где, например, как типы управляют значениями. Было бы явно глупо сказать,
List<List>
или
List<int>
В Java, поскольку List
необходимо применять к конкретному типу, который будет использоваться таким образом! Если мы посмотрим на их виды List : Boxed -> Boxed
и с тех пор Boxed -> Boxed /= Boxed
, вышесказанное является доброй ошибкой!
Большую часть времени мы на самом деле не думаем о видах, а просто относимся к ним как к «здравому смыслу», но в случае систем с причудливыми типами это важно учитывать.
Небольшая иллюстрация того, что я говорил до сих пор
value : type : kind : ...
true : bool : Prim : ...
new F() : Foo : Boxed : ...
Лучше читать, чем википедию
Если вы заинтересованы в подобных вещах, я очень рекомендую вложить хороший учебник. Теория типов и PLT в целом довольно обширны, и без единой базы знаний вы (или, по крайней мере, я) можете бродить, не доходя никуда в течение нескольких месяцев.
Две из моих любимых книг
- Типы и язык программирования - Бен Пирс
- Практические основы языков программирования - Боб Харпер
Обе прекрасные книги, которые рассказывают о том, о чем я только что говорил, и гораздо более красивые, хорошо объясненные детали.
int
в Java состоит из набора 2 ^ 64 различных значений. Аналогия с наборами ломается, когда включаются подтипы, но это достаточно хорошая начальная интуиция, особенно если учесть алгебраические типы данных (например, объединение двух типов может содержать любого из членов любого типа; это объединение этих наборов) ,Они должным образом определены жесткой академической математической поддержкой, обеспечивающей четкие утверждения о том, кем они являются, как они работают и что гарантировано.
Но программисты в основном не должны знать это. Им нужно понять концепции.
Ценности
Давайте начнем со значений, поскольку все строится оттуда. Значения - это данные, используемые в вычислениях. В зависимости от подхода, это те ценности, с которыми все знакомы: 42, 3.14, «Как теперь коричневая корова», кадровый учет для Дженни в бухгалтерии и т. Д.
Другие интерпретации значений являются символами . Большинство программистов понимают эти символы как «значения» перечисления.
Left
иRight
являются символами для перечисленияHandedness
(игнорируя двуличных людей и рыбу).Независимо от реализации, значения - это разные вещи, с которыми работает язык для выполнения вычислений.
Типы
Проблема со значениями заключается в том, что не все расчеты являются законными для всех значений.
42 + goat
на самом деле не имеет смысла.Это где типы вступают в игру. Типы - это метаданные, которые определяют подмножества значений.
Handedness
Перечисление выше , является хорошим примером. Этот тип говорит «толькоLeft
иRight
может быть использован здесь». Это позволяет программам очень рано определять, что определенные операции приведут к ошибке.Другое практическое применение: компьютеры работают с байтами. Байт 42 может означать число 42, или это может означать символ *, или это может означать Дженни из учета. Типы также (при практическом использовании, а не теоретически) помогают определить кодировку для базового набора байтов, используемых компьютерами.
Виды
И вот тут мы начинаем немного выходить. Итак, когда в языке программирования есть переменная, которая ссылается на тип, какой тип он имеет?
Например, в Java и C # он имеет тип
Type
(который имеет типType
, который имеет ... и так далее до конца). Это концепция видов . В некоторых языках вы можете сделать немного больше полезных вещей с помощью переменной Type, чем Java и C #. Как только это произойдет, будет полезно сказать : «Я хочу , что значение имеет тип, но также некоторые рода изIEnumerable<int>
». Та-да! Виды.Большинство программистов могут думать о таких типах, как общие ограничения Java и C #. Посмотрим
public class Foo<T> where T: IComparable{}
. В языке с видамиT: kindOf(IComparable)
объявление переменной становится легальным; не просто особая вещь, которую вы можете сделать в объявлениях классов и функций.Тип Конструкторы
Возможно неудивительно, что конструкторы типов просто конструкторы для типов . «Но как вы строите тип? Типы просто есть ». Эх ... не так много.
Также неудивительно, что это довольно сложно построить все различные полезные подмножества значений, которые когда-либо будет использовать любая компьютерная программа. Конструкторы типов работают, чтобы помочь программистам «создавать» эти подмножества осмысленными способами.
Самый распространенный пример конструктора типов - это определение массива:
int[4]
. Здесь вы указываете4
конструктор типов, который использует значение для построения массиваint
s с 4 записями. Если бы вы указали другой тип ввода, вы бы получили другой тип вывода.Обобщения являются еще одной формой конструктора типов, в качестве входных данных используется другой тип.
Во многих языках есть конструктор типа, например,
P -> R
для создания типа, который представляет функцию, которая принимает типP
и возвращает типR
.Теперь контекст определит, является ли «функция, которая возвращает тип» конструктором типа или нет. По моему (по общему признанию ограниченному) опыту, строка «Вы можете использовать этот тип во время компиляции?». Да? Тип конструктора. Нет? Просто функция.
Тип Параметр
Итак, вы помните параметры, переданные в конструкторы типов? Они обычно известны как параметры типа, так как общей формой конструктора типа является
Type[param]
илиType<param>
.источник
*
, в то время как конструктор типа (с одним аргументом) имеет тип* -> *
. Такие ограничения, как(Num a) => a
(что означает «любой тип,a
который является экземпляром классаNum
типов»), сами по себе не являются видами. Класс типовNum
не сам по себе «вид», но имеет вид* -> Constraint
. Мне трудно связать идею Хаскеля «вида» (которая, как я полагаю, тесно связана с видами в теории типов?) С примерами, которые вы приводите.:kind
дает видNum
как* -> Constraint
. Это может быть специфично для GHC, я не знаю.