Описание тега idris

Описание тега Вопросы с тегом
Idris is a general purpose pure functional programming language with dependent types.
1 ответ

Идрис: арифметика для ограниченного двойника

Я новичок в Идрисе. Мне нужно создать данные, описывающие ограниченное число. Итак, я сделал такие данные с помощью такого конструктора: data BoundedDouble : (a, b : Double) -> Type where MkBoundedDouble : (x : Double) -> {auto p : a <= x &…
31 май '16 в 22:09
1 ответ

Идрис: Написание функции начальных сегментов для векторов с длиной как фин, а не как натуральный

Я пытаюсь написать функцию начальных сегментов для векторов, которая хранит длину вектора в виде Fin, а не Nat, следующим образом: vectorsInits : Vect n t -> Vect n (p ** Vect (finToNat p) t) vectorsInits Nil = Nil vectorsInits (x::xs) = ((FS FZ)…
29 апр '18 в 15:02
1 ответ

Как порядок неявных аргументов влияет на idris?

Это не удается: > the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair (input):1:5:When checking argument value to function Prelude.Basics.the: Type mismatch between A -> B1 -> (A, B1) (Type of MkPair) and A1 -> B -> …
21 окт '17 в 01:18
1 ответ

Идрис: Можно ли переписать все функции, используя "с", чтобы использовать "case" вместо "с"? Если нет, не могли бы вы привести контрпример?

Можно ли в Idris переписать все функции, используя " с", чтобы использовать "case" вместо "с"? Если нет, не могли бы вы привести контрпример?
24 фев '16 в 18:41
0 ответов

Почему в Idris параметры интерфейса должны быть типом или конструктором данных?

Чтобы немного попрактиковаться с Idris, я пытался представить различные базовые алгебраические структуры в качестве интерфейсов. Сначала я решил организовать вещи так, чтобы параметры заданного интерфейса были заданы, а различные операции над ним, а…
26 май '18 в 20:10
3 ответа

Являются ли списки индуктивными или индуктивными в Хаскеле?

Так что в последнее время я читаю о коиндукции, и теперь мне интересно: списки на Haskell индуктивны или коиндуктивны? Я также слышал, что Хаскелл не различает их, но если да, то как они делают это формально? Списки определяются индуктивно, data [a]…
04 окт '16 в 14:09
0 ответов

Проверка целостности с косвенными взаимно рекурсивными типами данных в Idris

Я работаю с абстрактным синтаксическим деревом, где я хотел бы дать связующим их собственный тип. Это, кажется, вызывает проблемы для проверки целостности Идриса... С типичной референцией Tree Идрис прекрасно справляется с проверкой целостности. dat…
09 дек '18 в 18:15
1 ответ

Именованная реализация к реализации по умолчанию

Я определил именованную реализацию для класса типов Ord для типа Int. [mijnOrd] Ord Int where compare n1 n2 = ... Как я могу импортировать эту именованную реализацию и использовать ее как "по умолчанию" поэтому в другом модуле я хочу импортировать э…
18 май '16 в 13:41
0 ответов

idirs-vim <leader>c иногда удаляет строку

Я начинаю с idris и idris-vim. Но иногда \c (IdrisCaseSplit) удаляет строку, на которой я нахожусь. Я пытаюсь с помощью следующей программы: vApp : Vect n (a -&gt; b) -&gt; Vect n a -&gt; Vect n b затем я наведу курсор на vApp и нажмите \d и я получ…
11 окт '14 в 02:09
1 ответ

Модуль Network.Socket не найден в Идрисе

Я пытаюсь импортировать сокет в Идрис в REPL: Idris&gt; :module Network.Socket Can't find import Network/Socket Зачем?
20 май '17 в 21:31
0 ответов

Обозначение синтаксиса сахар для списка и сделать нотации

Итак, я заметил, что в Idris вы определяете свой собственный список или векторный тип, например, следующий тип, который я считаю полезным: data HFVec : (f : Type -&gt; Type) -&gt; (n : Nat) -&gt; Vec n Type -&gt; Type where Nil : HFVec f Z [] (::) :…
13 июн '17 в 12:39
2 ответа

Подпись типа "половина" в Idris

Я довольно новичок в Идрисе и пытаюсь уловить основные понятия и синтаксис. Даже если это может показаться бессмысленным, я пытаюсь определить half функция, которая наполовину естественная. Я хочу придумать что-то вроде: half : (n : Nat) -&gt; (k : …
30 ноя '16 в 22:30
1 ответ

Представление индуктивных типов

Я реализовал лямбда-исчисление с зависимой типизацией в духе этой статьи: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf Исчисление, работает, и я экспериментировал с ним и расширил несколько вещей: много вселенных, жестко закодированная индукция а…
12 мар '14 в 02:28
3 ответа

StringOrInt от Идрис -> Скала?

Type Driven Development с Idris представляет эту программу: StringOrInt : Bool -&gt; Type StringOrInt x = case x of True =&gt; Int False =&gt; String Как можно написать такой метод в Scala?
20 ноя '15 в 04:03
1 ответ

Работа с функциями, которые принимают ненулевые натуральные числа

Я пытаюсь определить функцию (congruentialMethod) в Идрисе, который среди прочего применяет арифметику модуля к некоторым аргументам, приведенным в моей функции. Модуль арифметики требует, чтобы второй аргумент был ненулевым, поэтому я попытался исп…
26 май '18 в 18:48
2 ответа

Почему эта проверка типа фрагмента Идриса не имеет явного типа?

Я только начинаю изучать Idris и работаю над книгой Type Driven Development с Idris. Одним из примеров упражнений из второй главы является написание функции, которая по заданной строке определяет среднюю длину слова в этой строке. Мое решение было с…
14 июл '17 в 02:59
1 ответ

Индексируется по типу против содержащему тип в idris

В настоящее время я прорабатываю разработку с использованием типов с книгой Idris. У меня есть два вопроса, относящихся к дизайну примера хранилища данных в главе 6. Хранилище данных - это приложение командной строки, которое позволяет пользователю …
04 авг '17 в 10:05
1 ответ

Преобразование Coq в Идрис

Каковы были бы некоторые полезные рекомендации для преобразования источника Coq в Idris (например, насколько похожи их системы типов и что можно сделать, переведя доказательства)? Из того, что я понял, встроенная библиотека тактики Идриса минимальна…
02 май '14 в 20:56
1 ответ

Медленная проверка типов и низкая производительность во время выполнения с большими натуральными числами в Idris 1.2.0

Я занимался созданием собственного генератора случайных чисел в Идрисе для целей обучения. В моем решении я стремлюсь к совокупности всех функций и, следовательно, я использую числа типа Nat и встроенная функция modNatNZ что требует доказательства т…
23 июн '18 в 21:39
1 ответ

Конструктор типа без параметров, вызывающий ошибку "Не могу определить аргумент"

Я определил тип как это: data MyList a = Empty | Cons a (MyList a) В Хаскеле пусто MyList может быть создан с помощью EmptyИдрис жалуется: &gt; Empty (input):Can't infer argument a to Empty Это почему?
17 апр '18 в 13:57