Вопросы по теме 'dependent-type'
Типы, зависящие от пути scala, и доказательства уровня типа
В настоящее время я пытаюсь определить модель языка синхронизированного потока данных в scala.
Поток виртуально представляет собой бесконечную последовательность значений некоторого типа T, изменяемую некоторыми часами C (часы показывают, в какие...
571 просмотров
schedule
04.02.2023
Универсальное программирование Arity в Agda
Как написать общие функции арности в Agda? Можно ли написать полностью зависимые и полиморфные вселенную общие функции с арностью?
655 просмотров
schedule
17.10.2022
Как сравнить Векторы натов в Агде
Я пытаюсь использовать Decidable Equality для сравнения двух векторов Nats в Agda. Я попытался открыть модуль Vector Equality, передав в качестве аргумента Nat DecSetoid следующим образом:
open import Data.Nat
open import Data.Vec
open import...
234 просмотров
schedule
18.08.2023
Вывод общего экземпляра класса типов из серии более мелких?
название этого, по общему признанию, не очень описательное, но я не знаю, как еще описать это в коротком названии. Буду признателен за любые рекомендации!
Я собираюсь представить очень упрощенную версию моей проблемы :)
Итак, у меня есть класс...
78 просмотров
schedule
28.02.2022
Саморепрезентация и вселенные в ОТТ
Вопрос касается теории наблюдательных типов .
Рассмотрим этот параметр:
data level : Set where
# : ℕ -> level
ω : level
_⊔_ : level -> level -> level
# α ⊔ # β = # (α ⊔ℕ β)
_ ⊔ _ = ω
_⊔ᵢ_ : level -> level -> level
α ⊔ᵢ...
187 просмотров
schedule
20.06.2022
Простой преобразователь температуры с зависимым типом в Haskell, можно ли сделать этот код короче?
Функция convert ниже имеет сигнатуру типа:
SUnit fromUnit-> SUnit toUnit ->Value fromUnit -> Value toUnit ,
который имеет избыточность , поскольку одна и та же информация может быть выражена с помощью:
Value fromUnit ->...
204 просмотров
schedule
08.06.2024
Мира мало
Я все еще пытаюсь внедрить теорию типов наблюдений в себя и все это в Агду.
В настоящее время у меня есть следующая иерархия вселенных:
Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁
Чтобы определить равенство...
208 просмотров
schedule
10.06.2023
Как написать определения coq с подтипами
У меня есть следующее определение для closed_subspace_equiv
Record Closed_Subspace (V:Normed_Space) := {
closed_subspace :> V -> Prop;
addition_closure : forall (x y:V),(closed_subspace x) -> (closed_subspace y) -> (closed_subspace...
161 просмотров
schedule
13.08.2022
типы потоков с постоянными строками и зависимые типы
Скажем, у меня есть следующая постоянная строка:
export default const FOO = 'FOO'
Скажем, я импортирую это в аннотированный файл потока следующим образом:
import FOO from '../consts/Foo'
Затем у меня есть функция:
const example =...
4482 просмотров
schedule
03.09.2023
Зависимый тип с обратной ссылкой (Scala)
Я играю с зависимыми (от пути) типами в Scala и наткнулся на следующий сценарий, для которого я не могу найти хорошего решения. Предположим, я хочу иметь некоторую иерархию зависимых типов, и я хочу, чтобы каждый из них имел обратную ссылку на свой...
109 просмотров
schedule
02.07.2023
Как создать ограниченный экземпляр на основе значений времени выполнения?
Я экспериментировал с реализацией matrix О'Коннора, основанной на *-полукольцах, что позволяет очень аккуратно решения для графовых алгоритмов:
import Data.Array
newtype Matrix i e = Matrix (Array (i,i) e)
matrix :: (Ix i, Bounded i) =>...
346 просмотров
schedule
30.01.2023
Как сопоставить с образцом на опоре при испытании в Coq без исключения на Type
Я пытаюсь доказать, что хвост отсортированного списка сортируется в Coq, используя сопоставление с образцом вместо тактики:
Require Import Coq.Sorting.Sorted.
Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A}...
514 просмотров
schedule
04.05.2022
Как использовать зависимый парный тип Sigma из библиотеки singletons?
Как зависимая пара может ввести Sigma из синглетонов использовать библиотеку?
Предположим, что существует следующий индексированный список типов и функция репликации:
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons...
320 просмотров
schedule
24.08.2022
Ltac: делайте что-то другое в каждой цели
У меня есть сценарий проверки, в котором я исследую несколько случаев, и в настоящее время он довольно медленный, поскольку у меня есть несколько стратегий для решения целей, и я пробую каждую из них в каждом случае.
Я знаю, что мне нужно применять...
217 просмотров
schedule
12.10.2023
Идрис: восстановить равенство после сопоставления с образцом
Я разбиваю список на голову и хвост, но позже мне нужно доказательство того, что они возвращают мне исходный список при объединении:
test: Bool -> String
test b = let lst = the (List Nat) ?getListFromOtherFunction in
case lst of...
60 просмотров
schedule
15.09.2023
Использование класса в качестве параметра шаблона в собственной деклерации
(Я знаю, что это не обычная реализация, но я хотел попробовать эту идею.)
struct TrieNode {
std::unordered_map<char, TrieNode> next;
};
Этот класс очень хорошо скомпилирован и работает, как и ожидалось, в Visual Studio 2017. Однако...
102 просмотров
schedule
11.07.2023
Можно ли доказать эквивалент Forall_inv для разнородных списков в Coq?
Следуя определению гетерогенных списков Адама Члипалы, я хотел определить эквивалент функции Forall в обычных списках. Это не так уж сложно, и вы, как обычно, получаете два конструктора. Теперь предположим, что я знаю, что факт верен в...
70 просмотров
schedule
07.09.2022
Идрис передает функции доказательство того, что аргументы являются LTE
У меня есть функция, которая вычитает два Nat . Как мне доказать, что первый аргумент, который я ему передаю, на самом деле меньше второго?
dummy : (k : Nat) -> (n : Nat) -> {auto smaller : LTE k n} -> Nat
dummy k n = n - k
Я...
63 просмотров
schedule
14.10.2023
Как в scala указать компилятору реализовать эквивалентность двух абстрактных типов?
У меня есть простой случай для проверки возможности вывода типа scala:
trait Super1[S] {
final type Out = this.type
final val out: Out = this
}
trait Super2[S] extends Super1[S] {
final type SS = S
}
case...
105 просмотров
schedule
14.06.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
