dons has been posting some links regarding agda on reddit. fairly interesting, a quick glance and you think you are reading haskell code. does anyone have any insights on the major differences in these languages?
On Friday 28 September 2007, brad clawsie wrote:
dons has been posting some links regarding agda on reddit. fairly interesting, a quick glance and you think you are reading haskell code.
does anyone have any insights on the major differences in these languages?
I'm not too familiar with Agda, but I believe it's one of the dependently typed functional languages/theorem provers that more and more people are growing interested in these days. If you want to know what all that sort of hype is about, you might want to read Why Dependent Types Matter [1] by the Epigram folks, which does a pretty good job explaining what you might want them for. Or, if you want an even shorter explanation, imagine the sort of type-system programming that Oleg does, and then imagine languages that attempt to make that sort of thing as easy as the ordinary programming you do (or, get it closer to there, at least). -- Dan [1]: http://e-pig.org/downloads/ydtm.pdf
Hello, Agda is essentially an implementation of a type checker for Martin-Lof type theory (i.e. dependent types). It is designed to be used as a proof assistant. Roughly speaking propositions are represented as types and a proof of a proposition is a well-typed, total and terminating function. Agda has machinery to help you fill in cases and generally make proof construction easier. Agda is different from Haskell in that Agda has dependent types and machinery for interactively constructing the definition of a function at a given type. Agda is also different from Haskell in that the focus is on the user interface and writing the proof/program itself, rather than on executing the resulting code (i.e. little work has gone into compiling Agda code). I think there have been several projects scattered around on generating Haskell from Agda and on importing Haskell code into Agda for formal verification. -Jeff haskell-cafe-bounces@haskell.org wrote on 09/28/2007 11:41:41 AM:
dons has been posting some links regarding agda on reddit. fairly interesting, a quick glance and you think you are reading haskell code.
does anyone have any insights on the major differences in these languages?
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
--- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.
On Fri, 28 Sep 2007, Jeff Polakow
Agda is essentially an implementation of a type checker for Martin-Lof type theory (i.e. dependent types).
It is designed to be used as a proof assistant.
Well, the language aims to become a practical programming language. Ulf's recently defended PhD thesis has the title "Towards a practical programming language based on dependent type theory" (http://www.cs.chalmers.se/~ulfn/papers/thesis.html). Lots of work remains to be done before this goal is reached, though. In the meantime, Agda is an excellent vehicle for experiments in dependently typed programming with inductive families (≈ GADTs). For more information, see the Agda wiki (http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php). -- /NAD
participants (4)
-
brad clawsie -
Dan Doel -
Jeff Polakow -
Nils Anders Danielsson