Permit empty closed type families
ClosedPublic

Authored by adamgundry on Apr 15 2015, 4:20 AM.

Details

Summary

Fixes Trac #9840 and Trac #10306, and includes an alternative resolution to Trac #8028. Basically all this does is remove some prohibitions on empty closed type families, and document them in the user guide.

Test Plan

Added indexed-types/should_compile/T9840 and updated indexed-types/should_fail/ClosedFam4 and th/T8028.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
adamgundry retitled this revision from to Permit empty closed type families.Apr 15 2015, 4:20 AM
adamgundry updated this object.
adamgundry edited the test plan for this revision. (Show Details)
adamgundry added reviewers: austin, simonpj, goldfire.
adamgundry updated the Trac tickets for this revision.
simonpj requested changes to this revision.Apr 15 2015, 4:35 AM

See my note above. Otherwise fine.

compiler/types/TyCon.hs
705

This doesn't look right. A closed family with no equations should be a ClosedSynFamilyTyCon, with no equations. The AbstractClosed.. thing is exclusively for the hs-boot stuff.

Simon

This revision now requires changes to proceed.Apr 15 2015, 4:35 AM
adamgundry added inline comments.Apr 15 2015, 5:29 AM
compiler/types/TyCon.hs
705

It seems a lot easier to make empty closed families not have a CoAxiom at all, rather than have a CoAxiom with no branches. In particular, it's not currently possible to have an empty BranchList. Maybe it would be better to have another constructor here, rather than reusing AbstractClosedSynFamilyTyCon, but still avoiding the need for CoAxioms for empty closed families?

adamgundry updated this revision to Diff 2767.Apr 15 2015, 6:16 AM
  • Fix panic when reifying an empty or built-in type family
  • Distinguish between abstract and empty closed type families

Adam, wouldn't it make sense to add another constructor to FamilyInfo? That would require a bit more work in the parser but implementation of tcFamDecl1 should become more straightforward.

compiler/types/TyCon.hs
705

I think that instead of saying "Abstract type families can only appear in hs-boot files" we could now have a new story that says "Abstract type families are closed type families that have no equations" without paying attention to where they appear (hs or hs-boot files).

If we really wanted to represent empty closed type families using ClosedSynFamTyCon a possible alternative would be to change the type of CoAxiom.co_ax_branches from BranchList CoAxBranch br to Maybe (BranchList CoAxBranch br). I don't think this is a good idea but just noting that the possibility exists.

adamgundry updated this revision to Diff 2768.Apr 15 2015, 6:52 AM
  • Update haddock submodule to fix build failure due to new constructor

I've updated the diff with an extra constructor for FamTyConFlav, so that we can distinguish between EmptyClosedSynFamilyTyCon and AbstractClosedSynFamilyTyCon. It's not very difficult, but I'm not sure it's worth it and I would agree with @jstolarek that we should simply say "Abstract type families are closed type families that have no equations". Note that Any is already such a type family, treated as abstract even though it is not defined in a boot file. @simonpj, does that make sense to you?

Exploring the alternative was worthwhile, however, because I found and fixed a panic when using TH to reify abstract/built-in type families (e.g. Any or type-level (+)).

Adam, wouldn't it make sense to add another constructor to FamilyInfo? That would require a bit more work in the parser but implementation of tcFamDecl1 should become more straightforward.

I'm not sure I follow: do you mean to distinguish syntactically between ClosedTypeFamily [] (an empty type family) and a new constructor for abstract type families?

adamgundry updated this object.Apr 15 2015, 7:16 AM
adamgundry edited the test plan for this revision. (Show Details)

I'm not sure I follow: do you mean to distinguish syntactically between ClosedTypeFamily [] (an empty type family) and a new constructor for abstract type families?

Yes, that's what I meant. I thought it would be nice to have close correspondence between representations in the parser and in the typechecker. But then I realized that this would also require lots of changes to Template Haskell so in the end I think it's not worth it.

adamgundry updated the Trac tickets for this revision.Apr 15 2015, 7:18 AM

One thing I wanted to test is whether it is safe to declare a type family in a .hs-boot file and then declare that type family as an empty type family in .hs file.

simonpj requested changes to this revision.Apr 15 2015, 6:00 PM

It seems a lot easier to make empty closed families not have a CoAxiom at all, rather than have a CoAxiom with no branches. In particular, it's not currently possible to have an empty BranchList.

Why? One branch you get an axiom. Two branches you get an axiom. No branches, you still get an axiom. Why make it different? For algebraic data types with no constructors the list of constructors is just empty. Adding a new flavour of family just doesn't smell right to me.

If BranchList isn't capable of an empty list, perhaps it should be! I've always thought it seemed a bit over-elaborate anyway.

Simon

This revision now requires changes to proceed.Apr 15 2015, 6:00 PM
In D841#22861, @simonpj wrote:

In particular, it's not currently possible to have an empty BranchList.

Why?

Current implementation does not allow an empty BranchList:

data BranchList a (br :: AxiomBranched) where
  FirstBranch :: a -> BranchList a br
  NextBranch :: a -> BranchList a br -> BranchList a Branched

toBranchList :: [a] -> BranchList a Branched
toBranchList [] = pprPanic "toBranchList" empty
toBranchList [b] = FirstBranch b
toBranchList (h:t) = NextBranch h (toBranchList t)
In D841#22861, @simonpj wrote:

In particular, it's not currently possible to have an empty BranchList.

Why?

Current implementation does not allow an empty BranchList:

Yes I know that. My comment was questioning it.

One thing I wanted to test is whether it is safe to declare a type family in a .hs-boot file and then declare that type family as an empty type family in .hs file.

Good point, I'll add a test case.

In D841#22861, @simonpj wrote:

Why? One branch you get an axiom. Two branches you get an axiom. No branches, you still get an axiom. Why make it different? For algebraic data types with no constructors the list of constructors is just empty. Adding a new flavour of family just doesn't smell right to me.

What is an axiom with no branches? It doesn't prove anything, and can never be used in Core, so it seems strange to even give it a Name. We could use Maybe (CoAxiom Branched) as the representation for a possibly-empty axiom, and regard CoAxiom Branched as representing non-empty axioms. That gets rid of the extra family flavour and keeps the patch simple.

If BranchList isn't capable of an empty list, perhaps it should be! I've always thought it seemed a bit over-elaborate anyway.

We could redesign BranchList to support empty lists, but that means a rather bigger surface area for this patch and requires checking that nothing relies on the assumption that the result of fromBranchList is non-empty.

What is an axiom with no branches? It doesn't prove anything, and can never be used in Core, so it seems strange to even give it a Name. We could use Maybe (CoAxiom Branched) as the representation for a possibly-empty axiom, and regard CoAxiom Branched as representing non-empty axioms. That gets rid of the extra family flavour and keeps the patch simple.

I could live with that. Please document it with a Note though.

adamgundry updated this revision to Diff 2775.Apr 16 2015, 5:22 AM
  • Extend T9840 test to cover empty type family in hs-boot file
  • Get rid of EmptyClosedSynFamilyTyCon in favour of Maybe CoAxiom in ClosedSynFamilyTyCon
  • Get rid of IfaceEmptyClosedSynFamilyTyCon (changes interface file format)

I have one question. Perhaps it is silly but I have to ask. Now that we can have empty closed type families represented using ClosedSynFamilyTyCon Nothing why not just remove AbstractClosedSynFamilyTyCon? I can't find anything that would go wrong if we did that. From what I see usage of AbstractClosedSynFamilyTyCon is limited to: a) definition of Any type family; b) type families defined in hs-boot files. My guess is that AbstractClosedSynFamilyTyCon was introduced to have a way to distinguish between normal closed type families (ie. ones in an .hs file, that are required to have at least one equation) and abstract closed type families that don't have any equations. But now we have two ways of internal representation for closed type families that don't have equations. This distinction is based only on the origin of the declaration (.hs or .hs-boot). There seems to be no difference in behaviour between the two. Wouldn't removing of AbstractClosedSynFamilyTyCon give us a more consistent story?

@jstolarek I believe you're right that we could remove AbstractClosedSynFamilyTyCon in favour of ClosedSynFamilyTyCon Nothing; that's isomorphic to what I did in my original patch, which simply used AbstractClosedSynFamilyTyCon for empty closed families. @simonpj asked that the hs-boot case continue to be distinguished. There is a subtle conceptual difference between an empty closed type family, and a closed type family whose equations are not yet known (but might be non-empty); the only place where the difference shows up is in checkBootTyCon. But since there is no way for Haskell to observe the emptiness of a type family, we could conflate these cases.

Indeed, Any is a perfectly ordinary empty type family. I guess it should probably now be a ClosedSynFamilyTyCon Nothing.

There is a subtle conceptual difference between an empty closed type family, and a closed type family whose equations are not yet known (but might be non-empty); the only place where the difference shows up is in checkBootTyCon.

Do you refer to the definition of eqFamFlav inside checkBootTyCon? If so then I don't see how it shows the difference between closed type family with yet unknown equations and empty closed type families. In fact it says that abstract closed type families and closed type families are the same.

Haven't yet looked at the code, but I have several comments. (Sorry for the delay on these -- I've been traveling and attending ETAPS, with irregular access. Home now.)

  • I think abstract and empty closed type families are different beasts and should be marked as so. If we solve Trac #9636, the difference will be manifest.
  • Any is just an empty closed type family. But when I changed it from being a magical tycon, we didn't have empty closed type families, so I cheated. Please do make it an empty closed type family. (Of course, if we solve Trac #9636, then Any becomes a new strange beast again: an empty closed type family that isn't an error. There's something interesting in here...)
  • I think it's probably better to just permit BranchList Branched to have 0 branches than to use Maybe (CoAxiom Branched). But you're right in that this would require a search for assumptions about non-emptiness. I believe that there are places where fromBranchList x is assumed to be non-empty.
  • The BranchList thing is perhaps heavy. I put it in because there are many places where we must know that a CoAxiom has precisely one branch (in dealing with newtypes and open type family instances). I wanted some compile-time guarantees. Are these worth the weight? I still think so, but I don't feel strongly about it. Removing BranchList would certainly be a simplification, but it would make GHC a tiny bit more error prone in the future.

I agree with everything Richard says.

I really want to keep the distinction between a closed family that is known to have no equations, and a signature for an as-yet-unknown family. It is possible that we treat the two identically at the moment, but please let's not conflate them.

Any is just an empty closed family; indeed, please make it so.

I can live with the Nothing story; but I think an axiom with zero branches would be better. If that means changing BranchedList, so be it. But I'm not going to stand and die for this.

Looking through the code, I see why the Maybe (CoAxiom Branched) is more expedient than allowing a BranchList Branched to have 0 branches. It is indeed probably simpler the way you've implemented it.

compiler/iface/IfaceSyn.hs
690

Isn't the where .. syntax for abstract CTFs? I would expect this to be where {} or similar.

compiler/typecheck/TcSplice.hs
1342

This should probably be its own TH.FamFlavour, but we may not need to fight that battle today.

1343

Ditto here.

compiler/types/TyCon.hs
1368–1369

This is very confusing. An abstract or empty CTF says, effectively, "no" to isClosedSynFamilyTyCon. This might agree fine with usages of this function, but perhaps it should be renamed.

docs/users_guide/glasgow_exts.xml
6051

I don't like this syntax for empty CTFs. What about where {}? Or even just where without anything after it?

And, I think we should make it possible to distinguish a concrete empty CTF from an abstract possibly-not-empty CTF in hs-boot files. As Backpack comes into being, the hs-boot file syntax will become more used, so this isn't as much of a corner case as it might seem.

6053

I would say that an empty closed type family is injective. Suppose E x is an empty CTF. If we know that E x ~ E Int, then it must be that x ~ Int, because E Int surely isn't reducing: it equals only itself.

Of course, this will only work once D202 lands.

Thanks @goldfire!

  • Any is just an empty closed type family. But when I changed it from being a magical tycon, we didn't have empty closed type families, so I cheated. Please do make it an empty closed type family. (Of course, if we solve Trac #9636, then Any becomes a new strange beast again: an empty closed type family that isn't an error. There's something interesting in here...)

I think the solution to Trac #9636 shouldn't involve making all closed type families automatically have an error clause; at least there should be a way to switch it off not just for Any. But that's a discussion for elsewhere...

  • The BranchList thing is perhaps heavy. I put it in because there are many places where we must know that a CoAxiom has precisely one branch (in dealing with newtypes and open type family instances). I wanted some compile-time guarantees. Are these worth the weight? I still think so, but I don't feel strongly about it. Removing BranchList would certainly be a simplification, but it would make GHC a tiny bit more error prone in the future.

I suspect an equally safe but more lightweight solution is possible if we allow empty branch lists: a BranchList Unbranched is always a singleton, while a BranchList Branched is an ordinary list. I'm coming to agree that this would be a worthwhile refactoring, but I think it's better to do it separately from this diff, to avoid getting in the way of D202.

compiler/typecheck/TcSplice.hs
1342

Agreed (on both counts). Let's wait until someone actually needs to see the difference in reify; at the moment I'll settle for GHC not crashing at this point!

compiler/types/TyCon.hs
1368–1369

Fair enough, I'll rename it.

docs/users_guide/glasgow_exts.xml
6051

I was trying to be lazy and avoid modifying the parser/AST, but you're right, it would be more consistent to use where <empty branch list> for an empty CTF and where .. for an abstract CTF. I'll give it a try.

6053

No no no no no! Injectivity would completely break my use case for empty CTFs: I want to use them to represent units-of-measure operators with their reduction behaviour implemented in a plugin. D202 doesn't *infer* injectivity for CTFs, does it? I think that would be a bad idea.

Of course, it would be fine (and indeed useful) to be able to declare empty CTFs with injectivity annotations.

jstolarek added inline comments.Apr 17 2015, 3:16 AM
docs/users_guide/glasgow_exts.xml
6053

D202 doesn't *infer* injectivity for CTFs, does it?

No, it doesn't. But even if we did that one day it should be simple to skip injectivity inference for empty closed type families.

Of course, it would be fine (and indeed useful) to be able to declare empty CTFs with injectivity annotations.

This raises the question how to ensure that reduction behaviour implemented by a plugin does not violate injectivity annotation.

adamgundry added inline comments.Apr 17 2015, 3:28 AM
docs/users_guide/glasgow_exts.xml
6053

This raises the question how to ensure that reduction behaviour implemented by a plugin does not violate injectivity annotation.

Our usual story for plugins is that they are responsible for the consistency of any axioms that they generate. I don't think this changes in the presence of injectivity annotations: if a plugin violates the specified injectivity properties of a type family, any resulting problems are the fault of the plugin, not GHC.

adamgundry updated this revision to Diff 2789.Apr 17 2015, 5:54 AM

Properly distinguish abstract and empty closed families

  • Make Any a non-abstract empty ClosedSynFamilyTyCon
  • Rename isClosedSynFamilyTyCon_maybe to isClosedSynFamilyTyConWithAxiom_maybe
  • Distinguish between abstract and empty type families in the parser
  • Update testsuite now that abstract and empty families parse differently
  • Update user's guide for syntactic difference between empty and abstract families
  • Rename test for Trac #10306 to match its ticket number
  • Update Haddock submodule

Thanks everyone for your feedback. Hopefully we're nearly there! I'm away on holiday next week, but will try to deal with any remaining issues and land this thereafter, unless anyone else wants to jump in first.

Note that there are also some haddock changes, but I don't think they should be controversial.

compiler/parser/Parser.y
1012–1022

I'd appreciate it if someone who knows their way around the parser and API annotations can quickly review this to make sure I haven't done anything stupid here.

Please see Trac #9840 for a proposal for a different direction here.

I suspect an equally safe but more lightweight solution is possible if we allow empty branch lists: a BranchList Unbranched is always a singleton, while a BranchList Branched is an ordinary list. I'm coming to agree that this would be a worthwhile refactoring, but I think it's better to do it separately from this diff, to avoid getting in the way of D202.

What a simple idea -- much better than the current story. Feel free to implement. Or if you don't feel free, I'll likely do this at some point in the future.

On the inferring-injectivity question: This debate lends further support to my recent ideas in Trac #9840. D202 currently does not infer injectivity for closed type families, but this choice was because Jan thought the user experience would be better without inference. I tend to agree. However, here we have a case where injectivity inference for CTFs would be downright wrong! This is a little alarming, because Simon and I proved injectivity checking sound & complete last week, suggesting that it's always safe to infer. The root problem: Adam doesn't want empty closed type families. He wants Something Else.

Just to be clear: I don't think my far-flung ideas in Trac #9840 or my ominous "He wants Something Else" should hold up this patch in the slightest. But I distinctly feel like there's a square peg going into a round hole somewhere.

compiler/deSugar/DsMeta.hs
330

This should error on Nothing. Otherwise, we're silently converting an abstract CTF to an empty one in a TH quote.

(To my shock and horror, TH really is allowed in hs-boot files. There's actually nothing wrong with TH in an hs-boot file, but it just feels so arcane!)

compiler/parser/Parser.y
1022

Seems reasonable to me. But I haven't a clue about API annotations. The non-annotations bits look fine.

compiler/prelude/TysPrim.hs
775

Should the type-lits operators be given the same treatment as Any here?

I suspect an equally safe but more lightweight solution is possible if we allow empty branch lists: a BranchList Unbranched is always a singleton, while a BranchList Branched is an ordinary list. I'm coming to agree that this would be a worthwhile refactoring, but I think it's better to do it separately from this diff, to avoid getting in the way of D202.

What a simple idea -- much better than the current story. Feel free to implement. Or if you don't feel free, I'll likely do this at some point in the future.

I'm all for it too!

Simon

See Trac #10344 for the task about simplifying BranchList. If that's included in the final version of this patch, please close the ticket. Thanks!

adamgundry updated this revision to Diff 2841.Apr 24 2015, 4:59 AM
  • Reject abstract CTFs in repFamilyDecl

Is this okay to land now?

I suspect an equally safe but more lightweight solution is possible if we allow empty branch lists: a BranchList Unbranched is always a singleton, while a BranchList Branched is an ordinary list. I'm coming to agree that this would be a worthwhile refactoring, but I think it's better to do it separately from this diff, to avoid getting in the way of D202.

What a simple idea -- much better than the current story. Feel free to implement. Or if you don't feel free, I'll likely do this at some point in the future.

Thanks for raising Trac #10344. I don't plan to do this right at the moment.

On the inferring-injectivity question: This debate lends further support to my recent ideas in Trac #9840. D202 currently does not infer injectivity for closed type families, but this choice was because Jan thought the user experience would be better without inference. I tend to agree. However, here we have a case where injectivity inference for CTFs would be downright wrong! This is a little alarming, because Simon and I proved injectivity checking sound & complete last week, suggesting that it's always safe to infer.

Well, it's safe in the sense that inferring injectivity of CTFs is a consistent extension of GHC's existing equational theory. Of course, making the equational theory stronger (allowing more equations to be proved) limits the ability of plugins to consistently extend it in other directions.

compiler/deSugar/DsMeta.hs
330

Fixed, and I've added a test. Good catch!

compiler/prelude/TysPrim.hs
775

I don't think so: there is already a separate BuiltInSynFamTyCon for type-lits operators, which captures their reduction behaviour.

goldfire accepted this revision.Apr 24 2015, 7:40 AM

Happy now.

Are you confident about the API annotations bit?

adamgundry updated this revision to Diff 2865.May 4 2015, 8:56 AM
  • Merge remote-tracking branch 'origin/master' into wip/T9840

Happy now.

Are you confident about the API annotations bit?

Thanks, I'll land. I've convinced myself that there is no less API annotations information than before, so I think it's okay for now. I'm not sure it is always possible to round-trip *abstract* CTFs, but *empty* ones should be fine.

This revision was automatically updated to reflect the committed changes.