Вопросы по теме 'dependent-type'
Сопоставление с образцом без специализации типов
Я играю в Coq, пытаясь создать отсортированный список. Мне просто нужна функция, которая берет список [1,2,3,2,4] и возвращает что-то вроде Sorted [1,2,3,4] , т.е. удаляет плохие части, но не сортирует весь список.
Я подумал, что начну с...
1387 просмотров
schedule
13.03.2023
Неустойчивое разрешение типа отверстия
Недавно я обнаружил, что типовые дыры в сочетании с сопоставлением с образцом в доказательствах обеспечивают довольно приятный опыт, подобный Agda, в Haskell. Например:
{-# LANGUAGE
DataKinds, PolyKinds, TypeFamilies,...
2239 просмотров
schedule
27.09.2023
Могут ли зависимые типы абстрагироваться от функций с n аргументами?
В динамически типизированных языках я могу создать функцию, которая принимает функцию в качестве аргумента и возвращает функцию.
Например, функция memoize в Clojure.
(def memoized-fn
(memoize any-function))
В этом примере memoize не...
123 просмотров
schedule
11.09.2022
Разница между параметрами типа и индексами?
Я новичок в зависимых типах, и меня смущает разница между ними. Кажется, люди обычно говорят, что тип параметризуется другим типом и индексируется некоторым значением . Но разве нет различия между типами и терминами в языке с зависимой...
3134 просмотров
schedule
26.09.2022
Квантификатор Forall и комплексные логические предложения в Idris
Я новичок в зависимых типах и, имея опыт работы с Haskell, медленно изучаю Idris. В качестве упражнения я хочу написать кодировку Хаффмана. В настоящее время я пытаюсь написать доказательство того, что «сглаживание» дерева кода дает префиксный код,...
409 просмотров
schedule
15.07.2022
Как работать с потоком в agda?
Я написал потоковый тип данных и одну головную операцию в Agda. Теперь я хочу проверить правильность работы головки.
Итак, я принимаю свой входной поток как 1 :: 2 :: 3 ::. . . Но agda не принимает это как поток.
Итак, мой вопрос в том, как...
295 просмотров
schedule
05.02.2023
Как я могу организовать сопоставление с образцом в зависимом представлении?
Я написал несколько простых типов для просмотра значений Vect :
data SnocVect : Vect n a -> Type where
SnocNil : SnocVect []
Snoc : (xs : Vect n a) -> (x : a) -> SnocVect (xs ++ [x])
data Split : (m : Nat) -> Vect n a -> Type...
203 просмотров
schedule
22.12.2022
Как пронумеровать элементы списка по `Fin`s за линейное время?
Мы можем перечислить элементы списка следующим образом:
-- enumerate-ℕ = zip [0..]
enumerate-ℕ : ∀ {α} {A : Set α} -> List A -> List (ℕ × A)
enumerate-ℕ = go 0 where
go : ∀ {α} {A : Set α} -> ℕ -> List A -> List (ℕ × A)
go n []...
517 просмотров
schedule
24.07.2022
Зависимо типизированная карта — не ошибетесь?
Предположим, я определяю свой собственный тип списка.
data MyVec : Nat -> Type -> Type where
MyNil : MyVec Z a
(::) : a -> MyVec k a -> MyVec (S k) a
И функция myMap , выполняющая роль fmap для MyVec :
myMap :...
90 просмотров
schedule
06.08.2023
Зачем нужны контейнеры?
(В качестве оправдания: заголовок имитирует заголовок Зачем нам нужны монады? )
Существуют контейнеры (и проиндексированные ) (и хазохистские ) и описания . Но контейнеры проблемны , и, судя по моему небольшому опыту, мне труднее думать с...
1301 просмотров
schedule
12.05.2023
Можно ли ввести в Haskell функцию с переменным числом аргументов?
Обратите внимание на следующий термин Haskell:
callNTimes :: forall a . Int -> (a -> a) -> a -> a
callNTimes n f 0 = x
callNTimes n f x = f (callNTimes (n-1) f x)
firstOf :: ??????
firstOf n = callNTimes n (\ x y -> x)
Если мы...
273 просмотров
schedule
07.06.2023
Замена одноэлементных типов данных семейством данных
Итак, в моем текущем проекте я выполняю кучу логики на уровне типов с одноэлементными типами.
Например:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs...
116 просмотров
schedule
19.11.2023
Вычисление нетривиального типа Идриса для тензорной индексации
Я возился с простой тензорной библиотекой, в которой я определил следующий тип.
data Tensor : Vect n Nat -> Type -> Type where
Scalar : a -> Tensor [] a
Dimension : Vect n (Tensor d a) -> Tensor (n :: d) a
Векторный параметр...
231 просмотров
schedule
25.06.2023
Равенство по зависимым типам записей
Некоторое время я ломал голову над этой проблемой: у меня есть типы записей с зависимыми полями, и я хочу доказать равенство при преобразованиях записей. Я попытался выразить суть моей проблемы в небольшом примере. Рассмотрим следующий тип записи...
447 просмотров
schedule
20.04.2022
Использование идиоматического логического равенства (синглетоны)
Я хочу создать структуру данных для хранения элементов, помеченных на уровне типа, с помощью Symbol. Этот:
data Store e (ss :: [Symbol]) where
Nil :: Store e '[]
Cons :: e s -> Store e ss -> Store e (s ': ss)
data HasElem (a :: k) (as...
286 просмотров
schedule
04.03.2024
Можно ли отменить обходы по типу?
Здесь много настроек. Если вы когда-либо видели последовательность, выровненную по типу, вы можете просмотреть все до строки.
Выровненная по типам последовательность — это все, что отдаленно похоже на
data ConsList c x y where
CNil ::...
225 просмотров
schedule
02.09.2022
Застрял на простом доказательстве равенства
Я пытаюсь реализовать некоторые матричные операции и доказательства вокруг них в Agda. В коде есть что-то вроде следующих определений:
open import Algebra
open import Data.Nat hiding (_+_ ; _*_)
open import Data.Vec
open import...
184 просмотров
schedule
29.05.2022
Равенство значений не распространяется на типы в зависимости от этих значений; я что-то упускаю?
Я пытаюсь реализовать как можно больше System F (полиморфное лямбда-исчисление) в Idris. Теперь я столкнулся с проблемой, которую хочу продемонстрировать на примере:
data Foo = Bar Nat
Eq Foo where
(Bar _) == (Bar _) = True
data Baz: Foo ->...
119 просмотров
schedule
13.08.2022
Самостоятельный тип Scala с зависимой типизацией
Это не компилируется:
trait FileSystem {
type P <: Path[this.type]
}
trait Path[S <: FileSystem] { self: fileSystem.P =>
val fileSystem: S
}
Как ограничение собственного типа может зависеть от члена-значения в этом свойстве?
146 просмотров
schedule
20.10.2023
Индексирует ли числовой тип Пеано тип, зависящий от сигмы или пи?
Итак, я столкнулся с зависимой типизацией на Scala Exchange (по адресу это talk), и спикер привел пример, в котором он индексировал вектор, используя числа Пеано, и использовал его для кодирования свойств операций над вектором в типах этих операций...
242 просмотров
schedule
28.08.2022
