`Integer` is not `Additive`

[andreasabel]

(Sorry, newbie here.) Trying to add Integers I am getting error:

No instance for (Additive Integer) arising from a use of ‘+’

Is there a deeper reason for this or is it just not implemented?

[aspiwack]

I'm not too sure how to handle Integer linearly, to be honest. It's quite possibly out of ignorance: I don't know how Integer is implemented.

What we have to consider is that for (+) to be linear on Integer, it needs to guarantee that it evaluates every thunk (or pass them into the resulting integer without dropping or duplicating any). It's quite obvious for Int and friends, which have a single thunk which is necessarily forced. But for Integer, I don't know.

[treeowl]

Why would every thunk have to be forced? Can't a non-linear implementation expose a linear interface? That said, Integer is completely strict internally, so there's nothing to worry about.

[aspiwack]

Why would every thunk have to be forced?

Every linear argument has to be consumed exactly once. This is the contract. A thunk, in a linear argument, can point to linear arguments which haven't been consumed yet (in which case, forcing the thunk will, transitively, consume the linear arguments it points to). So you really need to (ultimately force all the thunks exactly once. Otherwise you would break the contract with these arguments that you've closed over.

[treeowl]

I don't think your reasoning is entirely valid.

First, not all thunks are "exposed". If Integer were implemented using a data structure with thunks, that would have no impact on its semantics, which are designed and documented to be strict. There are quite a few data structures of that sort—see Okasaki in particular, but also Hinze and Paterson. No one can hang extras off those thunks, so their existence is irrelevant.

Second, you actually can't know for sure how many times a thunk will be forced, short of an expensive operation. GHC's "lazy blackholing" mechanism reserves the right to evaluate the same thunk twice in multiple threads, unless that thunk uses noDuplicate# to prevent it. This should only be done when truly necessary, as it is very definitely not free.

Third, while a linear argument can only be consumed once, it does not inherently have to be inspected only once. Yes, we would write

foo :: Maybe Bar %1-> (Maybe Bar, Bool)
foo Nothing = (Nothing, False)
foo (Just x) = (Just x, True)

But another valid implementation is

foo = toLinear (\m -> let !b = isJust m in (m, b))

[aspiwack]

First, not all thunks are "exposed". If Integer were implemented using a data structure with thunks, that would have no impact on its semantics, which are designed and documented to be strict.

Well, true, it's possible that thunks only contain internal computations to the data structure, in which case we may get away with not evaluating them. It does require some pretty careful reasoning if we are to unsafely cast from unrestricted to linear in this case.

Note that a linear type system can't know this sort of thing on its own: if it sees a linear thunk, it will force you to evaluate it (I'm pretty sure most of Okasaki's data structures could be typed linearly by the way). So if you want to skip on some thunks because you have some special knowledge about them, then you have to use unsafe code.

Second, you actually can't know for sure how many times a thunk will be forced, short of an expensive operation. GHC's "lazy blackholing" mechanism reserves the right to evaluate the same thunk twice in multiple threads, unless that thunk uses noDuplicate# to prevent it. This should only be done when truly necessary, as it is very definitely not free.

This is not a problem, because linear typing prevents multiple threads from holding a reference to a linear value (alternatively, we could say that this is the reason why linear typing must prevent multiple threads from holding a reference to a linear value).

Third, while a linear argument can only be consumed once, it does not inherently have to be inspected only once. Yes, we would write

foo :: Maybe Bar %1-> (Maybe Bar, Bool)
foo Nothing = (Nothing, False)
foo (Just x) = (Just x, True)

But another valid implementation is

foo = toLinear (\m -> let !b = isJust m in (m, b))

Indeed (though I think it's unrelated to the previous discussion). This doesn't typecheck today, but it could. I think of it as teaching the typechecker about call-by-need (the second implementation would not be linear in a call-by-name language). I don't quite know how to go about it. @andreasabel once suggested using a 0 multiplicity for something like this: isJust would have type Maybe a %0 -> Bool, at the time I wasn't very enthusiastic, I thought it would break a lot of things; I've warmed up to the idea since.

[andreasabel]

@andreasabel once suggested using a 0 multiplicity for something like this: isJust would have type Maybe a %0 -> Bool

Er, this isn't how %0 works in Agda (or Idris or Quantitative Type Theory), because %0 arguments cannot be inspected in ordinary situations, only in %0 contexts. The meaning of %0 in Agda is that it can be erased by the compiler.

[aspiwack]

Indeed, and it was my thought as well, originally. But I now think that uniform quantification and 0-multiplicity 𝛱-types actually ought to be different. For one thing, they have different polarities (uniform quantification is best modeled as being positive, whereas a 𝛱-type is negative). I think that there is a real mismatch there, and that the allure of the simple explanation (0 means erasable) led us astray.

The issue is magnified by the case_p rule whereby we can make a case expression which consumes p times its scrutinee, (and scales the multiplicity of the fields by p). This construction is not part of the original linear logic, but it is in Idris, Linear Haskell, and Granule (I don't know about Agda). If we want 0 to mean erasable, then we can't have a case_0 (case_0 lets us implement isJust which can't be implemented on an erased parameter). Then 0 becomes really weird, almost every multiplicity-polymorphic function must be prefixed by NotZero p =>. This is not great.

I think that 0 as: I've touched it but it's still fully available, albeit being something incompatible with call-by-name, has merit. I don't know that it's the right approach, just a plausible one.

[andreasabel]

@oskeri, have a look at Arnaud's comment.

[YellowOnion]

Hey as a causal observer, I'm curious if this was ever solved?

I'm somewhat dubious about the initial claims that it could contain such issues around thunks, There was a bit of drama a while back around the use of a GMP LGPL library internally, which made statically linked Haskell an issue.

my first thought is why would they complicate such a simple library with more than one thunk? how would you handle carry etc, Especially for performance reasons.

So anyway I looked it up, and it looks like the new reference replacement uses a strict Int or a strict ByteArray internally: https://hackage.haskell.org/package/ghc-bignum-1.3/docs/src/GHC.Num.Integer.html#Integer https://hackage.haskell.org/package/ghc-bignum-1.3/docs/src/GHC.Num.WordArray.html#WordArray%23

There's also the gmp and a "native" version in there too.

Hope that helps.

[aspiwack]

@YellowOnion sorry I'd missed your comment until now. Thank you.

If this is the implementation of Integer, then indeed the operations are going to be linear. I assume that the GMP-based implementation is going to be just as safe. I think we can go ahead an provide instances for Integer.