Описание тега data-kinds
For Haskell questions about involving the `-XDataKinds` extension in GHC. With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors.
2
ответа
Динамическое построение значений с помощью GADT с использованием типов данных
Почему сложнее построить значения с помощью типов данных, а сопоставить их с шаблонами сравнительно легко? {-# LANGUAGE KindSignatures , GADTs , DataKinds , Rank2Types #-} data Nat = Zero | Succ Nat data Direction = Center | Up | Down | UpDown deriv…
04 май '14 в 00:39
1
ответ
Какие механизмы используются для включения API на основе типов Servant?
Я очень озадачен тем, как Слуга способен достичь волшебства, которое он делает, используя набор текста. Пример на веб-сайте уже очень озадачивает меня: type MyAPI = "date" :> Get '[JSON] Date :<|> "time" :> Capture "tz" Timezone :> Ge…
31 окт '15 в 20:06
0
ответов
Как передать вид на реальную точность функциям и подпрограммам на Фортране?
Я хочу, чтобы мои подпрограммы и функции в Фортране поддерживали одинарную и двойную точность для вещественных чисел и другие виды для различных переменных, так же как и встроенные функции в Фортране. sin(x) даст нам значение синусоидальной точности…
02 июл '18 в 10:04
2
ответа
Сопоставление зависимого типа со списком типов
Я думаю, что мой вопрос довольно прост для понимания из простого кода, но, с другой стороны, я не уверен в ответе! Интуитивно понятно, что я хочу дать список типов [*] и некоторый зависимый тип Foo, сгенерировать тип [Foo *]. То есть я хочу "отобраз…
01 апр '14 в 14:26
1
ответ
Отражение неоднородных продвигаемых типов обратно в значения композиционно
Я играл с -XDataKinds в последнее время, и хотел бы взять продвинутую структуру структуры с семействами типов и вернуть ее обратно к уровню ценности. Я считаю, что это возможно, потому что композиционные компоненты очень просты, а терминальные выраж…
19 янв '15 в 17:15
2
ответа
Проблемы с EDSL, связанные с реализацией подписки на массив в Haskell
контекст Я пытаюсь реализовать EDSL, который очень напоминает OLP IBM (язык моделирования для линейного программирования). Код Haskell EDSL Code {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleIns…
23 апр '16 в 21:54
0
ответов
Использование поднятого типа данных справа от => в ghci
Рассмотрим следующий код {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} module Test () where type C x = x ~ 1 type family F x = r where F 0 = 0 F 1 = 2 F 2 = 4 Я пытаюсь убед…
07 май '17 в 12:58
0
ответов
Сжатие типов и значений вместе без экспоненциального увеличения
Предположим, у меня есть пара структур данных; один представляет тип, а другой значение: data Schema = Leaf | PairOf Schema Schema | ListOf Schema data ValueOf (schema :: Schema) where LeafElem :: String -> ValueOf 'Leaf PairElem :: ValueOf x -&g…
29 ноя '18 в 02:34
2
ответа
Понимание этого определения HList
Я относительно новичок в Haskell и пытаюсь понять одно из определений HList. data instance HList '[] = HNil newtype instance HList (x ': xs) = HCons1 (x, HList xs) pattern HCons x xs = HCons1 (x, xs) У меня есть пара конкретных вопросов: Что '[] а т…
14 дек '16 в 05:04
1
ответ
Семейные приложения типа Haskell не оцениваются
Я обнаружил интересную ситуацию при использовании типов данных с семействами типов. Сообщение об ошибке компилятора No instance for (C (ID ())) arising from a use of W, Это предполагает, что приложение семейства типов не полностью оценено, даже когд…
16 сен '14 в 16:32
2
ответа
Использование индуктивно определенных аппликативных экземпляров на типовых безопасных векторах
Я пытаюсь записать Category (конечномерных свободных) векторных пространств, но я не могу убедить GHC, что любой заданный индексированный вектор длины Applicative, вот что у меня есть: {-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, Functi…
18 апр '18 в 03:59
2
ответа
Функции с высшими видами?
Предположим, определены следующие типы данных: data X a = X {getX :: a} data Y a = Y {getY :: a} data Z a = Z {getZ :: a} Должно быть три отдельных функции, getX, getY, а также getZ? Мне кажется, что может быть функция, определенная примерно так: ge…
27 окт '16 в 20:44
1
ответ
Рекурсия по нат-видам
Этот вопрос является продолжением следующего вопроса. Сначала обратитесь к нему: перекрывающиеся экземпляры через Nat-kind Теперь пришло время сделать пример Group Symmetric, После некоторой дикой математики я подошел к примеру, который работает в п…
03 янв '19 в 04:50
2
ответа
Функции, которые работают только с одним конструктором типа
Я пишу библиотеку для очередей сообщений. Очереди могут быть Direct или же Topic, Direct очереди имеют статический связующий ключ, а Topic очереди могут иметь динамические. Я хочу написать функцию publish это работает только на Direct Очереди. Это р…
12 окт '16 в 21:00
2
ответа
Как именно работают добрые списки?
Я читал на vinyl недавно, который использует странные "списки видов" своего рода типов. Прочитав немного о видах и виниле, я получил некоторое интуитивное понимание их, и я смог взломать это вместе {-# LANGUAGE DataKinds, TypeOperators, FlexibleInst…
26 ноя '13 в 21:51
1
ответ
На моей (по общему признанию, замученной) функции Haskell появляется ложное ограничение. Как я могу удовлетворить это?
Играя с DataKinds в Haskell я создал следующий код, который реализует и использует некоторые унарные nats на уровне типов: {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUA…
12 янв '18 в 00:46
1
ответ
Попытка разработать рекурсивную функцию уровня типа для получения функции ввода и вывода
Следующие определения необходимы для понимания того, что я спрашиваю: data Param = PA | PB | PC data R p a where A :: S a -> R PA (S a) B :: S a -> R PB (S a) data S a where Prim :: a -> S a HO :: R pa a -> R pb b -> S ((R pa a) ->…
28 июл '13 в 04:29
1
ответ
Измените значения на индексы в `Conkin.Traversable` без`unsafeCoerce`
С использованием conkin пакет: https://hackage.haskell.org/package/conkin Я хочу иметь возможность принять любой Conkin.Traversable и выбросить его в Tuple оставляя позади индексы в это Tuple так что я могу восстановить это. Я использую несколько яз…
20 сен '18 в 14:16
1
ответ
Складной рекурсивный тип семейства
Я пытаюсь сложить данные с фантомным типом [*]. Вот упрощенная версия моего кода {-# LANGUAGE DataKinds, KindSignatures #-} module Stack where import Data.HList import Data.Foldable as F data T (a :: [*]) = T (Tagged a String) (!++!) :: T a -> T …
16 июн '14 в 21:44
1
ответ
Необычные виды и конструкторы данных
Я не знаю, как я этого не заметил, но конструкторы данных и определения функций не могут использовать типы с другими типами, кроме * и это варианты * -> * и т.д., из-за (->)подпись, даже под -XPolyKinds, Вот код, который я пробовал: {-# LANGUA…
13 янв '15 в 14:42