Публикации по теме 'idris'
Изучение Идриса: Relexivity Tactics one up Модульные тесты
Idris — это язык программирования с параметрическим полиморфизмом (вспомните дженерики), зависимыми типами (в качестве членов первого класса языка), средством проверки целостности (вспомните проблему остановки) и синтаксисом, подобным Haskell. Мои первые наблюдения за языком связаны с другой особенностью — синтаксисом доказательства.
Большинство инженеров знакомы с модульными тестами, независимо написанными и автоматизированными тестами очень маленьких битов (модулей) кода. Обычно это..
Конечные автоматы Идриса в приложениях JavaScript
Написание приложений JavaScript, которые ведут себя так, как вы хотите, сложно. Поскольку JavaScript динамически типизирован, программист обычно не получает от интерпретатора указания, если в его программе есть ошибка.
В этой статье я собираюсь продемонстрировать способ разработки приложений JavaScript с использованием функционального языка программирования с зависимой типизацией Idris . Зависимый тип - это тип, определение которого зависит от другого значения. Вы можете определять..
Вопросы по теме 'idris'
Литералы Идриса Ната в типах
Я хочу, чтобы Идрис доказал, что testMult : mult 3 3 = 9 обитаем.
К сожалению, это набирается как
mult (fromInteger 3) (fromInteger 3) = fromInteger 9 : Type
Я могу обойти это так:
n3 : Nat; n3 = 3
n9 : Nat; n9 = 9
testMult : mult n3...
374 просмотров
schedule
25.06.2022
Пользовательская тактика прувера в Идрисе
Если я правильно понимаю (в основном из-за наличия функции applyTactic ), то можно написать собственную тактику для доказателя теорем в Идрисе. Какие (или где) примеры я мог бы использовать, чтобы узнать, как это сделать?
726 просмотров
schedule
03.08.2022
Установка idris cabal не удалась. Следующие пакеты могут быть повреждены при переустановке
Сначала я выполняю процесс обновления/обновления Cabal, поэтому у меня есть cabal-install-1.20.0.3. Затем я делаю:
cabal install idris
Я получил:
...
idris-0.9.14.1 (new version)
The following packages are likely to be broken by the...
1308 просмотров
schedule
25.06.2023
Используя гетерогенное равенство с =
Что у меня есть до сих пор:
module Foo
postulate P : 'P
postulate NP : 'NP
complexityProof : P = NP
complexityProof = ?complexityProof_rhs
Но при попытке загрузить файл я просто получаю:
When elaborating type of Foo.complexityProof:...
327 просмотров
schedule
11.10.2022
Idris - использовать неявную переменную внутри функции
Как мы можем использовать неявную переменную внутри функции? Сводя к простейшему возможному случаю, можно ли иметь:
dim : Vect n a -> Nat
dim vec = n
без получения ошибки:
When elaborating right hand side of rep:
No such variable n...
294 просмотров
schedule
30.03.2023
Пример «Типа 1», который не является ни «Типом», ни обитателем «Типа».
Каков пример жителя Type 1 , который не является ни Type , ни жителем Type ? Я не мог ничего придумать, исследуя Idris REPL.
Чтобы быть более точным, я ищу некоторые x , отличные от Type , которые дают следующее:
Idris> :t x
x : Type 1
186 просмотров
schedule
12.07.2023
Генерация доказательств во время выполнения с предикатами типов в Idris
Я использую этот тип, чтобы рассуждать о строках, для которых может быть выполнен разрешимый синтаксический анализ:
data Every : (a -> Type) -> List a -> Type where
Nil : {P : a -> Type} -> Every P []
(::) : {P : a -> Type}...
643 просмотров
schedule
26.06.2022
Сообщите зависимой функции в ветке условного оператора, что условие истинно
У меня есть функция с сигнатурой типа (x, y : SomeType) -> (cond x y) = True -> SomeType . Когда я проверяю условие в операторе if-then-else/case/with, как мне передать функции в соответствующей ветке тот факт, что это условие истинно?
1082 просмотров
schedule
14.06.2023
idris-mode — в буфере *idris-repl* нет процесса
Я пытаюсь заставить работать режим idris. Я использую HEAD как из idris-dev , так и из idris-mode . Всякий раз, когда я запускаю C-l (idris-load-file), я получаю эту ошибку
Debugger entered--Lisp error: (file-error "make client process failed"...
258 просмотров
schedule
07.03.2023
Генерировать библиотеку вместо исполняемого файла в Idris?
Есть ли способ создать библиотеку вместо исполняемого файла с помощью idris ? Если я попытаюсь скомпилировать без main , я получу такую ошибку:
main:0:0:When elaborating an application of function run__IO:
No such variable Main.main...
1474 просмотров
schedule
14.02.2023
Как лучше всего использовать число во время компиляции и выполнения?
Я только начинаю изучать Идрис и решил, что для начала неплохо было бы реализовать конечные последовательности в виде деревьев на 2-3 пальца. Каждый внутренний узел в дереве необходимо аннотировать во время выполнения с указанием общего количества...
95 просмотров
schedule
21.09.2022
Какой хороший способ представлять свободные группы?
Легко представить свободные магмы (бинарные листовые деревья), свободные полугруппы (непустые списки) и свободные моноиды (списки), и несложно доказать, что они на самом деле являются тем, за что себя выдают. Но бесплатные группы кажутся намного...
146 просмотров
schedule
14.05.2022
Как сопоставить пару/кортеж?
В Haskell я бы сделал join (***) . В Идрисе flatten (***) не работает ( (***) сложно).
222 просмотров
schedule
08.10.2022
Доказать карту id = id в idris?
Я только начинаю играть с идрисом и доказательством теорем в целом. Я могу следовать большинству примеров доказательства основных фактов в Интернете, поэтому я хотел попробовать что-то произвольное самостоятельно. Итак, я хочу написать доказательный...
369 просмотров
schedule
15.07.2022
StringOrInt от Idris -> Scala?
Разработка на основе шрифтов с помощью Idris представляет эту программу:
StringOrInt : Bool -> Type
StringOrInt x = case x of
True => Int
False => String
Как такой метод можно написать на Scala?
752 просмотров
schedule
17.06.2022
(xs: Vect n elem) - ›Vect (n * 2) elem
В книге Type-Driven Development with Idris представлено это упражнение:
Определите возможный метод, соответствующий подписи:
two : (xs : Vect n elem) -> Vect (n * 2) elem
Я пытался:
two : (xs : Vect n elem) -> Vect (n * 2)...
228 просмотров
schedule
16.04.2022
Любые приемы, чтобы избавиться от шаблона при построении доказательств абсурдного предиката на перечислениях?
скажем, у меня есть
data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}
и предикат для этого типа,
data WineStock : Fruit -> Type where
CanonicalWine : WineStock Grape
CiderIsWineToo : WineStock Apple...
358 просмотров
schedule
05.08.2022
Как определить все подразмеры HVect?
Я хотел бы определить все подразмеры HVect как HVect .
Пример:
import Data.HVect
myHVect : HVect [Int, String, List Nat]
myHVect = [42, "text", [1, 2, 3]]
subDimensions : HVect [ HVect [Int], HVect [Int, String], HVect [Int, String, List...
76 просмотров
schedule
02.09.2022
Функция для определения, делится ли Nat на 5 во время компиляции
Использование полезного ответа Cactus я попытался написать функцию, которая при наличии Nat вернет Nat , если оно делится на 5 .
onlyModBy5Helper : (n : Nat) -> (k : Nat ** k `mod` 5 = 0) -> Nat
onlyModBy5Helper n k = n
И...
122 просмотров
schedule
27.06.2023
Как сравнить типы на равенство?
Я попытался сравнить String и String , ожидая True .
Idris> String == String
Can't find implementation for Eq Type
Тогда я ожидал False при сравнении String с Bool .
Idris> String /= Bool
Can't find implementation for Eq...
873 просмотров
schedule
21.03.2023
