Unlifted values are not consumed linearly

[andrewthad]

The proposal indicates that any pattern match on a value of type Int#, Char#, etc. should be considered linear consumption. Presumably, this would include wildcard matches with an underscore as well. So, this should typecheck:

foo :: Int ->. Bool
foo (I# _) = True

This doesn't currently work, and it causes me to reach for unsafeCoerce more than I otherwise would. It would be nice if the wrappers over also had the same (or similar behavior). This would let me simplify the above example to:

foo :: Int ->. Bool
foo !_ = True

I think the bang pattern is important here. Without it, we don't force the primitive Int# value.

[andrewthad]

Very closely related is that this doesn't work:

bar :: (a,Int) ->. Foo a
bar (x,1) = ...
bar (x,2) = ...
bar (x,_) = ...

[aspiwack]

Well, they linear semantically (though in the case of Int, it's a bit subtle). I'm not sure that we want to teach the type checker that they are (type checking is always an over-approximation of the semantic property). Is it worth the complication?

Probably, the simplest path is to make I# unrestricted in its field. For more advanced type checking features, I'd rather wait until the dust has settled.

[aspiwack]

Oh, and you are right about the !_ for Int, it is only linear with !_.

[andrewthad]

Ah, I had not considered that I# could simply be unrestricted in its field. That certainly alleviates some of the pain I am experienced. It also convinces me that having special rules for Int is unnecessary. But I still kind of want something special for Int#, Addr#, etc (but not the unlifted types Array#, MutableArray#, etc. since there's no way the type checker could enforce what is suggested in the proposal). I'll elaborate. Consider this primop:

readIntOffAddr# :: Addr# -> Int# -> State# s -> (# State# s, Int# #)
writeIntOffAddr# :: Addr# -> Int# -> Int# -> State# s -> State# s

It reads an Int at a given offset from an address. Right now, I can use unsafeCoerce to build a kind of linear pointer of top of this:

-- Here, we redefine Ptr and Int as you suggested above to be linear in their arguments.
data Ptr a where
  Ptr :: Addr# -> Ptr a

data Int where
  I# :: Int# -> Int

-- This is a pointer equipped with a state token
data Ref a where
  Ref :: !(Ptr a) -> State# RealWorld ->. Ref a

readIntRef :: Ref Int ->. (Ref Int, Int)
readIntRef = unsafeCoerce ...

writeIntRef :: Ref Int ->. Int -> Ref Int
writeIntRef = unsafeCoerce ...

Right now, I have to use unsafeCoerce manipulate linearity to write readIntRef and writeIntRef, and I don't like having to use it. What would get me half-way there was if readIntOffAddr# and writeIntOffAddr# were defined to be linear in their state tokens:

readIntOffAddr# :: Addr# -> Int# -> State# s ->. (# State# s, Int# #)
writeIntOffAddr# :: Addr# -> Int# -> Int# -> State# s ->. State# s

Now, writeIntRef can be written without unsafeCoerce. Sadly, readIntRef is still needs unsafeCoerce since we aren't going to consume the Int# in the returned tuple linearly. One solution would be treating Int# and friends specially concerning consumption. But as you point out, that complicates the implementation, and the payout isn't huge, so it's probably not worth it. Another solution would be to have readIntOffAddr# return a mixed-multiplicity unboxed record, but this might break existing uses of the function (I'm not totally sure since I don't really understand how these work). But there might be another way. What if we had a primop like this:

unrestrictInt# :: Int# ->. Mult# 'Omega Int#

This is zero-cost. And now we could write readIntRef without unsafeCoerce:

readIntRef :: Ref Int ->. (Ref Int, Int)
readIntRef (Ref (Ptr addr) s0) = case readIntOffAddr addr 0# s0 of
  (# s1, r #) -> case unrestrictInt r of
    Mult# v -> (Ref (Ptr addr) s1, I# v)

So maybe what I want is not a more sophisticated type checker but a primop to side-step the issue.

[aspiwack]

Well, yes unrestrictedInt# (I'd probably call it moveInt# to be in line with the Movable type class from linear-base) should be implemented. That is certainly going to happen fairly soon. (we need something like Mult#, which doesn't yet have an equivalent in Core, though, so it's not as trivial as it may first sound)

Another related point is that functions like readIntOffAddr# should have return types of a form similar to (# State# s, Mult# p a #), so that when linearity of the returned value is not required, we can return an unrestricted one directly.

[andrewthad]

While changing the type of readIntOffAddr# to use Mult# would certainly help me, it would break all existing consumers of the API. But, perhaps a new primop (something like readMultIntOffAddr#) could be introduced in GHC.Prim, and then the old readIntOffAddr# could be implemented in GHC.Exts instead as:

readIntOffAddr# :: Addr# -> Int# -> State# s -> (# State# s, Int# #)
readIntOffAddr# addr off s0 = case readMultIntOffAddr# addr off s0 of
  (# s1, Mult v #) -> (# s1, v #)

Also, I'm glad to hear about moveInt#. This will be helpful for me.

[andrewthad]

Is there currently some kind of magic trick I can use to subvert the linearity checker in certain cases? (Even if it's a bug). The way I currently use unsafeCoerce to accomplish this prevents GHC from doing case-of-known-data-constructor analysis, so my code does a bunch of allocations that won't be there once we have Mult# and the moveX# primops. But, for the time being, it would be nice to be able to inspect the core and look for bad allocations. I guess I'm looking for something like this:

data Bar = Bar where { Bar :: Addr# -> Bar }

foo :: Addr# ->. Bar
foo x = Bar (uncheckedLinearity# x)

Where uncheckedLinearity# is some kind of magic function that doesn't get type-checked like normal. I doubt there's anything like this, but I just wanted to check in case it's there.

[aspiwack]

There isn't yet, I'm afraid. linear-base defines the linearity casting function as unsafeCoerce unsafeCoerce (because unsafeCoerce itself is not linear, but this is something which we can quite possibly change), see the Unsafe module. I don't know whether Core knows to eliminate trivial unsafeCoerces when they show up. But, at any rate, some coercion pushing is blocked by coercions on arrow multiplicities. This is something that can be imrpoved, but not eliminated until we have a good notion in Core of usage-coercions. This is in the back of my mind. But I'm busy these days pushing an MVP which won't have this.

[andrewthad]

No problem. Once moveX# and Mult# are implemented, I won't really need unsafeCoerce for anything. I was just looking for a quick workaround for the time being.