I am currently trying to add quantities to my little dep typed language following I Got Plenty O' Nuthin' by Mcbride. The QTT paper points out that there is a flaw in the original typing rules which I didn't quite understand.
Conversation
My reading of it is that you can eta-expand a linear function to be used in an unrestricted way. Is that a particular problem? I much prefer the McBride approach because I can actually figure out how to implement it but I don't know if the issue will come back to bite me.
2
1
4
if either of you have thought about this issue I’d love to hear any conclusions you came to.
2
3
I dunno! I think atennapel on the Pikelet matrix/discord implemented QTT before - not sure if they know! My solution if I am confused by typing rules is to look around to try to see if anyone else has implemented the rules on github, and see if that helps me understand 😳
2
1
5
Oh, now that I think of it, I remember telling going through some of the issues with the McBride paper, but I dunno if he can remember at all! It was a couple of years ago I think!