On 12/4/06, Nils Anders Danielsson wrote:

If "laws not satisfied => any behaviour OK" were the correct interpretation, then it would be OK for the Array implementation to wipe all your files at the first encounter of a broken Ix law... ;)

Yeah, but that would just be asking for it to happen to *you*! Besides, it is too much work!

On 12/5/06, Simon Marlow wrote:

Nils Anders Danielsson wrote:

...

On Mon, 04 Dec 2006, Simon Marlow wrote:

...

An implementation is entitlesd to assume the following laws about these operations:

range (l,u) !! index (l,u) i == i -- when i is in scope inRange (l,u) i == i `elem` range (l,u) map index (range (l,u)) == [0..rangeSize (l,u)]

Even if these laws are not satisfied, is the implementation really allowed to segfault? I would have guessed that the array operations should still be equivalent to some pure Haskell program (e.g. undefined).

To me, the wording "An implementation is entitled to assume..." implies that there are no obligations on the implementation should the assumption not hold - no obligation to yield _|_ or any other behaviour.

...

If "laws not satisfied => any behaviour OK" were the correct interpretation, then it would be OK for the Array implementation to wipe all your files at the first encounter of a broken Ix law... ;)

Yup. That's not quite as bad as in C, where it's ok for an implementation to wipe all your files if you overflow the int type...

Cheers, Simon

Still, this is pretty bad, and raises questions about the safety of Haskell programs in general. It seems unsatisfactory that if a programmer makes a mistake in the definition of an 'Ix' instance, then there are no guarantees about the behavior of their program at all... I though that implementations did not assume anything about the user-specified instances. Are there other classes for which GHC assumes something about the instances? If so this should be documented in bold letters with lots of flashing red lights :-) -Iavor

Simon Peyton-Jones wrote:

...

...

To me, the wording "An implementation is entitled to assume..." implies that there are no obligations on the implementation should the assumption not hold - no obligation to yield _|_ or any other behaviour.

...

If "laws not satisfied => any behaviour OK" were the correct interpretation, then it would be OK for the Array implementation to wipe all your files at the first encounter of a broken Ix law... ;)

Yup. That's not quite as bad as in C, where it's ok for an implementation to wipe all your files if you overflow the int type...

Cheers, Simon

Still, this is pretty bad, and raises questions about the safety of Haskell programs in general. It seems unsatisfactory that if a programmer makes a mistake in the definition of an 'Ix' instance, then there are no guarantees about the behavior of their program at all...

I rather agree with Iavor here. If a program makes no use of unsafeX functions, and has no foreign calls, and passes the typechecker, then it should not crash.

Yes, I agree too! I'm just pointing out that the problem is already in the Haskell 98 specification, which we follow. If possible we should fix this in Haskell'.

However, I don't see how to achieve this for array indexing, without adding another test to every array access.

If (!) was changed to be a method of IArray, then for certain arrays we could use unsafeIndex instead of index, and check the index against the physical array size instead. Eg. (!) is currently defined as arr ! i = case bounds arr of (l,u) -> unsafeAt arr (index (l,u) i) This would be the default method for (!), but for some arrays we could replace it by arr ! i = case bounds arr of (l,u) -> safeAt (unsafeIndex (l,u) i) Where safeAt is implemented by looking at the physical array size. One slight problem is that the size stored in GHC's byte arrays is rounded up to the nearest word. Also we don't have a sizeOfArray# primitive, as Spencer pointed out in the original post in the thread. Similar changes would be required in the MArray class too: readArray/writeArray would need to become methods. Cheers, Simon

On 12/6/06, Iavor Diatchki wrote:

Hello,

another option (perhaps too draconian?) would be to disallow user-defined instances for Ix, and to ensure that the predefined instances satisfy the required laws. We can do this in one of the following ways: * Do not export 'Ix': not good because we cannot write type signatures * Export 'Ix' but not its methods: ensures that programmers can define only trivial (i.e. undefined) instances. * Add a super class to 'Ix' (e.g., 'PrivateIx') which is not exported. This would disallow user-defined instances because they can never satisfy the 'PrivateIx' constraint.

We could put one of these things in e.g. Data.Ix.IAmNotAnIdiot, so that users can define instances of Ix if they need to, but not without being warned that this might be dangerous, and that it is usually possible to just use derived one. (Such warnings would appear in the documentation of this module.)

On Tue, 05 Dec 2006, Simon Marlow wrote:

To me, the wording "An implementation is entitled to assume..." implies that there are no obligations on the implementation should the assumption not hold - no obligation to yield _|_ or any other behaviour.

I guess that's a valid interpretation. As an aside, it is interesting to note that the Ix instance for Integer does not satisfy the first law (if a wraparound semantics is used for Int; this is allowed by the report). With l = 0, u = toInteger (maxBound :: Int) + 1 and i = u we have inRange (l,u) i = True but range (l,u) !! index (l,u) i = ⊥ ≠ i. Furthermore, more seriously, the third law isn't type correct, and a corrected version, map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u)], isn't satisfied by the Ix instance for Int, since (with b = (0, 0 :: Int)) map (index b) (range b) = [0] while [0..rangeSize b] = [0, 1]. I think the law should really be map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u) - 1]. This law is also prone to overflow errors, by the way. -- /NAD

On Wed, 06 Dec 2006, "Samuel Bronson" wrote:

But, will you ever encounter such overflows in using an array? I suppose you might if you tried to make one larger than the address space...

Are you assuming that Ints can always be used to address the entire address space? Ints are only guaranteed to have 30 bits. -- /NAD

Nils Anders Danielsson wrote:

On Tue, 05 Dec 2006, Simon Marlow wrote:

...

To me, the wording "An implementation is entitled to assume..." implies that there are no obligations on the implementation should the assumption not hold - no obligation to yield _|_ or any other behaviour.

I guess that's a valid interpretation.

As an aside, it is interesting to note that the Ix instance for Integer does not satisfy the first law (if a wraparound semantics is used for Int; this is allowed by the report). With l = 0, u = toInteger (maxBound :: Int) + 1 and i = u we have inRange (l,u) i = True but range (l,u) !! index (l,u) i = ⊥ ≠ i.

Furthermore, more seriously, the third law isn't type correct, and a corrected version,

map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u)],

isn't satisfied by the Ix instance for Int, since (with b = (0, 0 :: Int)) map (index b) (range b) = [0] while [0..rangeSize b] = [0, 1]. I think the law should really be

map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u) - 1].

This law is also prone to overflow errors, by the way.

Thanks Nils, I'll make sure these points get addressed during the Haskell' process. Cheers, Simon