Вопросы по теме 'gadt'
Сравнение типов во время выполнения для переноса полиморфных структур данных в GADT.
Предположим, мы определяем GADT для сравнения типов:
data EQT a b where
Witness :: EQT a a
Можно ли тогда объявить функцию eqt со следующей сигнатурой типа:
eqt :: (Typeable a, Typeable b) => a -> b -> Maybe (EQT a b)...
430 просмотров
schedule
06.05.2022
Scala Type-Inference для конструктора типов
У меня есть вопрос относительно вывода типов в конструкторах типов Scala. Я использую Scala 2.9.1...
Предположим, я определил дерево:
sealed trait Tree[C[_], A]
case class Leaf[C[_], A](a: A) extends Tree[C, A]
case class Node[C[_], A](a:...
447 просмотров
schedule
20.05.2023
Как использовать функциональные зависимости и экзистенциальную количественную оценку, чтобы удалить ненужный параметр для моего типа
В библиотеке HLearn, над которой я работаю, у меня есть тип данных контейнера, который выглядит так:
data (Model params model) => Container' params model = Container'
{ baseparams :: params
, basemodel :: model
}
Проблема в...
352 просмотров
schedule
02.12.2022
Когда GADT были введены в GHC?
Когда GADT были введены в GHC? (версия + дата)
Кроме того, они по-прежнему считаются расширением языка или теперь они являются частью стандарта Haskell?
217 просмотров
schedule
21.03.2023
Деконструкция GADT: где я теряю контекст?
У меня есть этот тип и эти функции:
data Tag a where
Tag :: (Show a, Eq a, Ord a, Storable a, Binary a) => a -> BL.ByteString -> Tag a
getVal :: Tag a -> a
getVal (Tag v _) = v
isBigger :: Tag a -> Tag a -> Bool
a...
221 просмотров
schedule
09.04.2024
действительно ли этот GADT имеет репрезентативную роль типа
Этот тип данных может иметь type role HCons' representational representational , что позволяет использовать coerce для добавления или удаления новых типов, применяемых к элементам, без необходимости обхода списка.
data HNil' = HNil'
data HCons'...
309 просмотров
schedule
15.06.2022
Список любого типа DataKind в GADT
Отказ от ответственности
GADT и DataKinds для меня неизведанная территория, поэтому некоторые их ограничения и возможности мне неизвестны.
Вопрос
Итак, я пишу AST для эмиттера кода JavaScript, и я определил один крайний случай между...
291 просмотров
schedule
12.05.2022
Создание выражения GADT в OCaml
Вот мое игрушечное выражение GADT:
type _ expr =
| Num : int -> int expr
| Add : int expr * int expr -> int expr
| Sub : int expr * int expr -> int expr
| Mul : int expr * int expr -> int expr
| Div : int expr * int expr...
583 просмотров
schedule
11.11.2022
Вектор, содержащий GADT
Я просто изучаю все, что могу, об ExistentialQuantification, GADT, KindSignatures и т. д. И для этого я пытаюсь придумать несколько небольших программ, которые помогают мне лучше понять все.
Теперь у меня есть этот небольшой фрагмент (который на...
112 просмотров
schedule
28.06.2023
Обеспечение правильности данных
Я занимаюсь программированием на Haskell уже несколько месяцев, и мне это очень нравится. Я чувствую, что хорошо разбираюсь в монадах, функторах, чистоте и т. Д. Теперь, когда я использую эту прекрасную систему типов, идея о возможности выразить...
93 просмотров
schedule
26.05.2022
Построение конкретных типов для классов типов с помощью GADT
Вдохновением для этого является создание списка значений, которые являются экземплярами Show . Я нашел следующий фрагмент, который использует GADT для создания конкретного Showable типа.
data Showable where Showable :: Show a => a ->...
97 просмотров
schedule
11.06.2023
Автоматическое получение ограничений класса типов с помощью GADT
Я пишу библиотеку для работы с бесконечными последовательностями, используя ленивую оценку. Для краткости я использую обобщенные алгебраические типы данных (GADT), чтобы установить ограничение Ord для индекса каждого термина в последовательности....
91 просмотров
schedule
07.03.2023
Функции GADT
Это дополнительный вопрос о функциях для полиморфных типов данных .
Тип данных Question моделирует вопрос/ответ с помощью Message (текст вопроса) и функции ( String -> a ), которая сопоставляет ввод пользователя с результатом вопроса:...
186 просмотров
schedule
30.04.2022
Как я могу программно создать этот тип данных из другого?
Я бы хотел использовать DSum для чего-то. Чтобы работать с DSum , вам нужно иметь тип «тег», который принимает один аргумент типа, например.
data Tag a where
AFirst :: Tag Int
ASecond :: Tag String
Однако я хотел бы использовать это...
102 просмотров
schedule
13.01.2023
Избегайте избыточных ограничений при работе с фантомными типами
Это упрощенный, возможно, глупый пример того, что я пытаюсь закодировать (что более сложно и требует кодирования длины списка во время компиляции).
Учитывая следующее:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE...
159 просмотров
schedule
24.06.2022
Типы ограничений в конструкторе GADT
У меня простой ADT
data Concept a = Entity a | Role a | Relation a | Resource a | Sub (Concept a)
Теперь я хочу создать GADT, используя этот ADT, который будет ограничивать сигнатуру типа его конструкторов. Этот код не будет работать, но я...
242 просмотров
schedule
17.04.2022
Может ли кто-нибудь объяснить синтаксис типа, используемый в этой программе OCaml?
Приведенные ниже типы взяты из этот вопрос
(* contains an error, later fixed by the OP *)
type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b...
350 просмотров
schedule
25.07.2023
Должен ли я разыгрывать Nat-kind каждый раз?
Я попытался смоделировать квантовый компьютер. Вот тип данных, представляющий кубиты:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-#...
74 просмотров
schedule
19.02.2023
Не знаете, что такое GADT и распространяемые ограничения.
Существует множество вопросов и ответов о том, что GADTs лучше, чем DatatypeContexts , потому что GADT автоматически делают ограничения доступными в нужных местах. Например, здесь , здесь , здесь . Но иногда кажется, что мне все еще нужно...
206 просмотров
schedule
28.11.2022
