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

[Thiago Negri]

What I think to be the hard part to do is to put this on the type system, e.g.:

intDiv x y = if y > x then 0 else 1 + (intDiv (x - y) y)

Should not compile. Otherwise you will need the bottom value.

Am I missing something?

Thiago.


2011/12/20 Jesse Schalken <jesseschalken at gmail.com>:
> On Tue, Dec 20, 2011 at 10:43 PM, Gregory Crosswhite <gcrosswhite at gmail.com>
> wrote:
>>
>>
>> On Dec 20, 2011, at 9:18 PM, Jesse Schalken wrote:
>>
>> Why do you have to solve the halting problem?
>>
>>
>> You have to solve the halting problem if you want to replace every place
>> where _|_ could occur with an Error monad (or something similar), because
>> _|_ includes occasions when functions will never terminate.
>
>
> I think we're talking about different things. By "bottom" I mean the
> function explicitly returns "error ..." or "undefined". In those cases, it
> should go in an error monad instead. In cases where there is an infinite
> loop, the function doesn't return anything because it never finishes, and
> indeed this separate problem will never be solved while remaining Turing
> complete because it is the halting problem.
>
>>
>>
>> Consider integer division by 0.  [...]
>> This is all I was talking about.
>>
>>
>> But imagine there was an occasion where you *knew* that the divisor was
>> never zero --- say, because the divisor was constructed to be a natural
>> number.
>
>
> Then use a separate type for natural numbers excluding 0. Then you can
> define a total integer division function on it (although the return value
> may be zero and so needs a different type).
>
>>
>> Now there is no point in running in the Error monad because there will
>> never such a runtime error;  in fact, it is not clear what you would even
>> *do* with a Left value anyway, short of terminating the program and printing
>> and error, which is what would have happened anyway.
>
>
> What you do with a Left value is up to you - that's the point, you now have
> a choice. In fact, the value might not even be being handled by you, in
> which case someone else now has a choice.  Handling of the error is done in
> the same place as handling of the result, no IO needed.
>
>>
>> Furthermore, it is easy to imagine circumstances where you have now forced
>> your entire program to run in the Error monad, which makes everything
>> incredibly inconvenient with no benefit at all.
>
>
> This "inconvenience" I imagine is the extra code required to compose
> functions which return values in a monad as opposed to straight values. To
> me this is a small price to pay for knowing my code won't randomly crash,
> and I would rather this be handled syntactically to make composing monadic
> values more concise.
>
> The point is your program shouldn't be able to make assumptions about values
> without proving them with types. It's often easier not to make the
> assumption and propagate some error in an error monad instead, but that's
> better than getting away with the assumption and having the program crash or
> behave erratically because the assumption turned out false.
>
>> This is the problem with arguments against partial functions;  they don't
>> solve any problems at all except in the case where you have untrusted data
>> in which case you should be using a different function or manually checking
>> it anyway, and they add a lot of wasted overhead.
>
>
> The whole term "untrusted data" baffles me. How often can you actually
> "trust" your data? When you send your software out into the wild, what
> assumptions can you make about its input? What assumptions can you make
> about the input to a small part of a larger program which is millions of
> lines? You can often deduce that certain values do/do not occur in small
> parts of code, but the difficulty of such deductions increases exponentially
> with the size of the codebase, and is a job done much better by a type
> system.
>
> Also I would like to think this "wasted overhead" can be optimised away at
> some stage of compilation, or somehow removed without the programmer needing
> to think about it. Maybe I'm just dreaming on those fronts, however.
>
>> Cheers,
>> Greg
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>