3
Я играю с функцией -XDataKinds от Haskell довольно недавно, и я обнаружил, что хочу создать вид.Объявление и работа с типами в Haskell
Я не уверен, если мои желания могут сбыться, но от Эдварда Kmett-х constraints package, там, кажется, объявленного вида Constraint (с родом BOX), который говорит, что должны быть определен в GHC.Prim, но я не мог найти Это.
Есть ли способ объявить вид в Haskell или GHC вручную? Это, вероятно, потребует ручного подтверждения того, что типы данных, объявленные с data, будут иметь надлежащий вид. Моя идея что-то вроде следующего:
data Foo :: BOX
data Bar a :: Foo where
Bar :: a -> Bar a
Использование 'DataKinds' означает, что каждое объявление данных создает новый вид, не так ли? например 'данные Nat = Z | S Nat' создает новый вид 'Nat', населенный типами: Z :: Nat' и' S :: Nat -> Nat'. –
Это правильно, но только если продвинутый тип является правильным типом данных Haskell98. В моем случае я обнаружил, что мне нужно продвигать то, что выглядит как «данные Foo (x :: Bar) (y :: Bar) = Foo | ... ', где' Bar' - это своего рода. Это не будет способствовать использованию '-XDataKinds' - мне нужно будет _manually_ продвигать его с тем же именем. Это также было бы очень полезно для желающих продвигать GADT. –
Я читал ваш вопрос несколько раз, и у меня возникли проблемы с выяснением того, что вам нужно/предлагать. Кажется, это похоже на то, что вы просите объявить новый вид, населенный некоторыми новыми типами, которые сами проживают на уровне термина, что на данный момент невозможно. Это то, о чем вы просите, или что-то еще? Если это что-то еще, маленький случай использования будет достаточно освещен. Что касается продвижения GADT, я считаю, что это открытый вопрос исследования. –