Публикации по теме 'idris'
Действительно хорошая статья! 😻
Действительно хорошая статья! 😻
Я только утверждаю, что Either придерживается либо левого, либо правого, но не обоих одновременно, так что Either, верно? 😉 По крайней мере, с точки зрения Haskell / Idris это так - Either - это тип данных, который имеет два однопараметрических конструктора Left и Right.
Что касается Typescript ... Я не большой поклонник, хотя мне приходится много с ним работать. И ИМХО TS сильно нуждается в действительно хорошем выводе типа (иногда нужно..
Вопросы по теме 'idris'
Зависимо типизированный printf в Idris
Я пытаюсь перевести на Идрис пример из Cayenne — языка с зависимыми типами бумага .
Вот что у меня есть до сих пор:
PrintfType : (List Char) -> Type
PrintfType Nil = String
PrintfType ('%' :: 'd' :: cs) = Int ->...
1095 просмотров
schedule
18.08.2022
Я не могу доказать (n - 0) = n с Идрисом
Я пытаюсь доказать, что, на мой взгляд, является разумной теоремой:
theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m
Доказательство по индукции доходит до того, что мне нужно это доказать:
lemma1 : (n : Nat) -> (n - 0) = n...
2067 просмотров
schedule
20.03.2023
Разница между параметрами типа и индексами?
Я новичок в зависимых типах, и меня смущает разница между ними. Кажется, люди обычно говорят, что тип параметризуется другим типом и индексируется некоторым значением . Но разве нет различия между типами и терминами в языке с зависимой...
3134 просмотров
schedule
26.09.2022
Синтаксическая ошибка при использовании представлений
У меня есть следующий код (в основном сгенерированный автоматически, играя с idris-mode в emacs):
module Main
data Parity : Nat -> Type where
even : (n : Nat) -> Parity (n + n)
odd : (n : Nat) -> Parity (S (n + n))
parity : (n :...
83 просмотров
schedule
30.10.2022
Идрис: заставить векторные суммы быть равными
Я пытаюсь изучить Идрис, перестраивая (более простым способом) некоторые вещи, которые мы недавно делали на работе.
Я хотел бы иметь тип данных, который моделирует главную книгу с вектором кредитов и вектором дебетов. Я зашел так далеко:
data...
125 просмотров
schedule
10.05.2023
Квантификатор Forall и комплексные логические предложения в Idris
Я новичок в зависимых типах и, имея опыт работы с Haskell, медленно изучаю Idris. В качестве упражнения я хочу написать кодировку Хаффмана. В настоящее время я пытаюсь написать доказательство того, что «сглаживание» дерева кода дает префиксный код,...
409 просмотров
schedule
15.07.2022
Неразрешимая метапеременная для функции, у которой нет обитаемых аргументов
Я получаю нерешенную метапеременную для foo в приведенном ниже коде:
namespace Funs
data Funs : Type -> Type where
Nil : Funs a
(::) : {b : Type} -> (a -> List b) -> Funs (List a) -> Funs (List a)
data FunPtr : Funs a...
62 просмотров
schedule
11.08.2023
Есть ли поддержка регулярных выражений в Idris?
Я не вижу регулярного выражения в документации Idris, поддерживается ли оно каким-либо (предпочтительно переносимым) способом? Или планируется?
374 просмотров
schedule
18.10.2022
Как я могу организовать сопоставление с образцом в зависимом представлении?
Я написал несколько простых типов для просмотра значений 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
Общий сумматор от Idris до Scala?
Разработка на основе типов с помощью Idris представляет следующий общий подход к суммированию:
AdderType : (numArgs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next : Int) -> AdderType k
adder : (n : Nat) -> (acc : Int)...
333 просмотров
schedule
31.07.2023
Используете rewrite для моего собственного равенства?
У меня есть следующее определение равенства:
data Equal : x -> y -> Type where
Reflexive : Equal a a
Когда я хочу использовать синтаксис rewrite , мне нужно что-то типа (a = b) , поэтому я создал:
makeEquitable : Equal x y...
118 просмотров
schedule
03.11.2022
Тип данных, охватывающий два типа суммы?
Учитывая эти 2 типа суммы:
data Foo = A Int | B String
data Bar = C Int | D String
Я хотел бы определить функцию, которая возвращает Either (Foo or Bar) String .
Итак, я попытался сделать:
data Higher = Foo | Bar
Но не удалось...
208 просмотров
schedule
25.02.2023
Ограничение аргумента функции в интерфейсе
Каков синтаксис для ограничения аргумента функции в интерфейсе, который принимает функцию? Я попытался:
interface Num a => Color (f : a -> Type) where
defs...
Но там написано Name a is not bound in interface...
176 просмотров
schedule
03.01.2023
Определение экземпляра функтора для тензорного типа (Идрис)
Недавно я изучал Идрис и решил попробовать написать простую тензорную библиотеку. Я начал с определения типа.
data Tensor : Vect n Nat -> Type -> Type
Scalar : a -> Tensor [] a
Dimension : Vect n (Tensor d a) -> Tensor (n::d) a...
162 просмотров
schedule
28.07.2022
Вычисление нетривиального типа Идриса для тензорной индексации
Я возился с простой тензорной библиотекой, в которой я определил следующий тип.
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
Можно ли создать представление общих АТД на уровне типов?
Используя кодировку Черча, можно представить любой произвольный алгебраический тип данных без использования встроенной системы АТД. Например, Nat можно представить (пример в Идрисе) как:
-- Original type
data Nat : Type where
natSucc : Nat...
231 просмотров
schedule
12.12.2023
Равенство значений не распространяется на типы в зависимости от этих значений; я что-то упускаю?
Я пытаюсь реализовать как можно больше System F (полиморфное лямбда-исчисление) в Idris. Теперь я столкнулся с проблемой, которую хочу продемонстрировать на примере:
data Foo = Bar Nat
Eq Foo where
(Bar _) == (Bar _) = True
data Baz: Foo ->...
119 просмотров
schedule
13.08.2022
Идрис Дек против Может быть
Какие вещи можно выразить с помощью Dec , а не с помощью Maybe в Идрисе ?
Или другими словами: когда следует выбирать Dec и когда Maybe ?
364 просмотров
schedule
11.01.2023
