Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multiplicity subtyping with dependent types can break linearity #357

Open
KyleDavidE opened this issue May 8, 2020 · 2 comments
Open

Multiplicity subtyping with dependent types can break linearity #357

KyleDavidE opened this issue May 8, 2020 · 2 comments

Comments

@KyleDavidE
Copy link

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
Copy link
Owner

edwinb commented May 9, 2020

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.

@KyleDavidE
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants