Questions tagged [idris]
Idris is a general purpose pure functional programming language with dependent types.
790
questions
0
votes
1
answer
44
views
Can any dynamic language can write the some prog like the book<Type-Driven Development with idris>'s Chapter6's datastore? [closed]
The book's Chapter6's datastore:
module Main
import Data.Vect
infixr 5 .+.
data Schema = SString | SInt | (.+.) Schema Schema
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType ...
0
votes
1
answer
36
views
Cannot match two identical types
I don't really know how to properly address this since I'm new to Idris, so I'll tell my story.
I was implementing a type-safe sprintf function, with the following type signature:
sprintf : (s: String)...
0
votes
0
answers
34
views
Idris prove termination of proof without assert_smaller
I am proving a theorem using Idris and in the proof, I am applying the theorem itself to the hypotheses. However, I cannot apply it the hypotheses directly; I have to do a rewrite. Because of this, ...
0
votes
1
answer
44
views
Idris: rewrite does not work (rewriting by ... did not change)
I'm proving a theorem in Idris, and in the 2nd case:
theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let
(s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u
hyp1' = rewrite ueq in hyp1
in case ...
0
votes
2
answers
36
views
What is the equivalent of mapM and mapM_ in idris2?
I know there is the mapM function that applies a monadic action to a list and returns one monadic value containing a list. (See e.g.
What is the difference between mapM_ and mapM in Haskell?)
But I ...
1
vote
0
answers
41
views
How to generate a Decidable inequality proof in Idris2?
I know that Decidable.Equality has decDeq to be used for generating proofs about equality. For example, from this SO question, one can use decEq to decide if the length of a List is equal to the ...
2
votes
0
answers
52
views
How to write a pure function in idris2 FFI?
The idris2 has the following example for FFI, which adds two integers in C:
#include <stdio.h>
int add(int x, int y) {
return x+y;
}
(small.c)
I followed the steps, and after linking:
gcc -...
0
votes
0
answers
18
views
Updating a dependently typed field without updating what it depends on
I'd like to use record update syntax to update a dependently-typed field without also changing the field it depends on. So I'd like to have Idris 2 evaluate the other field, and realize everything is ...
3
votes
3
answers
88
views
Does idris support a way to collapse symmetrical statements into one?
I'm new to functional programming, so working through 'Type Driven Development with Idris'.
Give a function maxMaybe that can compute the max between two Maybe Doubles, defines as below
maxMaybe : Ord ...
1
vote
2
answers
60
views
Selecting a named implementation in Idris 2
According to this old answer, Idris 1 has the using syntax to select default implementations for a block of code. What is the corresponding Idris 2 syntax?
I've tried using the syntax from the answer:
...
0
votes
1
answer
39
views
How to use the result of a depedent pair?
I am learning dependent pairs in idris and couldn't understand how one can use it. For example, if I filter a Data.List, I get back a Data.List, which you I do sum or other computations on.
sum $ ...
4
votes
4
answers
227
views
Mapping functions over data in 'sum-types' in strongly typed programming languages
Today I encountered an implementation challenge with a large DU (sum-type) in F#, where I basically wanted to be able to map a set of functions over the values of the DU without having to repeat the ...
0
votes
0
answers
50
views
How to fix an inaccessible variable in idris2?
I am having trouble to make a short idris2 code from the summer school course SPLV20 work. The error is at the last line:
module Text.Token
%default total
||| For a type `kind`, specify a way of ...
2
votes
0
answers
44
views
Destructuring result of applying a linear function
Apropos this SO answer I tried writing the following Idris 2 function:
import Data.Vect
import Data.Fin
swap : (1 i : Fin (S n)) -> (1 xs : Vect (S n) a) -> Vect (S n) a
swap FZ (x0 :: xs) =...
0
votes
0
answers
42
views
Stream type with monadic effects
Is there a standard type (especially in the stdlib) for a Stream type (by which I mean a potentially infinite, lazy sequence) which allows for effects when accessing the next element? Something like ...
0
votes
0
answers
29
views
Why isn't this variable unknown in the type definition?
import Data.Vect
data NamedVect : Type -> (names : Vect n String) -> Type where
Nil : NamedVect a []
(::) : a -> NamedVect a ss -> NamedVect a (foo :: ss)
aa : NamedVect Nat ["...
0
votes
1
answer
36
views
What are the builddir and outputdir and why are they generating a "File Not Found" error?
The Goal: package an executable "Hello, world" program in Idris2
I'm working from the docs, which gives descriptions of the package fields but sadly doesn't provide any examples.
The issue: &...
0
votes
0
answers
39
views
Prove that `integerToFin` is just
I have the following setup:
data Shape : ( n : Nat ) -> Type where
Nil : Shape Z
(::) : ( k : Nat ) -> { auto prf : IsSucc k } -> ( xs : Shape n ) -> Shape ( S n )
record Tensor ( ...
2
votes
0
answers
125
views
Is there a semigroup/monoid in the context of a monad?
I'm giving my tensor operations a notion of sharing, using a monadic context Shared (implemented as State Nat), so
(+) : Tensor F64 -> Tensor F64 -> Tensor F64
becomes
(+) : Tensor F64 -> ...
0
votes
0
answers
17
views
How can I create a value of type Fin (divCeilNZ n m p)?
I'm experimenting with Idris and I had the idea to create a type that represented a valid reference to a subdivision of an array.
So for example, if the array has a size of 100 and I want my ...
1
vote
3
answers
107
views
How do I write proofs about private implementations?
I want to write a proof about my function
export
foo : Nat -> Nat
but since it's only export not public export, how can I do that? Afaik public makes the implementation public.
0
votes
1
answer
78
views
How does Fin "know" not to go past its type bound?
How does Fin actually work?
data Nat = Z | S Nat
data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
Where does k come from?
Why isn't FZ always the value of (n: Nat)...
0
votes
1
answer
138
views
How do I read all of standard input in Idris2?
I'm trying to figure out how to do something very simple: read all of standard input into a string (or a list of strings would be fine too).
Prelude has getLine : HasIO io => io String, which can ...
2
votes
0
answers
79
views
How should I sum doubles in Idris?
I don't understand why the following does not work:
Main> 2.1 + 2.3
Error: Can't find an implementation for FromDouble Integer.
(Interactive):1:1--1:4
1 | 2.1 + 2.3
^^^
It works with ...
0
votes
1
answer
39
views
Check length of a tuple by pattern matching
I want to learn idris by writing a length function that checks the length of a tuple. I leanred a tuple is made by the MkPair constructor so I try to do pattern matching.
length : {t2:_} -> Pair t1 ...
2
votes
1
answer
164
views
Building a DAG such that nodes are reused
I want to build a DAG, but am unsure how to do it without duplicating effort when evaluating it.
I started with an AST like
data Node =
Lit Double
| Neg Node
| Add Node Node
but traversing ...
0
votes
1
answer
59
views
How many times does a type function run, can you prove?
People say a dependent type language is slow in type checking so I think it is slow in running type functions.
Use the classic example on https://idris2.readthedocs.io/en/latest/tutorial/typesfuns....
1
vote
0
answers
29
views
function with no parameter and the main function?
Book "Type-driven Development with Idris" page 52 has
2.5 Summary ...
Function types have one or more input types and one output type.
The entry point to an Idris program is the main ...
0
votes
1
answer
60
views
Can I print something in the middle of a function?
One example code on https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html says isSingleton returns Nat when the parameter is True, and returns a list when the parameter is False.
isSingleton ...
1
vote
1
answer
62
views
Can we express () in terms of a Record in Idris?
Can we express () i.e Unit type in terms of a Record in Idris ?
2
votes
0
answers
99
views
Idris 2 analog to Agda's `rewrite` that also changes types of bindings in the environment
Suppose I have a theorem
foo : (n : _) -> (f : Fin (n + 0)) -> ...
foo n f = ?goal
and it'd really benefit me if I could use f in contexts where Fin n is expected (and I really mean the precise ...
3
votes
1
answer
124
views
Idris totality check
I am compiling the following simple program using Idris2.
import Data.Fin
%default total
negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin ...
2
votes
1
answer
48
views
How to deal with "Error: Multiple solutions found"?
I'm trying to build a set datatype.
mutual
data Set : Type -> Type where
Nil : Eq a => Set a
(::) : Eq a => (x : a) -> (s : Set a) -> {auto _ : contains x s = False} -> ...
2
votes
1
answer
73
views
How to use interfaces with parameterized tuple?
I have Coord function that transforms an n-dimensional size to the type of coordinates bounded by given size: Coord [2,3] = (Fin 2, Fin 3).
import Data.Fin
import Data.List
Size : Type
Size = List ...
2
votes
1
answer
72
views
How to implement `Show` interface for parameterized tuple?
I have Coord function that transforms an n-dimensional size to the type of coordinates bounded by given size: Coord [2,3] = (Fin 2, Fin 3).
import Data.Fin
import Data.List
Size : Type
Size = List ...
4
votes
1
answer
74
views
Can I avoid lower-case global variables being shadowed in types?
The following code compiles okay in Idris2:
C : Nat
C = 2
claim : C = 2
claim = Refl
but it fails if C is not capitalized:
c : Nat
c = 2
claim : c = 2
claim = Refl
The error message is
Warning: ...
4
votes
1
answer
138
views
The difference between dependent type signatures and proofs
With dependent types, you can either capture function properties in the type signature, like in concatenation with length-indexed lists
(++) : Vect m a -> Vect n a -> Vect (m + n) a
or you can ...
3
votes
2
answers
116
views
What does the 0 or 1 before a parameter name mean in Idris?
I've seen it here and there in Idris source code, but I have yet to find an explanation for what it means. The closest I've gotten is finding that it's called RigCount in the syntax reference. But ...
1
vote
1
answer
71
views
Why does Idris think my type parameter k is of type Type?
Sorry I couldn't think of a less confusing way to put this.
I'm trying to build something like a map that can be safely accessed without returning a maybe, because all of its keys are contained in its ...
2
votes
1
answer
149
views
Expressing the type of variadic functions in Idris
In the book "Type-Driven developement with Idris" the author explains how to create variadic functions. He takes the example of a adder function that consumes a first parameter n: Nat and ...
2
votes
0
answers
62
views
What are the correct C types to use in Idris FFI?
When making an FFI to C from Idris, the following Idris types are allowed
Int
Char
Double (as double in C)
Bits8
Bits16
Bits32
Bits64
String (as char* in C)
Ptr t and AnyPtr (both as void* in C)
...
0
votes
1
answer
64
views
Why does `clockTime` not seem to work for benchmarking, in Idris?
There are probably libraries to do this (although I haven't found any), I'm actually looking to measure the time a function takes to run in Idris. The way I've found is by using clockTime from System ...
1
vote
1
answer
65
views
Recursive function is not total due to with block
I created a function which returns decidable property if the list is an ordered sequence with a step +1.
data Increasing : List Nat -> Type where
IncreasingSingle : Increasing [x]
...
0
votes
1
answer
205
views
Idris2: Nested WITH clause
My Code
My piece of code, i.e.:
equal_suffix: Eq a => List a -> List a -> List a
equal_suffix u v with (snocList u)
equal_suffix _ _ | Empty = []
equal_suffix _ v | (Snoc x xs snx) ...
3
votes
2
answers
160
views
How can i convince Idris that my function is covering?
I wrote a function doSomething that takes an open or closed parenthesis and returns a corresponding Int:
doSomething : (c : Char) -> {auto isPar : c == '(' || c == ')' = True} -> Int
doSomething ...
0
votes
1
answer
65
views
Returning a dependent pair from a foreign function
I have the following Chez support file:
(define list-copy-with-length (xs)
(cons (length xs) (list-copy xs)))
and I have this Idris file:
%foreign "scheme,chez:list-copy-with-length"
...
1
vote
1
answer
159
views
Concept of First-Classed Type in Idris
When learning Idris with Edwin's Type-driven Development with Idris, I read about the unique property of Idris that it's type is a first class construct, compared to other programming languages, and ...
3
votes
2
answers
170
views
Importing from the contrib library fails
I'm following the TDD book in Idris 2, and the online documentation gives the following advice:
For the VList view in the exercise 4 after Chapter 10-2 import Data.List.Views.Extra from contrib ...
3
votes
1
answer
153
views
Types that constrain vectors based on norm
In a language like Haskell or Idris, is it possible to create a data type which checks if an input vector for a function is, for instance, unitary? That is, can I create a data type SumsToOne which ...
2
votes
1
answer
175
views
Why does Idris 2 fail to resolve constraints with function composition in this trivial example?
I have encountered a problem with some code I am trying to write in Idris 2. I would like to resolve this issue, but more importantly, I wish to understand it more deeply and develop some skills in ...