On Thu, 11 Jun 2009, David Menendez wrote:
I'd ask why system is indicating failure through an exit code instead of throwing an exception.
Yes, throwing exception would also be nice. However current Haskell IO system hides the possibility of exceptions and does not tell, which exceptions may occur. To this end, various monads were developed (transformers,mtl:Control.Monad.Error, explicit-exception:Control.Monad.Exception.Synchronous, control-monad-exception). Of course, under the hood they use return values.
It's quite easy to add 'ignore' where necessary and it safes us from ignoring a result by accident. Avoiding errors is the goal of using types, isn't it?
If that's all there is to it, then why aren't you using Agda or Coq?
I assumed, Haskell shall also be developed towards dependent types, which are intended for more safety, aren't they? Nonetheless, I find Agda an interesting project.