crash on 1L / 0

[adam-antonik]

Most divide by zero operations produce the largest value of the resulting type. However, 1L / 0 crashes with

Floating point exception (core dumped)

[kthielen]

Maybe it would be better to exclude this case in the type system too, though it bothers people to be obliged to prove that a value is non-zero.

Anyway, I'm not sure that defining this result to be a particular value is the right thing to do (especially if it means additional overhead for the typical case). I'm inclined to leave it, or plan to exclude it with a suitable type.

[adam-antonik]

My confusion is that it seems like that it should be handled by the type-class in boot/arith.hob How is it that we can divide 1L (or 1H) by (0 :: int)? Surely we must go through the Divide type-class, and for those that have different types, then we can only divide if we can convert one to the other. But 1 / 0 or (convert(1L) :: int) / 0 1L / 0L or 1L / (convert(0) :: long) both work. So the type-class lookup should mean that this does not crash.

[kthielen]

1 / 0 or (convert(1L) :: int) / 0 1L / 0L or 1L / (convert(0) :: long) both work. So the type-class lookup should mean that this does not crash.

There's a small difference. The expressions you're providing can be immediately rewritten, and then consist only of constant data so that the back-end (LLVM) will immediately evaluate them (and it decides to define this undefined behavior in a different way than the hardware does when the evaluation happens later).

One easy way to see this is with the "unsweeten transform" at the shell:

$ hi -s
> :u 1L / (convert(0)::long)
(ldiv::(long * long) -> long)(1L:long, (i2l:(int) -> long)(0:int):long):long

Here you can see that the expression has been rewritten as overloaded terms are resolved. So "ldiv" is the low-level function for 64-bit division (maps exactly to CreateSDiv at the back-end), and "i2l" is the low-level function for signed 32-bit to 64-bit widening (maps to another primitive instruction). So you see how we get to this state where LLVM sees that it has enough information to simplify by immediate evaluation.

OTOH, for the expression that you started with:

$ hi -s
> :u 1L / 0
(.rfn.t4137:(long * int) -> long)(1L:long, 0:int):long

In this case, this obscure function name .rfn.t4137 is produced by the rewriting as an instance of Divide at your type instantiation is requested (normally people don't poke around at this level, but you can see this association at the shell with : i Divide which will show you all of the instances, including instance Divide long int long where / = .rfn.t4137::(long * int) -> long.

This function call stays in the residual program and so you get the behavior at runtime that you observed (since that's how the machine does it).

But this is just an explanation of what happened in terms of the low level implementation of everything. Maybe the better answer is that it's undefined behavior in general, so should be avoided (and ideally excluded within the type system to prevent the issue altogether).