Объявление видов и работа с ними в Haskell

В последнее время я много играл с функцией Haskell -XDataKinds и обнаружил, что хочу создать своего рода.

Я не уверен, что мои желания сбудутся, но из constraints package, кажется, есть объявленный тип Constraint (с сортировкой BOX), который, как сказано, определен в GHC.Prim, но я не смог его найти.

Есть ли способ объявить вид в Haskell или GHC вручную? Это, вероятно, потребует ручного подтверждения того, что типы данных, объявленные с помощью data, будут надлежащего типа. Моя идея примерно следующая:

data Foo :: BOX

data Bar a :: Foo where
  Bar :: a -> Bar a

haskell dependent-type type-kinds data-kinds
person Athan Clark    schedule 11.01.2015    source источник
comment
Использование DataKinds означает, что каждое объявление данных создает новый вид, не так ли? например data Nat = Z | S Nat создает новый вид Nat, населенный типами Z :: Nat и S :: Nat -> Nat.   -  person Daniel Wagner    schedule 12.01.2015
comment
Это правильно, но только если продвинутый тип является правильным типом данных Haskell98. В моем случае мне нужно продвигать что-то похожее на data Foo (x :: Bar) (y :: Bar) = Foo | ..., где Bar — тип. Это не будет продвигаться с помощью -XDataKinds — мне нужно вручную продвигать его с теми же именами. Это также было бы очень полезно для продвижения GADT.   -  person Athan Clark    schedule 12.01.2015
comment
Я прочитал ваш вопрос несколько раз, и у меня возникли некоторые проблемы с выяснением того, что вам нужно/предлагаете. Кажется, вы просите объявить новый вид, населенный некоторыми новыми типами, которые сами населены на уровне терминов, что на данный момент невозможно. Это то, о чем вы спрашиваете, или что-то другое? Если это что-то другое, небольшой вариант использования был бы весьма поучительным. Что касается продвижения GADT, я считаю, что это все еще открытый вопрос исследования.   -  person Daniel Wagner    schedule 12.01.2015
comment
@DanielWagner Ты очень близко. Я не уверен, нужны ли мне типы, обитаемые на уровне терминов (например, синглтоны), но я очень хотел бы объявить вид, независимый от его типов, а затем специально объявить типы обитателями ранее определенного вида. Это не ясно, я знаю, но если бы я мог просто объявить Вид, а затем создать типы обитателей этого вида в другом выражении, это было бы идеально. Я не уверен, что мне нужны термины для этих типов, но они тоже не повредят. В идеале я хотел бы сделать data FooKind :: BOX where, затем data Bar a :: FooKind where ....   -  person Athan Clark    schedule 12.01.2015
comment
@AthanClark Я думаю, вы спрашиваете, есть ли способ объявить новые типы открытого мира в GHC в дополнение к k1 -> ... kN -> * и k1 -> ... -> kM -> Constraint. Насколько я знаю, ответ - нет. Все остальные типы в GHC возникают как продвижение (закрытых) типов данных.   -  person Lambdageek    schedule 12.01.2015

Ответы (1)


arrow_upward
1
arrow_downward

В текущем GHC (на момент написания 7.8) нельзя отделить объявление нового типа от объявления его обитателей на уровне типов.

person Daniel Wagner    schedule 12.01.2015
comment
Такие системы, как Agda, помогают смягчить эту потребность, верно? - person Athan Clark; 12.01.2015
comment
@AthanClark Я не эксперт Agda и не знаю, поддерживает ли он объявление открытых типов (на более высоких уровнях) или нет. Я бы немного удивился, если бы это произошло. - person Daniel Wagner; 12.01.2015