goldfirere
commented
6 years ago What you want is reasonable. And perhaps key functions, like foldr, can be rewritten as you suggest. But part of the point of singletons is so that you don't have to rewrite your functions! Yet, option (2) seems terrible and fragile.
Maybe the solution is for lambda-lifting to be a bit cleverer in its approach. We could likely tell statically that we don't need foldr's last argument and so can leave it off when lifting. That will solve your immediate problem, but perhaps we can settle for that, for now.
RyanGlScott
infinity0
A proof about a function needs to have the implementation details of the function. In
singletons, functions are type families, and type families must expose all their equations (AKA their implementation). However, functions that uselet/wherecreate helper type families, where the implementation is known, but the type families themselves have unutterable names. It becomes impossible to write proofs for these hidden functions, so proofs for the whole function become impossible.E.g.
Both cases fail with a similar error
The issue is that the
goinfoldr, when promoted, gets an (unused) argument that representsfoldr's list argument. This mucks up the proof, where it isn't clear that the argument doesn't matter. Because this function has no stable name, not to mention its unexported status, one can't prove around that. It seems impossible to writesumIs.I feel like a fix for this deserves to be in
singletons. Here are a couple ways:Remove
gofromfoldr. Replacingfoldrwith a nicer version fixes this:I think, sometimes, this strategy will fail. In those cases, the helper function can be wholly lifted out. However, this is a complicated procedure. Further, the changes involved are to the functions being promoted themselves. This requires actual effort by the person writing the functions (i.e. me), which is at odds to the fact that I am lazy. If the promoted functions in
singletonswere changed like this, I also think maintainability would take a hit, due to the changes to thebasecodesingletonscopies.Expose the implementation details of promoted functions. Give stable names to all the supporting definitions for a promoted function, which lets them be exported and talked about. This kicks the number of things that can appear in export lists from "high" to "higher" (further evidence for TH-controlled exports). This also has the effect of coupling (even further than usual) the API of a promoted function to the exact way
singletonsdecides to promote it. I'm not sure what the stance is on that, or even how fastsingletons's implementation changes currently. There's always the option of making only some things stable (e.g.whereclauses get stable names,cases don't, etc.).