Open RyanGlScott opened 4 years ago
Question: what should we do to resolve inconsistencies (1)-(3) above? Here are my thoughts:
My initial gut feeling is that using genDefunSymbols
on the name of a function, class method, data constructor, or record selector should produce defunctionalization symbols for the promoted equivalent of that name. For instance, genDefunSymbols ['id]
should produce IdSym0
and IdSym1
.
There is one potential sticking point with this idea. Recall that this is the code that gets generated for IdSym1
:
type IdSym1 (x :: a) = Id x
This code assumes that the promoted Id
type family already exists. However, if Id
doesn't exist, then this code will error out. Therefore, allowing genDefunSymbols
to be invoked on id
offers a new way to shoot yourself in the foot.
It is worth noting, however, that there is already a footgun of a similar variety on the quoting side. This code will also error out if Id
does not exist:
$(singletonsOnly [d| type Id x = x |])
genDefunSymbols [''D]
(where D
is the name of a data type) produce defunctionalization symbols for D
's promoted record selectors. Again, this is a footgun if any of the promoted record selector type families do not yet exist, but it is exactly the same footgun as in (1).This is a tricky one. Personally, I find it quite strange that genDefunSymbols
generates defunctionalization symbols for class names. If C
is the name of a class, then one doesn't need to generate CSym0
at all, since you can just as well use TyCon C
to achieve the same thing. But alas, someone specifically asked for this feature, so it might be a bit reckless to change this convention.
Having just written this, I wonder if we should explore an alternative design where genDefunSymbols
doesn't exhibit the "bundling" behavior that it currently has. For example, given data D a = MkD { unD :: a }
, then genDefunSymbols [''D]
won't just generate DSym0
et al.. It will also bundle along MkDSym0
and UnDSym0
et al. Perhaps genDefunSymbols [''D]
should simply generate DSym0
et al. and nothing else. If you want MkDSym0
et al., you will have to write genDefunSymbols ['MkD]
explicitly, and similarly for UnDSym0
et al.
As far as classes go, this would mean that genDefunSymbols [''C]
would continue to produce defunctionalization symbols. If C
had any associated type families or methods, you would have to call genDefunSymbols
on them separately.
The downside to this approach is that this code:
$(genDefunSymbols [''D, 'MkD, 'unD])
And this code:
$(singletons [d| data D = MkD { unD :: a } |])
Would no longer do the same thing, as the former would produce defunctionalization symbols for D
, but the latter would not. Perhaps this inconsistency is acceptable, however, since this hypothetical version of genDefunSymbols
is explicitly designed to work at a more fine-grained level than quoting is.
Thanks for this thorough analysis. Here is what I propose as a way forward -- but my opinion here is fairly weak, and I am happy with many possible directions (including simply documenting the current strange setup, which I don't believe is actively hurting anyone).
I think genDefunSymbols
should blindly generate defunctionalization symbols for all the names it is given. It should not bundle. That has a very nice, simple specification. If that means that the generated code refers to some name that is not in scope, then so be it.
Perhaps it is worth adding genAllDefunSymbols
, which generates defunctionalization symbols for all the names passed to it, and any names which would be exported if you put (..)
after any of these names in an export list (ignoring the possibility that some of these names may be out of scope). That's also a specification users are likely to find intuitive. It means that classes include their methods and associated types, and datatypes include their constructors.
I think the quoting mechanisms should produce only the defunctionalization symbols they need -- just as they work now. Which ones are generated should be documented, of course.
These ideas broadly follow yours, but with the possibility that some find the bundling behavior useful.
I like your suggested design of having both genDefunSymbols
and genAllDefunSymbols
. I wonder if it's worth adding another variant that generates defunctionalization symbol names using the same approach as quoting does? After all, my plan for implementing this idea was to add an extra argument to D.S.Promote.Defun.defunctionalize
of type GenSymbolsDepth
, where:
data GenSymbolsDepth
= GenNameOnlyDefunSymbols
| GenNonDataOrClassDefunSymbols
| GenAllDefunSymbols
With this approach, genDefunSymbols
becomes (roughly) an alias for defunctionalize GenNameOnlyDefunSymbols
and genAllDefunSymbols
becomes an alias for defunctionalize GenAllDefunSymbols
. I use GenNonDataOrClassDefunSymbols
when invoking defunctionalize
from functions that deal with quoted declarations (such as promote
and singletons
), but there is no genNonDataOrClassDefunSymbols
alias for defunctionalize GenNonDataOrClassDefunSymbols
. Should there be?
I don't feel the need for exposing this much flexibility, per se. Is anyone asking for it? But I'm also not actively against exposing it.
I don't feel the need for exposing this much flexibility, per se. Is anyone asking for it?
It's hard to answer that question since this new design is still hypothetical. But it is worth noting that anyone who relies on the current behavior of $(genDefunSymbols [''D])
(given data D = D_1 | ... D_n
) won't have a clear migration path in the new design, since neither the new genDefunSymbols
nor genAllDefunSymbols
will do quite the same thing. A user could conceivably write out each individual constructor to be defunctionalized (i.e., write $(genDefunSymbols [''D_1, ..., ''D_n]
), but I could foresee this being annoying if n
is large.
Of course, it could be the case that my worrying is completely unfounded and that no one will miss the current behavior of genDefunSymbols
. But I don't know how to gauge how users would react to this idea.
Given that there are about 20 usages of genDefunSymbols
in all of hackage (not counting singletons
), I'm not very worried about the migration story. Futhermore, generating all symbols is rarely troublesome. In other words, do whatever is easiest.
I briefly looked into implementing this, but it turned out to be much more work than I originally had expected. For now, I'll just document the various corner cases of genDefunSymbols
in the README
and leave this issue open as a reminder to implement the better design in https://github.com/goldfirere/singletons/issues/429#issuecomment-569340217 (or to just wait until UnsaturatedTypeFamilies
is a thing and makes defunctionalization obsolete, I suppose). I've taken care of the documentation side of things in #441.
While pondering the questions in https://github.com/goldfirere/singletons/pull/427#discussion_r361532779, I realized that trying to document the existing status quo regarding what language constructs are OK to defunctionalize is much, much trickier than I thought. The main source of trickiness is that
singletons
has an inconsistent ruleset: whether something is defunctionalized or not depends on whether it is quoted (i.e.,$(singletons [d| ... |])
) or reified (i.e.,$(genDefunSymbols [...])
):Quoted
Functions
Legal. Just define the function in quotes, e.g.,
And
singletons
will produceFooSym0
andFooSym1
.Classes
Legal, but only in the sense that quoted classes will produce defunctionalization symbols for the promoted class methods and associated type families, e.g.,
Defunctionalization symbols for the class itself are not produced.
Class methods
Legal. See the "Classes" section.
Type families and synonyms
Legal. Quoted type families and synonyms are defunctionalized as you would expect. See also the "Classes" section for how associated type families are handled.
Data types
Legal, but only in the sense that quoted data types will produce defunctionalization symbols for the promoted record selectors and data constructors, e.g.,
Defunctionalization symbols for the data type itself are not produced.
Data constructors
Legal. See the "Data types" section.
Record selectors
Legal. See the "Data types" section.
Reified
Functions
Illegal. Attempting to use
genDefunSymbols
on a function name will throw an error:Classes
Legal. Reified class names will get defunctionalization symbols, but its promoted class methods and associated type families will not be defunctionalized:
Class methods
Illegal. Attempting to use
genDefunSymbols
on a class method name will throw an error:Reifying the parent class name will not produce defunctionalization symbols for its promoted class methods either.
Type families and synonyms
Legal. Reified type families and synonyms are defunctionalized as you would expect. Associated type families are not automatically defunctionalized when the parent class name is reified, but one can just as well reify the associated type family name directly.
Data types
Legal, but only in the sense that reified data types will produce defunctionalization symbols for the data constructors, e.g.,
Data constructors
Illegal. Attempting to use
genDefunSymbols
on a data constructor name will throw an error:The only way to defunctionalize data constructor names through reification is to reify the parent data type.
Record selectors
Illegal. Attempting to use
genDefunSymbols
on a record selector name will throw an error:Reifying the parent data type name will not produce defunctionalization symbols for its promoted record selectors either.
There are multiple inconsistencies between quote-based defunctionalization and reification-based defunctionalization: