Вопросы по теме 'gadt'
Последствия использования GADT для производительности
Когда отвечая на вопрос с предложением использовать GADT , в комментариях возникло несколько вопросов относительно производительности. Вопрос касался класса типов PlotValue :
class PlotValue a where
value :: a -> Double
и мой ответ...
620 просмотров
schedule
03.05.2023
Устранение subst для доказательства равенства
Я пытаюсь представить счетчики mod-n как разрез интервала [0, ..., n-1] на две части:
data Counter : ℕ → Set where
cut : (i j : ℕ) → Counter (suc (i + j))
Используя это, определить две важные операции несложно (некоторые доказательства...
248 просмотров
schedule
21.04.2024
Неоднозначный тип для полиморфных функциональных членов драйвера GADT
Я тестирую код для небольшого эксперимента, который я провожу, но в самом начале я натолкнулся на препятствие, которое я не знаю, как исправить.
data DatabaseDriver a b where
DatabaseDriver :: (Table table, Field field) => {
dbInsert...
136 просмотров
schedule
02.06.2022
Труба с динамическим типом запроса/ответа?
Это кажется разумным желанием, но у меня проблемы с типом. Я хотел бы иметь Client , который может отправить список параметров Server , который выберет один и вернет выбранный элемент. Что-то вроде этого:
module Toy where
import Pipes
asker...
210 просмотров
schedule
21.07.2023
Могу ли я принудить экзистенциально квантифицированный аргумент в конструкторе типа?
У меня есть тип данных, чей (единственный) конструктор содержит экзистенциально квантифицированную переменную типа:
data LogEvent = forall a . ToJSON a =>
LogEvent { logTimestamp :: Date
, logEventCategory...
161 просмотров
schedule
02.07.2023
ocaml GADT: зачем набирать файл. нужный?
В базовом примере GADT из §7.20 руководства по ocaml , что означает «тип а». ? Почему недостаточно объявить eval: a term -> a?
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App :...
586 просмотров
schedule
27.01.2024
Вывод общего экземпляра класса типов из серии более мелких?
название этого, по общему признанию, не очень описательное, но я не знаю, как еще описать это в коротком названии. Буду признателен за любые рекомендации!
Я собираюсь представить очень упрощенную версию моей проблемы :)
Итак, у меня есть класс...
78 просмотров
schedule
28.02.2022
Можно ли создать экземпляр моноида для GADT?
Учитывая следующий тип данных
{-# LANGUAGE GADTs #-}
data Response a where
ResponseMap :: HashMap Text (Sum Int) -> Response (HashMap Text (Sum Int))
ResponseSum :: Sum Int -> Response (Sum Int)
как бы я получил экземпляр моноида...
131 просмотров
schedule
04.01.2024
Функция GADT полиморфного типа результата
В следующем коде, что я могу заменить x = ... . Обратите внимание, что я не хочу накладывать ограничение класса на a (конечно, a уже относится к типу Bool , поэтому может принимать только один из двух типов).
{-# LANGUAGE GADTs #-}
{-#...
150 просмотров
schedule
05.10.2023
Как реализовать типы сумм в динамически типизированных языках без сопоставления с образцом
У меня есть только теоретическое представление о типах сумм Haskell. И все же я чувствую, что они действительно важны в Haskell и коренным образом меняют способ моделирования ваших данных. Поскольку я считаю, что они могут быть полезны и в языках с...
901 просмотров
schedule
09.10.2022
Ошибки полиморфной рекурсии OCaml
Учитывая следующие виды:
type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a...
146 просмотров
schedule
01.08.2023
Как удалить сахар из GADT?
Я читал Принуждение и роли для чайников , и автор мимоходом упомянул, что GADT — это просто синтаксический сахар.
GADT — это синтаксический сахар поверх (~) , поэтому ожидайте, что GADT будут иметь номинальные параметры типа роли.
Далее...
137 просмотров
schedule
14.11.2023
различия: GADT, семейство данных, семейство данных, которое является GADT
В чем / почему разница между этими тремя? Является ли GADT (и обычные типы данных) сокращением семейства данных? В чем конкретно разница между:
data GADT a where
MkGADT :: Int -> GADT Int
data family FGADT a
data instance FGADT a where...
864 просмотров
schedule
11.01.2023
Использование вариантов GADT в полиморфном составном типе, как в обычных алгебраических вариантах?
Скажем, у меня есть этот простой вариант типа:
type flag = {
name: string;
payload: string option;
}
type word =
| Arg of string
| Flag of flag
let args = [|
Arg "hello";
Flag {name = "foo"; payload = Some "world"};
|]
Однако если...
159 просмотров
schedule
04.04.2023
Косвенно ссылайтесь на определенные И неспецифические объекты в Haskell без монад
Я хочу хранить кучу элементов разных «видов» в структуре данных контейнера (список, набор,..) и косвенно ссылаться на них откуда-то еще. Обычно вы, вероятно, использовали бы тип суммы для элементов и, возможно, список в качестве контейнера или что-то...
59 просмотров
schedule
31.03.2024
Сопоставление шаблона в семействе данных в Haskell
Я упаковал все семейство данных в один экзистенциал:
data Type = Numeric | Boolean
data family Operator (t :: Type)
data instance Operator 'Numeric = Add | Sub
data instance Operator 'Boolean = And | Or
data AnyOp where
AnyOp :: Operator t...
183 просмотров
schedule
10.12.2023
Развертывание экзистенциально квантифицированного GADT
У меня есть пользовательский тип значения Value , помеченный своим типом ValType :
data ValType
= Text
| Bool
data Value (tag :: ValType) where
T :: Text -> Value 'Text
B :: Bool -> Value 'Bool
и я хотел бы определить функцию,...
138 просмотров
schedule
10.04.2024
