Multiplicity subtyping with dependent types can break linearity

[edwinb]

Issue by KyleDavidE
Friday May 08, 2020 at 15:07 GMT
Originally opened as edwinb/Idris2-boot#357

---

Steps to Reproduce

badEq : ((x: Nat) -> Nat) = ((1 x:Nat) -> Nat)
badEq = Refl

Expected Behavior

The term should not typecheck because this can be used to cast (x: Nat) -> Nat to (1 x:Nat) -> Nat, this sort of trick could easily be used to make "safe" terms of type IO ((0 x: Type) -> IO x -> x) which could grotesquely break things.

Observed Behavior

It type checks, though it is of note that

1. If you reverse the order in the type definition, (i.e. badEq : ( (1 x:Nat) -> Nat ) = ( (x: Nat) -> Nat)) it does not type check
2. This doesn't work with erased arguments

[edwinb]

Comment by edwinb
Saturday May 09, 2020 at 12:07 GMT

---

Hmm, this is a bit awkward. The subtyping rules are to allow you to pass linear functions to HOFs which don't have linearity constraints (but not vice-versa). But this suggests the rules are too liberal.

There's no subtyping rules between 0-multiplicity things and others, so I don't think this can cause erased things to be needed at run time, but if you can use it to pass non-linear functions in a context that requires linearity, that would be bad.

[edwinb]

Comment by KyleDavidE
Friday May 15, 2020 at 20:43 GMT

---

It seems to me that the linearity rules subtyping should only lift over (dependent) function types. In an ideal world it would also lift over positive functors, but I have no idea if that is possible.

The haskell-y way to solve this problem would be linearity polymorphism rather than subtyping but I can't imagine terms with linearity polymorphism would be pleasant to reason about.

[edwinb]

I've been trying to use this to break linearity for something concrete, but with no success. I thought sym badEq might help, but you get...

Main> :t sym badEq
sym badEq : Nat -> Nat = Nat -> Nat

...which is quite safe. The reason you get that is that, thanks to the subtyping rule, the explicit definition of badEq is Refl {x = Nat -> Nat}. So I think what it's proving is that it's safe to use a linear function where a generic multiplicity is expected, but not vice versa, which is fine.

[KyleDavidE]

The behavior you are seeing with sym only seems to be happening as a weird product of type inference, here is a fully worked example creating a IO action that produces the unsafePreformIO primitive

note that the explicit arguments on transport' are required.

This same approach could be used to make a cloner for any type.

public export
data UWorld : Type where
    MkUWorld : %World -> UWorld


public export useUnlimitedWorld : (1 u: UWorld) -> IORes %World
useUnlimitedWorld (MkUWorld a) = MkIORes a a


WorldCloner : Type
WorldCloner =  (1 x: %World) -> UWorld

ConstructorType : Type
ConstructorType = ( (x: %World) -> UWorld )

badEq : ConstructorType = WorldCloner
badEq = Refl

transport' : (a : Type) -> (b: Type) -> a = b -> a -> b
transport' a a Refl x = x

worldCloner : WorldCloner
worldCloner = transport' ConstructorType WorldCloner badEq MkUWorld

extractWorld : IO %World
extractWorld = fromPrim (\x => useUnlimitedWorld (worldCloner x))

makeUnsafeIoHelper : %World -> (x: Type) -> IO x -> x
makeUnsafeIoHelper w x action = case (toPrim action w) of
                                        (MkIORes x _) => x

makeUnsafeIo: IO ((x: Type) -> IO x -> x)
makeUnsafeIo = map makeUnsafeIoHelper extractWorld

[aDifferentJT]

I had the related issue #743 break things in some real code

[aDifferentJT]

Would this be better done not as subtyping but with an implicit insertion of the following function?

removeLinearity : ((1 _ : a) -> b) -> a -> b
removeLinearity f x = f x

[ohad]

@edwinb wrote:

I've been trying to use this to break linearity for something concrete, but with no success.

Why is this not really bad already?

foo : ((x : a) -> (a,a)) ~=~ ((1 x : a) -> (a,a))
foo = Refl

diagonal : (1 x : a) -> (a,a)
diagonal = let u = replace {p = id} foo in u (\x => (x,x))

[aDifferentJT]

Ah, I think what @edwinb was doing before was using rewrite not replace and since rewrite requires the equality the other way around.
He was saying that having ((_ : a) -> (a,a)) = ((1 _ : a) -> (a,a)) meant we could convert a linear function to an unrestricted one but not vice versa which would then mean that there's a problem with replace. Obviously replace is a perfectly legitimate term so that's not going to work.

[ohad]

I'm still confused. We can get both equations:

foo : ((x : a) -> (a,a)) ~=~ ((1 x : a) -> (a,a))
foo = Refl

foo' : ((1 x : a) -> (a,a)) ~=~ ((x : a) -> (a,a))
foo' = let u = replace {p = \w => w ~=~ (x : a) -> (a,a) } foo in u Refl

so this can't be about the direction of rewriting...

[aDifferentJT]

Yeah, I think that unless we want to fully embrace the concept of variance which is necessary whenever you have subtyping (I think this would be a mistake) we need to drop subtyping.

[aDifferentJT]

The same logic that allows us to convert a (1 _ : a) -> b to an a -> b also allows us to convert an (a -> b) -> c to a ((1 _ : a) -> b) -> c but this isn't done at the moment. I imagine that'd create even more issues using the current system though if we're inserting functions like removeLinearity this could also be done.

[KyleDavidE]

Back when I was thinking with this I noticed that most of the time that it seems like the language is stopping you from breaking linearity using this it is actually an issue of type inference not type checking, so if you make everything explicit it can breaks. (This is what causes the illusion of the direction of rewriting mattering)

Subtyping is definitely weird but it seems like it seems like if it is to be dropped, something else needs to go in its place (ie. Linearity polymorphism) since it is definitely a real world use case that comes up a ton. Especially if we want people to be able to aggressively declare functions as linear whenever possible.

[edwinb]

Since this is an issue of inference, I am wondering if it would be better to extend unification to have "multiplicity variables" which are resolved later in the process. At the moment they have to be solved immediately, which is what causes the guessing. There is a PR to remove subtyping, but I'm reluctant to merge because it is quite limiting.

[aDifferentJT]

Is this an issue of inference? #743 doesn’t seem to be an issue of inference, plus I don’t see inference causing an issue in @ohad’s example:

@edwinb wrote:

I've been trying to use this to break linearity for something concrete, but with no success.

Why is this not really bad already?

foo : ((x : a) -> (a,a)) ~=~ ((1 x : a) -> (a,a))
foo = Refl

diagonal : (1 x : a) -> (a,a)
diagonal = let u = replace {p = id} foo in u (\x => (x,x))

I think the issue is having subtyping but not variance (and I really don’t want variance, that seems like an enormous headache)

[edwinb]

Well that's awkward. We definitely don't want to have to think about that. We'll probably have to make the multiplicities incompatible then. It's a shame that it'll make some libraries harder to write, but we can't have a way to subvert linearity.

[jasoncarr0]

Would it not be a possibility to have variance only for function args/returns, but not anywhere else (e.g. the equality type)