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