Stack Overflow
Stack Overflow

Questions tagged [agda]

Agda is a dependently typed, total functional programming language and a proof assistant.

Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program.

Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL.

The current version is 2.6.1.1

Useful links

819 questions
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
87
votes
2 answers

What is the combinatory logic equivalent of intuitionistic type theory?

I recently completed a university course which featured Haskell and Agda (a dependent typed functional programming language), and was wondering if it was possible to replace lambda calculus in these with combinatory logic. With Haskell this seems…
grasevski
  • 2,894
  • 2
  • 21
  • 22
80
votes
1 answer

Why is my definition not allowed because of strict positivity?

I have the following two definitions that result in two different error messages. The first definition is declined because of strict positivity and the second one because of a universe inconsistency. (* non-strictly positive *) Inductive SwitchNSP…
ichistmeinname
  • 1,480
  • 10
  • 19
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
50
votes
1 answer

How to use Agda's auto proof search effectively?

When writing proofs I noticed that Agda's auto proof search frequently wouldn't find solutions that seem obvious to me. Unfortunately coming up with a small example, that illustrates the problem seems to be hard, so I try to describe the most common…
Helmut Grohne
  • 6,578
  • 2
  • 31
  • 67
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

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
43
votes
1 answer

What is Axiom K?

I've noticed the discussion of "Axiom K" comes up more often since HoTT. I believe it's related to pattern matching. I'm surprised that I cannot find a reference in TAPL, ATTAPL or PFPL. What is Axiom K? Is it used for ML-style pattern matching as…
Steven Shaw
  • 6,063
  • 3
  • 33
  • 44
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
37
votes
1 answer

Why do we need containers?

(As an excuse: the title mimics the title of Why do we need monads?) There are containers [1] (and indexed ones [2]) (and hasochistic ones [3]) and descriptions.[4] But containers are problematic [5] and to my very small experience it's harder to…
effectfully
  • 12,325
  • 2
  • 17
  • 40
36
votes
2 answers

Do Hask or Agda have equalisers?

I was somewhat undecided as to whether this was a math.SE question or an SO one, but I suspect that mathematicians in general are fairly unlikely to know or care much about this category in particular, whereas Haskell programmers might well do. So,…
Ben Millwood
  • 6,754
  • 24
  • 45
36
votes
0 answers

Are there examples Agda code running in production?

Agda is a nice programming language to explore dependent types and play around with intuitionistic type theory and to experiment with the implementation of these things. But are there already examples for “real” programs written in Agda? Maybe even…
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
33
votes
1 answer

Differences between Coq and Agda

What are each of these programs designed for and what does each offer other the other? Also, are both systems consistent, and moreover, are they based on some foundational mathematical theory? Two things I care about: Easy to install Easy to…
Cristian Garcia
  • 9,630
  • 6
  • 54
  • 75
1
2 3
…
54 55