36

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 examples that show off its features (similar to how xmonad is often mentioned as an example of a “real” Haskell program)?

bowsersenior
  • 12,524
  • 2
  • 46
  • 52
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
  • 32
    Hmm, too bad the question got closed, and I don’t think it fits the criteria listed in the explanation. I guess the reason that it does not fit the Q&A format is that it is hard to answer negatively. – Joachim Breitner Aug 28 '12 at 09:22
  • i think there is a web server written in agda, + client code http://ect.bell-labs.com/who/ajeffrey/papers/padl13.pdf – nicolas Oct 11 '15 at 09:33
  • 1
    What do you mean by ' "Real" ' ? I noticed that you put quotations around the word possibly implying that the meaning could be a bit unusual. Are you referring to standalone executables being generated from the language or to I/O programs specifically being defined using the language? If so, search for those properties of programs written in Agda online. There are plenty of those immediately searchable. – Timothy Swan Oct 29 '15 at 04:11
  • “Real” in the sense of that they were written with the intend to solve a real world problem, not with the (primary) intend to play around with Agda per se. Programs, where Agda was but (hopefully useful) tool to achieve a goal. Something along the lines of https://www.joachim-breitner.de/blog/606-Real_World_Haskell_Applications – Joachim Breitner Oct 29 '15 at 08:11

0 Answers0