Вопросы по теме 'idris'
С чего начать программирование зависимого типа?
Существует учебник Idris, учебник Agda и многие другие документы в стиле учебника и вводные материалы с бесконечными ссылками на вещи, которые еще предстоит изучить. Я как бы ползаю посреди всего этого и большую часть времени застреваю в...
2879 просмотров
schedule
27.09.2022
Тип Cong, subst и равенство в языках программирования с зависимой типизацией
В теории зависимо типизированных типов есть тип равенства. Обычно при определении этого типа вводится ряд утилит, а именно cong и subst. Насколько они выразительны? Можно ли выразить все, что можно, с помощью элиминатора на равенство с ними?
242 просмотров
schedule
18.06.2023
Как установить ограничение типа для типа данных в idris
Как в idris ограничить тип параметров в алгебраическом типе данных?
В haskell я бы сделал:
data Foo = Bar {x :: Integer, str :: String}
Могу ли я сделать это в Идрисе?
633 просмотров
schedule
06.11.2023
Как мне доказать, казалось бы, очевидный факт, когда соответствующие типы абстрагируются лямбдой в Идрисе?
Я пишу базовый монадический парсер в Idris, чтобы привыкнуть к синтаксису и отличиям от Haskell. У меня есть основы, которые работают нормально, но я застрял на попытке создать экземпляры VerifiedSemigroup и VerifiedMonoid для парсера.
Без лишних...
1015 просмотров
schedule
26.03.2022
Можете ли вы создать функции, возвращающие функции зависимой арности на языке с зависимой типизацией?
Исходя из того, что я знаю о зависимых типах, я думаю, что это должно быть возможно, но я никогда раньше не видел такого примера на языке с зависимой типизацией, поэтому я не совсем уверен, с чего начать.
Я хочу, чтобы функция формы:
f : [Int]...
673 просмотров
schedule
11.01.2023
Внедрение Total Parsers в Idris на основе статьи на Agda
Я пытаюсь реализовать общие парсеры с Idris на основе этой статьи . Сначала я попытался реализовать более простой тип распознавателя P :
Tok : Type
Tok = Char
mutual
data P : Bool -> Type where
fail : P False
empty : P True...
451 просмотров
schedule
05.09.2022
Дело Идриса / тактика индукции
Они были реализованы в Idris 0.9.14, и я успешно использовал induction для некоторых доказательств. Однако они работают только для некоторых типов библиотек; в то время как, например, Vect поддерживает их, почти изоморфный All - нет:...
301 просмотров
schedule
01.02.2023
Где и почему я должен использовать лишние пустые шаблоны?
Например:
intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy _ [] _ = []
intersectBy _ _ [] = []
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
Есть дополнительные шаблоны для []...
716 просмотров
schedule
15.04.2022
Как указать неявный аргумент явно?
Предположим, у меня есть функция с такой сигнатурой:
myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n
Пытаюсь применить вот так myNatToFin k (S k) в теле другой функции и получаю ошибку:
Can't solve goal...
516 просмотров
schedule
03.03.2023
Почему Idris не принимает мой пользовательский фолд?
Вот вектор, элементы которого индексируются по длине вектора.
data IxVect : (n : Nat) -> (a : Nat -> Type) -> Type where
Nil : IxVect 0 a
(::) : a n -> IxVect n a -> IxVect (S n) a
Я хочу сложить IxVect .
total...
301 просмотров
schedule
28.05.2023
несоответствие типов между предполагаемым значением и длиной вектора
Попытка выполнить упражнение об умножении матриц в Разработка с использованием типов с помощью Idris привел меня к досадной проблеме.
Пока что я определил набор вспомогательных функций вроде этого:
morexs : (n : Nat) -> Vect m a ->...
310 просмотров
schedule
21.03.2022
Как я могу печатать функции в Node.js так же, как Firefox печатает функции (а именно дает имя)?
var fun1=function(){console.log('hello');}
var fun2=fun1
console.log(fun2);
Приведенный выше код, запущенный в Firefox, печатает fun2 . В Chrome он печатает тело функции, в Node.js — Function .
Почему эта разница?
Как я могу получить...
85 просмотров
schedule
02.05.2023
Как отменить HVect в Идрисе?
Я новичок в Irdis. Можно ли отменить HVect ? Если я вызываю реверс для HVect [String, Int] , он должен вернуть HVect [Int, String] , а если я вызываю обратный для HVect [String, Int, Day] , он должен возвращать HVect [Day, Int, String] .
Я...
219 просмотров
schedule
26.03.2023
Определите, делится ли сумма Vect n Nat равномерно на 5?
Cactus продемонстрировал, как ответить на мой вопрос: Вспомогательная функция для определения, если Nat` mod` 5 == 0 .
Он написал:
onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n
Затем я попытался...
75 просмотров
schedule
02.11.2022
Определите, является ли `Nat mod 5 = 0` во время компиляции в Scala
Этот ответ демонстрирует, как написать функцию в Idris, чтобы определить, является ли Nat mod 5 = 0 во время компиляции:
onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n
Тесты:
*Test> onlyModBy5...
126 просмотров
schedule
13.01.2023
Определите функцию равенства списков
Type-Driven Development with Idris представляет это упражнение:
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
Однако я попытался реализовать его через:
data EqList : (xs : List a) -> (ys : List a)...
120 просмотров
schedule
22.01.2023
В Идрисе, как добавить 1 к плавнику, пока не будет достигнут максимум
У меня есть тип данных, который принимает число в конструкторе, и это число ДОЛЖНО быть между 1 и 5 (представлено как 0..4):
import Data.Fin
data Stars = MkStars (Fin 5)
Я хочу создать функцию, которая добавляет единицу к существующему star...
272 просмотров
schedule
08.12.2022
DPair проиндексирован по Fin
Я следую учебнику Idris и хочу поэкспериментировать с зависимыми парами и Fin.
Следующий код не печатает check в Idris.
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
P : (Fin 1) -> Type
P FZ = Char
vec...
70 просмотров
schedule
16.06.2022
Именованные v аргументы безымянного типа данных
В коде из главы 6 Тип-ориентированная разработка с Idris , я озадачил этот код:
data DataStore : Type -> Type where
MkData : (size : Nat) ->
(items : Vect size schema) ->
DataStore schema
Я думал, что...
153 просмотров
schedule
29.03.2022
Почему зависимые типы в Idris не могут справиться с этой ситуацией?
Я хочу сделать следующее:
data Foo : (a : Type) -> (b : Type) -> (c : a -> b -> Type) -> Type where
Bar : a -> (c a) -> Foo a b c
но я получаю следующую ошибку:
When checking type of test.Bar:
When checking argument...
171 просмотров
schedule
09.07.2022
