one last problem when trying to convert to Idris2
Closed this issue · 7 comments
I appreciate you haven't looked at this library for a long time however if you are still interested, I've been trying to get it to work with Idris 2. I have only one function left that's giving me issues (apart from Examples.idr but I think that will be easier to solve). The last error can be seen by getting the master branch from https://github.com/shmish111/idris-lens and trying to build with idris2 idris2 --build lens.ipkg
It looks like you figured it out?
yes, someone on the Idris Slack channel helped out. Are you still interested in maintaining this library?
Yes, to a degree.
I'm not hugely using Idris at the moment, but it's a skill to maintain.
Do you want commit access?
No it's ok, I'll open a PR. I would like a review but if you don't have time you can merge it anyway, better than just giving me commit access for now I think.
I do have an issue that you might help with. In Ex7 https://github.com/HuwCampbell/idris-lens/blob/master/Control/Lens/Examples.idr#L55 you don't have Additive in Idris 2 since you can have named instances of Monoid for Nat. However why do I need a Monoid at all in this case?
f : Either (String, Nat) Int -> Nat
f = view (_Left . _2)
Seems like it has the signature f : Monoid m => Either (a, m) b -> Nat but it's just view (_Left . _2) which seems like a prism that shouldn't need a monoid?
ah, so the Idris slack channel helped me understand this. It's because you are using a prism on a view and in your implementation that compiles as long as you have a default value (i.e. the monoid I'm missing).