[Haskell-cafe] agda v. haskell

[Dan Doel]

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