Что такое "*" в Haskell?

Ответ 1

Во-первых, * не является подстановочным знаком! Он также обычно произносится как "звезда".

Кровоточащее примечание к краю: к февралю 2015 г. предлагается упростить систему подкастов GHC (в 7.12 или новее). Эта страница содержит хорошее обсуждение истории GHC 7.8/7.10. С нетерпением, GHC может отказаться от различия между типами и видами, с * :: *. См. Weirich, Hsu и Eisenberg, System FC с явным добровольным равенством.

Стандарт: описание выражений типа.

Отчет Haskell 98 определяет * в этом контексте как:

Символ * представляет тип всех конструкторов нулевого типа.

В этом контексте "nullary" просто означает, что конструктор не принимает никаких параметров. Either является двоичным; он может применяться к двум параметрам: Either a b. Maybe является унарным; он может быть применен к одному параметру: Maybe a. Int является нулевым; он может применяться без каких-либо параметров.

Это определение немного неполное само по себе. Выражение, содержащее полностью примененный унарный, двоичный и т.д. Конструктор, также имеет вид *, например. Maybe Int :: *.

В GHC: что-то, что содержит значения?

Если мы сориентируем документацию GHC, мы получим что-то более близкое к определению "может содержать определение времени выполнения". Страница комментариев GHC "Виды" гласит, что "*" - это тип значений в штучной упаковке. Такие вещи, как Int и Maybe Float имеют вид *. "С другой стороны, PolyKinds.)

Вставные значения и поднятые типы немного отличаются. Согласно странице комментариев GHC "TypeType" ,

Тип unboxed, если его представление не является указателем. Разблокированные типы также не сбрасываются.

Тип поднимается, если у него есть дно в качестве элемента. Закрытия всегда имеют поднятые типы: то есть любой идентификатор с привязкой в ​​ядре должен иметь поднятый тип. Оперативно поднимаемый объект - это тот, который можно ввести. Только поднятые типы могут быть объединены с переменной типа.

So ByteArray#, тип необработанных блоков памяти, помещен в коробку, потому что он представлен как указатель, но не изменен, потому что bottom не является элементом.

> undefined :: ByteArray#
Error: Kind incompatibility when matching types:
   a0 :: *
   ByteArray# :: #

Поэтому представляется, что старое определение User Guide более точно, чем комментарий GHC: * - это тип отмененных типов. (И, наоборот, # - это вид неэкранированные типы.)

Обратите внимание, что если типы типа * всегда поднимаются, для любого типа t :: * вы можете построить "значение" сорта с undefined :: t или каким-либо другим механизмом для создания дна. Поэтому даже "логически необитаемые" типы, такие как Void, могут иметь значение, т.е. Нижнее.

Итак, да, * представляет типы типов, которые могут содержать значения времени выполнения, если undefined - это ваша идея значения времени выполнения. (Что не совсем сумасшедшая идея, я не думаю.)

Расширения GHC?

Есть несколько расширений, которые немного оживляют систему. Некоторые из них являются обыденными: KindSignatures позволяет писать аннотации типа, например аннотации типов.

ConstraintKinds добавляет вид Constraint, грубо говоря, вид левой части =>.

DataKinds позволяет вводить новые типы помимо * и #, так же, как мы можем вводить новые типы с data, newtype и type.

С DataKinds каждое объявление data (могут применяться положения и условия) генерирует объявление продвинутого вида. Так

 data Bool = True | False

вводит обычный конструктор значений и имя типа; кроме того, он производит новый вид Bool и два типа: True :: Bool и False :: Bool.

PolyKinds вводит переменные вида. Это просто способ сказать "для любого типа k", как мы говорим "для любого типа t" на уровне типа. Что касается нашего друга * и будет ли он по-прежнему означать "типы со значениями", я бы предположил, что тип t :: k, где k - это переменная вида, может содержать значения, если k ~ * или k ~ #.

Ответ 2

В самой базовой форме родного языка, где есть только вид * и конструктор вида ->, тогда * - это вид вещей, которые могут стоять в типе отношения к значениям; ничто другое не может быть типом значений.

Существуют типы для классификации значений. Все значения с одним и тем же типом являются взаимозаменяемыми с целью проверки типов, поэтому для проверки типов требуется только тип, а не конкретные значения. Таким образом, мы имеем "уровень ценности", в котором живут все фактические значения, и "тип уровня", где живут их типы. Отношение типа "тип" образует связи между двумя уровнями, причем один тип является типом (обычно) многих значений. Хаскелл делает эти два уровня совершенно явными; это почему вы можете иметь такие объявления, как data Foo = Foo Int Chat Bool, где вы объявили объект типа Foo (тип с видом *) и объект уровня ценности Foo (конструктор с типом Int -> Char -> Bool -> Foo), В двух Foo участвуют просто ссылки на разные сущности на разных уровнях, и Haskell полностью разделяет их так, что он всегда может сказать, на каком уровне вы обращаетесь, и, таким образом, может (иногда смутно) на разных уровнях иметь одинаковые имя.

Но как только мы вводим типы, которые сами имеют структуру (например, Maybe Int, который является конструктором типа Maybe, примененным к типу Int), тогда мы имеем вещи, которые существуют на уровне типа, которые не фактически стоят в типе отношения к любым значениям. Нет значений, тип которых просто Maybe, только значения с типом Maybe Int (и Maybe Bool, Maybe (), даже Maybe Void и т.д.). Поэтому нам нужно классифицировать наши вещи на уровне уровня по той же причине, что и нам, чтобы классифицировать наши ценности; только определенные типы-выражения фактически представляют что-то, что может быть типом значений, но многие из них работают взаимозаменяемо с целью "проверки вида" (является ли он правильным типом для объекта уровня ценности, который он объявляет типом является проблемой для другого уровня). ¹

So * (который часто заявляется как произносится "тип" ) является основным видом; это тип всех типов уровня, которые могут быть указаны как тип значений. Int имеет значения; поэтому его тип *. Maybe не имеет значений, но принимает аргумент и создает тип, имеющий значения; это дает нам вид вроде ___ -> *. Мы можем заполнить пробел, заметив, что аргумент Maybe используется как тип значения, отображаемого в Just a, поэтому его аргумент также должен быть типом значений (с видом *), и поэтому Maybe должен иметь вид * -> *. И так далее.

Когда вы имеете дело с типами, которые включают только звезды и стрелки, то только типы-выражения вида * являются типами значений. Любой другой вид (например, * -> (* -> * -> *) -> (* -> *)) содержит только другие "сущности типа", которые не являются фактическими типами, которые содержат значения.

PolyKinds, как я понимаю, совсем не меняет эту картину. Он просто позволяет делать полиморфные декларации на уровне уровня, что означает, что он добавляет переменные к нашему добрым языкам (в дополнение к звездам и стрелкам). Поэтому теперь я могу рассмотреть вещи типа типа k -> *; это может быть создано для работы как вида * -> *, так и (* -> *) -> * или (* -> (* -> *)) -> *. Мы приобрели точно такую ​​же силу, как (a -> b) -> [a] -> [b] на уровне, который нам удалось получить; мы можем написать одну функцию map с типом, который содержит переменные, вместо того, чтобы писать каждую возможную функцию отображения отдельно. Но есть еще один вид, который содержит типы уровня, которые являются типами значений: *.

DataKinds также вводит новые вещи на добрый язык. Фактически то, что он делает, это позволить нам объявлять произвольные новые виды, которые содержат новые объекты уровня типа (так же, как обычные объявления data позволяют нам объявлять произвольные новые типы, которые содержат новые объекты уровня ценности). Но это не позволяет нам объявлять вещи с соответствием сущностей во всех трех уровнях; если у меня есть data Nat :: Z | S Nat и используйте DataKinds, чтобы поднять его до уровня уровня, тогда у нас есть две разные вещи с именем Nat, которые существуют на уровне типа (в качестве типа значения уровня Z, S Z, S (S Z) и т.д.) и на уровне уровня (в качестве типа уровня Z, S Z, S (S Z)). Тип Z уровня не является типом любых значений; значение Z находится на уровне уровня Nat (который, в свою очередь, имеет вид *), а не тип Z. Таким образом, DataKinds добавляет новые пользовательские вещи к родному языку, который может быть видом новых пользовательских вещей на уровне типа, но остается, что единственными типами уровня, которые могут быть типы значений, являются вида *.

Единственное дополнение к родному языку, о котором я знаю, который действительно меняет это, относится к видам, упомянутым в ответе @ChristianConkle, например # (я считаю, что еще есть пара? действительно ужасно осведомлены о типах "низкого уровня", таких как ByteArray#). Это типы типов, которые имеют значения, которые GHC должны знать, чтобы относиться по-разному (например, не предполагая, что они могут быть помещены в коробки и лениво оценены), даже если задействованы полиморфные функции, поэтому мы не можем просто приложить знания, которые им нужны для того, чтобы иначе относиться к типам этих значений, иначе они будут потеряны при вызове на них полиморфных функций.

¹ Таким образом, слово "тип" может быть немного запутанным. Иногда он используется для обозначения вещей, которые фактически стоят в типе отношения к вещам на уровне значений (это интерпретация, используемая, когда люди говорят: "Maybe не является типом, это тип-конструктор" ). И иногда он ссылался на все, что существует на уровне типа (под этой интерпретацией Maybe на самом деле есть тип). В этой статье я стараюсь очень четко ссылаться на "вещи на уровне шрифта", а не на "тип" как на короткую руку.

Ответ 3

Для новичков, которые пытаются узнать о типах (вы можете думать о них как о типе типа), я рекомендую эту главу книги Learn you a Haskell.

Я лично думаю о видах таким образом:

У вас есть конкретные типы, например Int, Bool, String, [Int], Maybe Int или Either Int String.

Все они имеют вид *. Зачем? Поскольку они не могут принимать больше типов в качестве параметра; Int, является Int; a Maybe Int - это, Maybe Int. А Maybe или [] или Either?

Когда вы говорите " Maybe, у вас нет конкретного типа, потому что вы не указали его параметр. Maybe Int или Maybe String отличаются друг от друга, но у обоих есть * вид, но, Maybe, ждет вид типа * чтобы вернуть вид *. Чтобы уточнить, давайте посмотрим, что GHCI :kind команда может нам рассказать:

Prelude> :kind Maybe Int
Maybe Int :: *
Prelude> :kind Maybe
Maybe :: * -> *

Со списками это одно и то же:

Prelude> :k [String]
[String] :: *
Prelude> :k []
[] :: * -> *

Как насчет Either?

Prelude> :k Either Int String
Either Int String :: *
Prelude> :k Either Int
Either Int :: * -> *

Вы могли бы думать об интуитивном мышлении о Either как о функции, которая принимает параметры, но параметры являются типами:

Prelude> :k Either Int
Either Int :: * -> *

означает, что Either Int ожидает параметр типа.