Questions tagged [idris]

Idris is a general purpose pure functional programming language with dependent types.

Filter by
Sorted by
Tagged with
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 ...
wang kai's user avatar
  • 1,725
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)...
Futarimiti's user avatar
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, ...
Henrique Guerra's user avatar
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 ...
Henrique Guerra's user avatar
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 ...
thor's user avatar
  • 21.7k
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 ...
thor's user avatar
  • 21.7k
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 -...
thor's user avatar
  • 21.7k
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 ...
Cactus's user avatar
  • 27.1k
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 ...
Jordan Simba's user avatar
  • 1,096
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: ...
Cactus's user avatar
  • 27.1k
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 $ ...
thor's user avatar
  • 21.7k
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 ...
user avatar
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 ...
thor's user avatar
  • 21.7k
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) =...
Cactus's user avatar
  • 27.1k
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 ...
joel's user avatar
  • 6,738
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 ["...
Gqqnbig's user avatar
  • 5,925
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: &...
Eleanor Holley's user avatar
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 ( ...
Andrew's user avatar
  • 443
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 -> ...
joel's user avatar
  • 6,738
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 ...
Bryan's user avatar
  • 193
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.
joel's user avatar
  • 6,738
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)...
I was in the neighborhood's user avatar
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 ...
Tomas Aschan's user avatar
  • 58.9k
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 ...
lxnv's user avatar
  • 41
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 ...
Gqqnbig's user avatar
  • 5,925
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 ...
joel's user avatar
  • 6,738
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....
Gqqnbig's user avatar
  • 5,925
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 ...
Gqqnbig's user avatar
  • 5,925
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 ...
Gqqnbig's user avatar
  • 5,925
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 ?
Rocky's user avatar
  • 13
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 ...
0xd34df00d's user avatar
  • 1,496
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 ...
haskell looks great's user avatar
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} -> ...
magras's user avatar
  • 1,709
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 ...
magras's user avatar
  • 1,709
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 ...
magras's user avatar
  • 1,709
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: ...
haskell looks great's user avatar
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 ...
joel's user avatar
  • 6,738
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 ...
Aron's user avatar
  • 8,838
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 ...
Aron's user avatar
  • 8,838
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 ...
Contactomorph's user avatar
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) ...
joel's user avatar
  • 6,738
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 ...
Foxy's user avatar
  • 990
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] ...
Stefan Dorn's user avatar
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) ...
Clément Dato's user avatar
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 ...
CifarettoWiggum's user avatar
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" ...
shadowtalker's user avatar
  • 12.9k
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 ...
Clément Dato's user avatar
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 ...
MB-F's user avatar
  • 23k
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 ...
Gotthold's user avatar
  • 133
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 ...
label17's user avatar
  • 153

1
2 3 4 5
16