Я изучаю язык программирования Haskell и пытаюсь понять, в чем разница между a type
и a kind
.
Как я понимаю a kind is a type of type
. Например, a ford is a type of car
и a car is a kind of vehicle
.
Это хороший способ думать об этом?
Потому что, как мой мозг в настоящее время подключен, а ford is a **type** of car
, в car is a **type** of vehicle
то же время, а car is a **kind** of vehicle
. Т.е. условия type
и kind
взаимозаменяемы.
Может ли кто-нибудь пролить свет на это?
type-theory
Томас Кук
источник
источник
Ответы:
Здесь «значения», «типы» и «виды» имеют формальное значение, поэтому рассмотрение их общего использования на английском языке или аналогии с классификацией автомобилей только поможет вам.
Мой ответ относится к формальным значениям этих терминов в контексте Хаскелла; эти значения основаны (хотя на самом деле не идентичны) значениям, используемым в математической / CS "теории типов". Таким образом, это не будет очень хорошим ответом «информатики», но он должен послужить довольно хорошим ответом на Haskell.
В Haskell (и других языках) полезно назначить тип программному выражению, который описывает класс значений , которые разрешено иметь выражению. Здесь я предполагаю, что вы видели достаточно примеров, чтобы понять, почему было бы полезно знать, что в выражении
sqrt (a**2 + b**2)
переменныеa
иb
всегда будут значениями типа,Double
а не, скажем,String
иBool
соответственно. По сути, наличие типов помогает нам в написании выражений / программ, которые будут корректно работать в широком диапазоне значений .Теперь, что вы, возможно, не поняли, - это то, что типы Haskell, такие как те, которые появляются в сигнатурах типов:
на самом деле написаны на подъязыке Haskell на уровне типов. Текст программы
Functor f => (a -> b) -> f a -> f b
- в буквальном смысле - выражение типа, написанное на этом подъязыке. Подъязык входят операторы (например,->
является правым ассоциативным инфиксный оператор на этом языке), переменные (например,f
,a
, иb
), и «приложение» одного выражения типа к другому (например,f a
этоf
применяется кa
).Я упоминал, как во многих языках было полезно назначать типы программным выражениям для описания классов значений выражений? Что ж, в этом подъязыке на уровне типов выражения оцениваются по типам (а не по значениям ), и в итоге оказывается полезным назначать виды выражениям типов для описания классов типов, которые им разрешено представлять. По сути, наличие видов помогает нам в написании выражений типов, которые будут корректно работать с широким диапазоном типов .
Таким образом, значения относятся к типам, а типы - к видам , а типы помогают нам писать программы уровня значения, а виды помогают нам писать программы типа уровня .
Как выглядят эти виды ? Хорошо, рассмотрим тип подписи:
Если выражение типа
a -> a
должна быть действительными, какой вид из типов , мы должны позволить переменнымa
быть? Ну, типа выражения:выглядят корректно, поэтому типы
Int
иBool
, очевидно, правильного вида . Но даже более сложные типы, такие как:смотри правильно. Фактически, поскольку мы должны иметь возможность вызывать
id
функции, даже:выглядит хорошо. Таким образом,
Int
,Bool
,[Double]
,Maybe [(Double,Int)]
, иa -> a
все выглядят как типы правого вида .Другими словами, похоже, что есть только один вид , давайте назовем его
*
подстановочным знаком Unix, и у каждого типа будет свой вид*
, конец истории.Правильно?
Ну, не совсем. Оказывается, что
Maybe
само по себе так же верно выражение типа, как иMaybe Int
(почти так жеsqrt
, как само по себе, так же верно выражение значения, как иsqrt 25
). Однако следующее выражение типа недопустимо:Потому что, в то время как
Maybe
это выражение типа, он не представляет вид из типа , который может иметь значение. Итак, вот как мы должны определить*
- это вид из типов , которые имеют значение; он включает в себя «полные» типы, такие какDouble
или,Maybe [(Double,Int)]
но исключает неполные, бесполезные типы, такие какEither String
. Для простоты я буду называть эти полные типы вида*
«конкретными типами», хотя эта терминология не универсальна, и «конкретные типы» могут означать нечто совсем иное, скажем, для программиста C ++.Теперь в выражении типа
a -> a
, пока типa
имеет тип*
(тип конкретных типов), результат выражения типа такжеa -> a
будет иметь тип (т. Е. Тип конкретных типов).*
Итак, что вид из типа является
Maybe
? Ну,Maybe
может быть применен к конкретному типу, чтобы получить другой конкретный тип. Так,Maybe
выглядит как маленькая , как функция типа уровня , который принимает вид из рода*
и возвращает тип из вида*
. Если бы мы имели функцию на уровень значения, принявшее значение из типаInt
и возвращающее значение из типаInt
, мы бы дать ему тип подписьInt -> Int
, поэтому по аналогии мы должны датьMaybe
на любезную подпись* -> *
. GHCi соглашается:Возвращаясь к:
В сигнатуре этого типа переменная
f
имеет вид,* -> *
переменныеa
иb
вид*
; встроенный оператор->
имеет вид* -> * -> *
(он принимает тип вида*
слева и один справа и возвращает тип также типа*
). Из этого и правил вывода вида можно сделать вывод, чтоa -> b
это допустимый тип с типом*
,f a
аf b
также допустимые типы с типом*
и(a -> b) -> f a -> f b
допустимый тип типа*
.Другими словами, компилятор может «проверять вид» выражения типа,
(a -> b) -> f a -> f b
чтобы убедиться, что он действителен для переменных типа правильного типа, так же, как он «проверяет тип»,sqrt (a**2 + b**2)
чтобы убедиться, что он действителен для переменных правильного типа.Причина использования отдельных терминов для «типов» и «видов» (т. Е. Не говорить о «типах») состоит в основном во избежание путаницы. Эти виды выше вид очень отличается от типов и, по крайней мере , на первый, кажется, ведут себя совершенно по- разному. (Например, требуется некоторое время, чтобы понять, что каждый «нормальный» тип имеет одинаковый тип,
*
а типa -> b
-*
нет* -> *
.)Часть этого также историческая. По мере развития GHC Haskell различия между значениями, типами и типами начали стираться. В наши дни значения можно «преобразовать» в типы, а типы и типы - это одно и то же. Таким образом, в современном Haskell значения имеют как типы, так и типы ARE (почти), а типы - просто больше типов.
Пользователь @ user21820 попросил дать дополнительное объяснение: «типы и типы - это одно и то же». Чтобы быть более понятным, в современном GHC Haskell (я думаю, начиная с версии 8.0.1) типы и виды обрабатываются одинаково в большей части кода компилятора. Компилятор прилагает некоторые усилия в сообщениях об ошибках, чтобы различать «типы» и «виды», в зависимости от того, жалуется ли он на тип значения или тип типа соответственно.
Кроме того, если расширения не включены, они легко различимы на языке поверхности. Например, типы (значений) имеют представление в синтаксисе (например, в сигнатурах типов), но виды (типов) являются - я думаю - полностью неявными, и нет явного синтаксиса, где они появляются.
Но если вы включите соответствующие расширения, различие между типами и видами в значительной степени исчезнет. Например:
Здесь
Bar
есть (и значение, и) тип. Как тип, его тип естьBool -> * -> Foo
, который является функцией уровня типа, которая принимает тип типаBool
(который является типом, но также и типом) и типом типа*
и производит тип типаFoo
. Так:правильно проверок.
Как объясняет @AndrejBauer в своем ответе, эта неспособность различать типы и виды небезопасна - наличие типа / типа
*
, тип / тип которого сам является (что имеет место в современном Haskell), приводит к парадоксам. Тем не менее, система типов Хаскелла уже полна парадоксов из-за отсутствия завершения, так что это не считается большой проблемой.источник
type
- это простоtype
сам по себе, и в этом не было бы никакой необходимостиkind
. Так в чем же различие?Bool
это типType
это вид, потому что его элементы являются типамиBool -> Int
это типBool -> Type
это вид, потому что его элементы являются функциями, которые возвращают типыBool * Int
это типBool * Type
это вид, потому что его элементы являются парами с одним компонентом типа*
*
U_1
источник
Type :: Type
это аксиома. В этом случае различие между «типом» и «видом» полностью в человеческом языке.True
имеет тип,Bool
иBool
имеет типType
, который сам имеет типType
. Иногда мы называем тип видом, чтобы подчеркнуть, что это тип сущности уровня типа, но в Haskell это все еще просто тип. В системе, где фактически существуют вселенные, такие как Coq, тогда «тип» может относиться к одной вселенной и «добр» к другой, но тогда мы обычно хотим бесконечно много вселенных.Type :: Type
и другое, и различие между типами и видами. Кроме того, какой фрагмент кода демонстрируетType :: Type
в Haskell?*
в Haskell есть своего рода вселенная. Они просто так этого не называют.Type
отData.Kinds
и*
должно быть синонимами. Изначально у нас был только*
примитив, а в настоящее время это внутренне определяется какGHC.Types.Type
во внутреннем модулеGHC.Types
, а в свою очередь определяется какtype Type = TYPE LiftedRep
. Я думаю, чтоTYPE
это настоящий примитив, обеспечивающий семейство видов (поднятые типы, распакованные типы, ...). Большая часть «не элегантной» сложности здесь заключается в поддержке некоторых низкоуровневых оптимизаций, а не по фактическим теоретическим причинам типа.v
это значение, то оно имеет вид:v :: T
. ЕслиT
это тип, то она имеет вид:T :: K
. Тип типа называется его родом. Типы, которые выглядят так,TYPE rep
могут называться сортировками, хотя это слово встречается редко. ЕслиT :: TYPE rep
этоT
разрешено появляться на RHS a::
. У слова «добрый» есть свой нюанс: «K
в»T :: K
- это «добрый», но не «в»v :: K
, хотя и тот жеK
. Мы могли бы определить «K
это вид, если его вид является своего рода« ака », виды на RHS of::
», но это неправильно отражает использование. Поэтому моя позиция "человеческого различия".Значение , как специфический красный 2011 Ford Mustang с 19,206 миль на нем , что вы сидели в дороге.
Эта неформальная ценность может иметь много типов : это Мустанг, и это Форд, и это автомобиль, и это автомобиль, среди многих других типов, которые вы могли бы составить (тип «вещей»). принадлежащие вам ", или тип" красные вещи ", или ...).
(В Haskell, в приближении первого порядка (GADT нарушают это свойство, а магия вокруг числовых литералов и расширение OverloadedStrings немного затеняет его), значения имеют один главный тип вместо множества неформальных «типов», которые вы можете дать stang.
42
, для целей этого объяснения, anInt
; в Haskell нет типа для «чисел» или «даже целых чисел», или, скорее, вы можете создать его, но это будет непересекающийся тип изInt
.)Теперь, "Мустанг" может быть подтипом "автомобиля" - каждая ценность, которая является Мустангом, является также автомобилем. Но тип - или, если использовать терминологию Хаскелла, тип «Мустанг» - это не «автомобиль». «Мустанг» - это не то, что вы можете припарковать на подъездной дороге или покататься по нему. «Мустанг» - это существительное, категория, или просто тип. Это, неофициально, виды "Мустанга".
(Опять же, Haskell распознает только один вид для каждой вещи на уровне типа. Так что
Int
есть добрый*
, и никаких других видов.Maybe
Есть добрый* -> *
, и никаких других видов. Но интуиция все еще должна держаться:42
естьInt
, и вы можете делатьInt
с ней все . , как сложение и вычитаниеInt
сам по себе не являетсяInt
, нет такого числа , какInt + Int
Вы можете неформально слышать , как люди говорят , что.Int
этоNum
, по которым они понимают , что есть экземпляр изNum
класса типа для типаInt
-Эты не то же самое как говорят, чтоInt
имеет добрыеNum
.Int
имеет добрый «тип», который пишется на Хаскеле*
.)Так не каждый ли неформальный «тип» - это просто существительное или категория? Все ли типы имеют одинаковый вид? Зачем вообще говорить о видах, если они такие скучные?
Вот где английская аналогия станет немного странной, но потерпите меня: сделайте вид, что слово «владелец» в английском языке не имеет смысла в отдельности, без описания принадлежащей вещи. Притворись, что если бы кто-то назвал тебя «владельцем», это не имело бы никакого смысла для тебя; но если бы кто-то назвал вас «владельцем машины», вы могли бы понять, что они имели в виду.
«Владелец» не похож на «автомобиль», потому что вы можете говорить об автомобиле, но вы не можете говорить о владельце в этой вымышленной версии английского языка. Можно говорить только о «владельце машины». «Владелец» создает нечто вроде «существительное» только в том случае, если оно применяется к чему-то, что уже имеет «существительное», например, «машина». Мы бы сказали, что тип «владелец» это «существительное -> существительное». «Владелец» подобен функции, которая берет существительное и производит из него другое существительное; но это не само существительное.
Обратите внимание, что «владелец автомобиля» не является подтипом «автомобиля»! Это не функция, которая принимает или возвращает автомобили! Это просто совершенно отдельный тип от "автомобиля". В нем описываются ценности с двумя руками и двумя ногами, которые в определенный момент имели определенную сумму денег, и доставили эти деньги в дилерский центр. Он не описывает значения с четырьмя колесами и окраской. Также обратите внимание, что «владелец автомобиля» и «владелец собаки» относятся к разным типам, и то, что вы, возможно, захотите сделать с одним, может быть неприменимо к другому.
(Аналогично, когда мы говорим, что в Haskell это
Maybe
имеет вид* -> *
, мы имеем в виду, что бессмысленно (формально; неофициально мы делаем это все время) говорить о наличии «aMaybe
». Вместо этого мы можем иметь aMaybe Int
или aMaybe String
, поскольку это вещи добрый*
.)Таким образом, весь смысл разговора о видах вообще состоит в том, чтобы мы могли формализовать наши рассуждения вокруг слов типа «владелец» и обеспечить, чтобы мы когда-либо принимали значения только тех типов, которые были «полностью сконструированы» и не являются бессмысленными.
источник
Это верно - давайте посмотрим, что это значит.
Int
илиText
конкретные типы, ноMaybe a
это абстрактный тип. Он не станет конкретным типом, пока вы не решите, какое конкретное значение вы хотите дляa
конкретной переменной (или значение / выражение / что угодно), напримерMaybe Text
.Мы говорим, что
Maybe a
это конструктор типа, потому что он похож на функцию, которая принимает один конкретный тип (напримерText
) и возвращает конкретный тип (Maybe Text
в данном случае). Но конструкторы других типов могут принять еще больше «входных параметров», прежде чем они возвращают конкретный тип. Например,Map k v
необходимо принять два конкретных типа (например,Int
иText
), прежде чем он может построить конкретный тип (Map Int Text
).Таким образом, конструкторы типов
Maybe a
иList a
имеют ту же «сигнатуру», которую мы обозначаем как* -> *
(аналогично сигнатуре функции Haskell), потому что если вы дадите им один конкретный тип, они будут выплевывать конкретный тип. Мы называем это «типом» типаMaybe
иList
имеем тот же вид.Говорят, что конкретные типы имеют тип kind
*
, и наш пример Map является kind,* -> * -> *
поскольку он принимает два конкретных типа в качестве входных данных, прежде чем он сможет выводить конкретный тип.Вы можете видеть, что это в основном только количество «параметров», которые мы передаем конструктору типов, но понимаем, что мы можем также получить конструкторы типов, вложенные в конструкторы типов, так что мы можем получить вид, который выглядит,
* -> (* -> *) -> *
например, как ,Если вы являетесь разработчиком Scala / Java, вам также может пригодиться это объяснение: https://www.atlassian.com/blog/archives/scala-types-of-a-higher-kind
источник
Maybe a
синонимforall a. Maybe a
полиморфного типа*
иMaybe
мономорфный тип* -> *
.