[Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

[Ben Lippmeier]

On 20/12/2011, at 21:52 , Gregory Crosswhite wrote:
> 
>> Some would say that non-termination is a computational effect, and I can argue either way depending on the day of the week.
> 
> *shrug*  I figure that whether you call _|_ a value is like whether you accept the Axiom of Choice:  it is a situational decision that depends on what you are trying to learn more about.

I agree, but I'd like to have more control over my situation. Right now we have boxed and lifted Int, and unboxed and unlifted Int#, but not the boxed and unlifted version, which IMO is usually what you want.


>> Of course, the history books show that monads were invented *after* it was decided that Haskell would be a lazy language. Talk about selection bias.
> 
> True, but I am not quite sure how that is relevant to _|_...

I meant to address the implicit question "why doesn't Haskell use monads to describe non-termination already". The answer isn't necessarily "because it's not a good idea", it's because "that wasn't an option at the time".


> Dec 20, 2011, в 14:40, Jesse Schalken <jesseschalken at gmail.com> написал(а):


>> Including all possible manifestations of infinite loops?
> 
> So... this imaginary language of yours would be able to solve the halting problem?

All type systems are incomplete. The idea is to do a termination analysis, and if the program can not be proved to terminate, then it is marked as "possibly non-terminating". This isn't the same as deciding something is "*definitely* non-terminating", which is what the halting problem is about. This "possibly non-terminating" approach is already used by Coq, Agda and other languages.

Ben.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111220/1f307744/attachment.htm>