Вопросы по теме 'data-kinds'
Как сделать, чтобы значения зависели от других значений без DataKinds?
У меня есть тип юниверса и рабочий тип. Рабочие могут изменить вселенную. Чего я хотел бы добиться, так это гарантировать, что вселенная может быть изменена только работниками из этой вселенной (а не работниками в будущем или в прошлом).
Лучшее,...
97 просмотров
schedule
18.04.2022
Как использовать виды данных + фантомные типы для кодирования единиц в Haskell?
Приведенный ниже код не работает , поскольку он компилируется . Не должно (интуитивно).
1) Почему этот код компилируется?
2) Как я могу «исправить» эту программу, чтобы «плохие» программы, такие как isKm $ getMeter 1 , отклонялись во время...
390 просмотров
schedule
18.06.2022
Последовательность над разнородным списком в Haskell
Рассмотрим следующее определение HList :
infixr 5 :>
data HList (types :: [*]) where
HNil :: HList '[]
(:>) :: a -> HList l -> HList (a:l)
И семейство типов Map для сопоставления списков уровней типов:
type family Map...
212 просмотров
schedule
28.06.2022
Перегрузка метода show для типов Maybe
Это продолжение моего предыдущего вопроса . Теперь я пытаюсь изменить метод toText , чтобы он также обрабатывал Maybe a с перегруженной функцией toText . Ниже приведен код, который компилируется и работает нормально — теперь я хотел бы...
90 просмотров
schedule
28.07.2022
Построить значение из вида в Haskell
Я хотел бы перейти от типа к значению следующим образом, но без использования устаревших DatatypeContexts:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DatatypeContexts #-}
import Data.Proxy
import...
54 просмотров
schedule
29.07.2022
Понимание этого определения HList
Я относительно новичок в Haskell и пытаюсь понять одно из определений HList .
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs = HCons1 (x, xs)
У меня есть пара конкретных вопросов:...
482 просмотров
schedule
13.09.2022
Попытка разработать рекурсивную функцию уровня типа для получения ввода и вывода функции
Следующие определения необходимы, чтобы понять, о чем я спрашиваю:
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...
101 просмотров
schedule
04.07.2023
Вывод типа с отражением и типами данных
У меня проблемы с тем, чтобы GHC вывел тип в том месте, где он должен быть очевиден. Ниже приведен полный фрагмент, демонстрирующий проблему.
{-# LANGUAGE DataKinds, ScopedTypeVariables, KindSignatures, TypeOperators, GADTs #-}
import...
238 просмотров
schedule
23.12.2022
Какие механизмы используются для включения API Servant на основе типов?
Я очень озадачен тем, как Servant может достичь волшебства, которое он делает, используя набор текста. Пример на веб-сайте меня уже сильно озадачивает:
type MyAPI = "date" :> Get '[JSON] Date
:<|> "time" :> Capture "tz"...
1432 просмотров
schedule
10.04.2023
Расшифровка продвижения типа DataKind в библиотеке Servant
Я пытаюсь изучить руководство для servant , веб-DSL на уровне типов. Библиотека широко использует DataKind . языковое расширение.
В начале этого руководства мы находим следующую строку, определяющую конечную точку веб-службы:
type...
335 просмотров
schedule
26.10.2022
Черч-кодирование логического значения и STLC
Часто говорят, что
tru t f = t
fls t f = f
представляют True и False в том смысле, что «мы можем использовать эти термины для выполнения операции по проверке истинности логического значения».
Но за этим скрывается важное предостережение,...
242 просмотров
schedule
10.01.2023
Доброе понижение в должности (в отличие от доброго продвижения по службе)
Расширение DataKinds продвигает "значения " (т.е. конструкторы) в типы. Например, True и False становятся разными типами вида Bool .
Я хотел бы сделать обратное, то есть понизить типы до значений. Функция с такой сигнатурой подойдет:...
295 просмотров
schedule
28.11.2022
Могу ли я запретить один конкретный конструктор данных внутри другого, в то время как оба дают один и тот же тип?
Я хотел бы создать тип T в Haskell, который позволяет
[Leaf 1, Rooted (Leaf 2), Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]
но нет
[Leaf 1, Rooted (Leaf 2), Branch (Rooted (Leaf 3)) (Branch (Leaf 4) (Leaf 5))]
т.е. все...
78 просмотров
schedule
06.03.2023
Нормализация неравенств TypeNats
У меня есть две функции, обе с видом Nat (от TypeNats), которые имеют оператор типа сравнения <= . Ограничение 2 <= n для функции b содержит ограничение 1 <= n для функции a . Есть ли способ заставить ghc решить, что 2 <= n...
111 просмотров
schedule
11.01.2023
Невозможно создать список на уровне типов с одним элементом
Я чешу голову со следующим поведением. Есть ли очевидная причина, почему это так?
Prelude> :set -XDataKinds
Prelude> :k 'True
'True :: Bool
Prelude> :k ['True, 'False]
['True, 'False] :: [Bool]
Prelude> :k ['True]...
42 просмотров
schedule
20.03.2023
Отражение разнородных продвигаемых типов обратно к ценностям, композиционно
Я недавно играл с -XDataKinds и хотел бы взять продвинутую структуру с семействами типов и вернуть ее на уровень значений. Я считаю, что это возможно, потому что композиционные компоненты очень просты, а терминальные выражения столь же...
544 просмотров
schedule
06.01.2024
