Stack Overflow
Stack Overflow

Questions tagged [idris]

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

Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker.

Useful links:

785 questions
202
votes
3 answers

What is an appropriate type for smart contracts?

I'm wondering what is the best way to express smart contracts in typed languages such as Haskell or Idris (so you could, for example, compile it to run on the Ethereum network). My main concern is: what is the type that captures everything that a…
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
190
votes
2 answers

Differences between Agda and Idris

I'm starting to dive into dependently-typed programming and have found that the Agda and Idris languages are the closest to Haskell, so I started there. My question is: which are the main differences between them? Are the type systems equally…
serras
  • 2,165
  • 2
  • 13
  • 11
84
votes
1 answer

"Monad transformers more powerful than effects" - Examples?

The paper "Programming and reasoning with algebraic effects and dependent types" by Edwin C. Brady on effects in Idris contains the (unreferenced) claim that: Although [effects and monad transformers] are not equivalent in power — monads and monad…
geoff_h
  • 1,245
  • 8
  • 13
50
votes
3 answers

Why is typecase a bad thing?

Both Agda and Idris effectively prohibit pattern matching on values of type Type. It seems that Agda always matches on the first case, while Idris just throws an error. So, why is typecase a bad thing? Does it break consistency? I haven't been able…
András Kovács
  • 29,931
  • 3
  • 53
  • 99
48
votes
7 answers

Dependent types can prove your code is correct up to a specification. But how do you prove the specification is correct?

Dependent types are often advertised as a way to enable you to assert that a program is correct up to a specification. So, for example, you are asked to write a code that sorts a list - you are able to prove that code is correct by encoding the…
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
45
votes
2 answers

How do we overcome the compile time and runtime gap when programming in a Dependently Typed Language?

I'm told that in dependent type system, "types" and "values" is mixed, and we can treat both of them as "terms" instead. But there is something I can't understand: in a strongly typed programming language without Dependent Type (like Haskell), Types…
luochen1990
  • 3,689
  • 1
  • 22
  • 37
44
votes
2 answers

Practical examples of Idris

Are there any examples of Idris that might be used to study and perhaps apply it for general purpose/"real world" application? I am moderately proficient in Haskell, of which Idris seems to borrow significantly, and the official FAQ/documentation is…
Arets Paeglis
  • 3,856
  • 4
  • 35
  • 44
44
votes
2 answers

Where to start with dependent type programming?

There is an Idris tutorial, an Agda tutorial and many other tutorial style papers and introductory material with never ending references to things yet to learn. I'm kind of crawling in the middle of all these and most of the time I'm stuck with…
Ashkan Kh. Nazary
  • 21,844
  • 13
  • 44
  • 68
41
votes
6 answers

Dependent Types: How is the dependent pair type analogous to a disjoint union?

I've been studying dependent types and I understand the following: Why universal quantification is represented as a dependent function type. ∀(x:A).B(x) means “for all x of type A there is a value of type B(x)”. Hence it's represented as a function…
Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
41
votes
2 answers

Difference between type parameters and indices?

I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is parameterized by another type and indexed by some value. But isn't there no distinction between types and terms in a dependently…
Alex
  • 1,184
  • 7
  • 15
33
votes
2 answers

Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes

So in Idris it's perfectly valid to write the following. item : (b : Bool) -> if b then Nat else List Nat item True = 42 item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A Without the type signature, this looks like a…
ruben.moor
  • 1,876
  • 15
  • 27
33
votes
1 answer

Doing rank-n quantification in Idris

I can only do rank-n types in Idris 0.9.12 in a rather clumsy way: tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b) tupleId f (a, b) = (f _ a, f _ b) I need the underscores wherever there's a type application, because Idris throws parse errors…
András Kovács
  • 29,931
  • 3
  • 53
  • 99
31
votes
3 answers

Are Lists Inductive or Coinductive in Haskell?

So I've been reading about coinduction a bit lately, and now I'm wondering: are Haskell lists inductive or coinductive? I've also heard that Haskell doesn't distinguish the two, but if so, how do they do so formally? Lists are defined inductively,…
Crazycolorz5
  • 747
  • 6
  • 12
31
votes
1 answer

Idris eager evaluation

In Haskell, I might implement if like this: if' True x y = x if' False x y = y spin 0 = () spin n = spin (n - 1) This behaves how I expect: haskell> if' True (spin 1000000) () -- takes a moment haskell> if' False (spin 1000000) () --…
Snowball
  • 11,102
  • 3
  • 34
  • 51
28
votes
2 answers

Why haven't newer dependently typed languages adopted SSReflect's approach?

There are two conventions I've found in Coq's SSReflect extension that seem particularly useful but which I haven't seen widely adopted in newer dependently-typed languages (Lean, Agda, Idris). Firstly, where possible predicates are expressed as…
LogicChains
  • 4,332
  • 2
  • 18
  • 27
1
2 3
…
52 53