-
Notifications
You must be signed in to change notification settings - Fork 375
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
Loss of Linearity in Interaction of Abstract Interfaces and Linear State Transformer Monad #3287
Comments
What's the type of |
Hi! Thanks so much for your response. The self-contained file is linked at the very top, I will put it here again: https://github.com/Lichborne/IdrisLinearityIssue/blob/main/ErrorExamples.idr innerFuncDummy is a dummy function : AbstractInterface t => (i : Nat) -> (m: Nat) -> LVect i Nat -@ LStateT (t m) (t m) (LVect i Nat), that is;
In the real-life scenario, there is a function here that actually does something, which is why this is included, but in this case it's just lifting to the right context. Hope this helps. |
Writing Ditching the named application style entirely,
Moving on to
Adding a There seems to be an issue with the way named application is elaborated. |
Dear gallais, Thanks so much! Hope I did not waste your time. Best, |
Not at all, there does seem to be a bug hiding behind the non-bug of the shrunken case. |
A full explanation of and a minimal case for reproducing the problem can be found here: https://github.com/Lichborne/IdrisLinearityIssue/blob/main/ErrorExamples.idr
Depends only on Data.Linear.LVect and Data.Linear.Notation
Steps to Reproduce
Firstly, we create a linear state transformer monad as in the file, with the usual functions. In the real-life cenario, there are two slightly different versions, but this is sufficient to get the issue.
Then, we have two separate abstract interfaces
Then, we attempt to first use the above, and then take the LVect out and move it up and do something with it in the outer interface. innerFuncDummy is just a dummy function on the inner interface. See ErrorExamples.idr.
Expected Behavior
Type-checks.
Observed Behavior
Fails to check that qs is linear ("use of non-linear qs in a linear context").
I hope I am doing something wrong here. Otherwise, qs is clearly linear, used in a linear context, so it seems to me that this should be alright.
The text was updated successfully, but these errors were encountered: