Вопросы по теме 'dependent-type'
Преобразование свободных переменных в терминах типа в аргументы неявной функции
Для того, чтобы мой вопрос имел смысл, я должен предоставить некоторую предысторию.
Я думаю, было бы полезно иметь язык с зависимой типизацией, который мог бы вывести существование и тип аргумента a для функции, чьи другие параметры и/или...
70 просмотров
schedule
26.02.2024
Функция индикатора уровня типа для класса типа в Haskell
По моим гнусным и по большей части непонятным причинам я решил, что нужна функция уровня типа, которая бы указывала на наличие экземпляра класса типа для типа. Это будет работать так:
> :kind! HasClass Show Int
> 'True
> :kind!...
208 просмотров
schedule
11.07.2023
Как я могу подтвердить, что тип действителен в Agda?
Я пытаюсь провести доказательства по зависимым функциям, и у меня возникла загвоздка.
Итак, допустим, у нас есть теорема f-equal
f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl
Я пытаюсь доказать более общее...
326 просмотров
schedule
17.12.2022
Зависимые типы Coq
Я новичок в Coq, и мне нужна помощь с некоторыми тривиальными примерами, чтобы начать. В частности, меня интересует определение некоторых операций над векторами (списки фиксированного размера) с использованием зависимых типов. Я начал с пакета...
1146 просмотров
schedule
23.12.2022
Пример «Типа 1», который не является ни «Типом», ни обитателем «Типа».
Каков пример жителя Type 1 , который не является ни Type , ни жителем Type ? Я не мог ничего придумать, исследуя Idris REPL.
Чтобы быть более точным, я ищу некоторые x , отличные от Type , которые дают следующее:
Idris> :t x
x : Type 1
186 просмотров
schedule
12.07.2023
Как убедить ghc в том, что добавление уровня типа коммутативно (чтобы реализовать зависимо типизированный реверс)?
Это не компилируется, потому что, как мне сообщает ghc, Add не является инъективным. Как сообщить компилятору, что Add действительно коммутативен (возможно, сообщив ему, что Add является инъективным)? Из статьи о хасохизме кажется, что нужно...
448 просмотров
schedule
11.10.2023
Объявление видов и работа с ними в Haskell
В последнее время я много играл с функцией Haskell -XDataKinds и обнаружил, что хочу создать своего рода.
Я не уверен, что мои желания сбудутся, но из constraints package , кажется, есть объявленный тип Constraint (с сортировкой BOX ),...
122 просмотров
schedule
10.03.2023
Необычные виды и конструкторы данных
Я не знаю, как я не заметил этого, но конструкторы данных и определения функций не могут использовать типы с видами, отличными от * и его вариантов * -> * и т. д., из-за сигнатуры вида (->) даже под -XPolyKinds .
Вот код, который я...
90 просмотров
schedule
30.10.2023
Как лучше всего использовать число во время компиляции и выполнения?
Я только начинаю изучать Идрис и решил, что для начала неплохо было бы реализовать конечные последовательности в виде деревьев на 2-3 пальца. Каждый внутренний узел в дереве необходимо аннотировать во время выполнения с указанием общего количества...
95 просмотров
schedule
21.09.2022
Agda: сопоставление с образцом одинаковых переменных?
В качестве учебного опыта я пытаюсь реализовать проверенный сопоставитель регулярных выражений с использованием стиля передачи продолжения в Agda на основе предложенного в этот документ .
У меня есть тип регулярных выражений, определенный...
647 просмотров
schedule
18.03.2022
Какой хороший способ представлять свободные группы?
Легко представить свободные магмы (бинарные листовые деревья), свободные полугруппы (непустые списки) и свободные моноиды (списки), и несложно доказать, что они на самом деле являются тем, за что себя выдают. Но бесплатные группы кажутся намного...
146 просмотров
schedule
14.05.2022
Устранение возможного на уровне типа
Есть ли способ развернуть значение, которое находится внутри монады Maybe , на уровне типа? Например, как определить безопасный тип tail для Vec , имеющих этот вариант pred :
pred : ℕ -> Maybe ℕ
pred 0 = nothing
pred (suc n) = just...
163 просмотров
schedule
05.07.2022
Агда: формирование всех пар {(x, y) | х в хс, у в ys}
Мне интересно, как лучше всего подойти к спискам или декартовым продуктам в Agda.
У меня есть два вектора, xs и ys . Я хочу (неформальный) набор {(x, y) | x в xs, y в ys }.
Я могу довольно легко сформировать этот набор, используя map и...
246 просмотров
schedule
14.09.2022
Haskell: определение ограничений одинаковой длины для списков в системе типов
В Haskell у меня часто бывает функция типа f , которая принимает список и возвращает список равной длины:
f :: [a] -> [a] -- length f(xs) == length xs
Точно так же у меня может быть функция типа g , которая принимает два списка...
1424 просмотров
schedule
16.08.2022
Воссоздание команды `apply` из Лиспа в Haskell с использованием GADT
В качестве упражнения я пытаюсь воссоздать Lisp apply в Haskell. Я не собираюсь использовать это в каких-либо практических целях, я просто думаю, что это хорошая возможность ближе познакомиться с системой типов Haskell и системами типов в целом....
243 просмотров
schedule
05.02.2023
Типизированный абстрактный синтаксис и дизайн DSL в Haskell
Я разрабатываю DSL на Haskell и хочу иметь операцию присваивания. Что-то вроде этого (приведенный ниже код предназначен только для объяснения моей проблемы в ограниченном контексте, у меня не было проверенного типа типа Stmt):
data Stmt = forall...
891 просмотров
schedule
26.04.2023
Разрешимость пропозиционального равенства
Два термина в agda считаются равными по определению именно тогда, когда они оба имеют одну и ту же нормальную форму --- я думаю ---, а пропозициональное равенство – это просто представление типа данных определения равенства --- опять же, я думаю ---...
85 просмотров
schedule
12.04.2023
Почему левая идентичность над сложением является тривиальным доказательством, а правая идентичность — нет?
Я только изучаю Агду, но я не понимаю, что, когда я пытаюсь доказать Тождество над Сложением, я вижу, что Левое Тождество является тривиальным доказательством.
left+identity : ∀ n -> (zero + n) ≡ n
left+identity n = refl
Но это не верно...
162 просмотров
schedule
18.04.2023
Любые приемы, чтобы избавиться от шаблона при построении доказательств абсурдного предиката на перечислениях?
скажем, у меня есть
data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}
и предикат для этого типа,
data WineStock : Fruit -> Type where
CanonicalWine : WineStock Grape
CiderIsWineToo : WineStock Apple...
358 просмотров
schedule
05.08.2022
Как доказать, что определяющие уравнения рекурсора для N верны пропозиционально, используя принцип индукции для N в Agda?
Это упражнение из книги Теория гомотопических типов . Вот что у меня есть:
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
iter : {C : Set} → C → (C → C) → ℕ → C
iter z f zero = z
iter z f (succ n) = f (iter z f n)
succℕ : {C : Set} → (ℕ...
135 просмотров
schedule
22.08.2022
