Вопросы по теме 'dependent-type'
Как сделать Vect n Int экземпляром Monoid
В Идрисе Vect n a - это тип данных, представляющий вектор длиной n, содержащий элементы типа a. Представьте, что у меня есть функция:
foo : Int -> Vect 4 Int
foo n = [n-1, n, n+1, n*4]
Тело функции не важно, это может быть что угодно,...
403 просмотров
schedule
18.10.2021
Идрис: арифметика для ограниченного двойника
Я новичок в Идрисе. Мне нужно создать данные, описывающие ограниченное число. Итак, я сделал такие данные с помощью такого конструктора:
data BoundedDouble : (a, b : Double) -> Type where
MkBoundedDouble : (x : Double) ->...
193 просмотров
schedule
18.09.2021
Использование Idris Vect.fromList со сгенерированным списком
Я пытаюсь нащупать свой путь к зависимым типам. Основываясь на приведенной ниже логике функции windowl , я хочу вернуть список векторов, длина которых зависит от предоставленного размера .
window : (n : Nat) -> List a -> List (Vect n a)...
415 просмотров
schedule
03.10.2021
Зависимый тип Scala не компилируется
Этот код должен компилироваться на Scala:
trait Pipe {
type Input
type Output
def apply(input: Input): Output
}
object Pipe {
trait Start extends Pipe {
override type Input = Seq[String]
}
abstract class Connect(val prev: Pipe)...
122 просмотров
schedule
24.11.2021
TypeScript: как сделать так, чтобы общий тип выводился внутри функции?
Я изо всех сил пытаюсь уменьшить тип аргумента функции внутри этой функции. На мой взгляд, всякий раз, когда я выполняю if -проверку, которая сокращает возможные значения до меньшего подмножества, средство проверки типов уменьшает тип. Что меня...
427 просмотров
schedule
29.10.2021
Общее программирование с помощью эффектов
В библиотеке эффектов Idris Effects есть представлен как
||| This type is parameterised by:
||| + The return type of the computation.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type...
1740 просмотров
schedule
20.02.2022
Могу ли я написать универсальную функцию-оболочку для интерфейса Wrapper, представляющего тип, который является оболочкой для какого-то другого типа?
Полный пример кода ниже (который успешно компилируется) является упрощенным и слегка надуманным примером моей проблемы.
NatPair - это пара Nat , и я хочу «поднять» бинарные Num операции до NatPair точечно, используя функцию...
63 просмотров
schedule
16.03.2022
Определите индуктивный зависимый тип с ограничениями на параметр типа
Я пытаюсь определить индуктивный зависимый тип в Coq для представления бит-векторных переменных в бит-векторной логике.
Я прочитал это сообщение в блоге Ксавье Лероя, в котором он определяет такую структуру следующим образом:
Require Import...
522 просмотров
schedule
26.03.2022
Выполнение количественной оценки ранга n в Идрисе
В Idris 0.9.12 я могу делать только типы rank-n довольно неуклюже:
tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)
Мне нужны подчеркивания везде, где есть приложение типа, потому что Идрис...
1672 просмотров
schedule
02.04.2022
Как переписать тело функции в Идрисе так, чтобы тип соответствовал сигнатуре функции и все это компилировалось
Я бы хотел, чтобы это скомпилировали:
foo: Vect n String -> Vect n String
foo {n} xs = take n xs
Это не может быть скомпилировано, потому что компилятор не может объединить n с n + m . Я понимаю, что это из-за подписи take для Vect,...
706 просмотров
schedule
01.04.2022
Распределимость `subst`
Предположим, у меня есть транзитивное отношение ~ с двумя эндокартами f и g . Предполагая, что f и g соглашаются везде и f a ~ f b ~ f c , тогда есть два способа показать g a ~ g c : преобразовать каждый f в g по заданному равенству,...
128 просмотров
schedule
30.04.2022
Coq: Как правильно запомнить зависимые значения, не испортив гипотезу индукции?
У меня есть схема индукции для вектора, содержащего значение leb ( x <= y ),
Definition vector_ind_with_leb : forall (A : Type) (P : forall n y: nat, y <= n -> vector A n -> Prop),
(forall (n : nat) (y : nat) (H : S y <= S n)...
169 просмотров
schedule
09.05.2022
Всего постоянных очередей в реальном времени
Окасаки описывает постоянные очереди реального времени, которые могут быть реализованы в Haskell с использованием типа
data Queue a = forall x . Queue
{ front :: [a]
, rear :: [a]
, schedule :: [x]
}
где инкрементальные вращения...
435 просмотров
schedule
14.05.2022
Agda - разница между аргументами типа слева и справа от двоеточия
Следующее определение компилируется и ведет себя хорошо:
data Eq {lvl} {A : Set lvl} (x : A) : A → Set where
refl : Eq x x
Однако этот не компилируется:
data Eq {lvl} {A : Set lvl} (x : A) (y : A) : Set where
refl : Eq x x
так как...
134 просмотров
schedule
17.05.2022
Ограничение типа функции с помощью интерфейса Idris
Я хотел бы создать функцию с типом, ограниченным интерфейсом. Я намерен создать простой решатель моноидов, используя VerifiedMonoid определенный модуль in Classes.Verified из пакета contrib.
Идрис выдает следующую ошибку:
Monoid-prover.idr...
226 просмотров
schedule
01.06.2022
Как определить тип пары в Idris, который содержит только определенные комбинации значений
Я пытаюсь узнать о зависимых типах в Идрисе, пытаясь сделать что-то далекое от моей глубины. Пожалуйста, потерпите меня, если я сделаю глупые ошибки.
Учитывая простой тип
data Letter = A | B | C | D
Я хотел бы определить тип LPair ,...
196 просмотров
schedule
28.05.2022
Преобразуйте случайный список в список с зависимой типизацией в Coq
У меня есть следующее определение списка в Coq:
Variable A : Set.
Variable P : A -> Prop.
Hypothesis P_dec : forall x, {P x}+{~(P x)}.
Inductive plist : nat -> Set :=
pnil : plist O
| pcons : A -> forall n, plist n -> plist n
|...
80 просмотров
schedule
31.05.2022
Поддерживает ли Perl6 зависимые типы?
Недавно я просматривал страницу википедии для зависимых типов , и мне было интересно; действительно ли Perl 6 вводит зависимые типы? Кажется, я не могу найти надежный источник, подтверждающий это.
Для кого-то это может быть очевидно, но для меня...
628 просмотров
schedule
04.06.2022
Последовательность над разнородным списком в Haskell
Рассмотрим следующее определение HList :
infixr 5 :>
data HList (types :: [*]) where
HNil :: HList '[]
(:>) :: a -> HList l -> HList (a:l)
И семейство типов Map для сопоставления списков уровней типов:
type family Map...
212 просмотров
schedule
28.06.2022
Автоматическое определение домена для функции зависимого типа в Idris
Учебник по языку Idris содержит простой и понятный пример идеи зависимых типов : http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types
Вот код:
isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False =...
209 просмотров
schedule
07.07.2022
