I respect all directions of research in type theory. That being said, #AntiWTypeCrew, and I look forward to finally defeating it tomorrow
I regret to announce that I will not be defeating W types today, because from my experiments (and an old paper) I found that all you need for W types to behave nicely in ITT are eta rules and an explicit base case for W
I've discovered that the eta rules for sums (and by extension, case expressions) are in fact not merely some filling-up rules, but also cover a lot more pieces
Uh oh I'm going down a rabbit hole of eta equivalences
There is so much literature on what I thought would be a simple case of "I just need to look it up and I'll be done"
I've decided to pick four eta reductions as my hallowed laws and discarded the rest
I have not and will not prove that terms will normalize, but I think they do, since they're reduction rules and they go from bigger terms to smaller terms (no substitution required)
I'm not too sure about confluence since I did discard one big giant rule that's supposed to help the set be equivalent in some sense to the proper (but undecidable?) eta equivalence rule, but I've decided to solve that problem by not caring
Now I can get back to defeating the W types
Are you KIDDING me. One of these eta rules broke subject reduction
[SCENE: Γ = (P: Unit -> Type), (x: Unit), (f: (x: Unit) -> P x)]
Jesus: One of you will betray me tonight.
Γ ⊢ case_P x of [() ⇒ f ()] ⇝ f x: Is it me, Jesus?
Jesus: No.
Γ ⊢ case_(λx. Unit) x of [() ⇒ ()] ⇝ x: Is it me, Jesus?
Jesus: It's not you either.
Γ ⊢ case_P x of [() ⇒ f ()] ⇝ f (): Is it me, Jesus?
Jesus: *mockingly* Is it meee, Jesuuus??
This could never happen with inductive types with more than one branch since the expected types of the branches are different
This could never happen with constructors that take any arguments since the eta contraction only occurs on constant branches
Which means anything shaped like the unit type is literally the only time subject reduction could break
I have a fourth eta rule and it breaks well-typedness after reduction lmao
I guess these eta rules really can't be generalized for dependent case expressions
I have defeated the W types
It took me a total of five different eta laws
You may have W types in ITT only if you have explicit base cases and all five of those eta laws
(Thankfully those ones no longer cause typey problems)
I therefore conclude that W types are bad, ugly, gross, and disgusting
@ionchy I think nlab has something to say about this
@ionchy oooh wheres ur formulation
@pounce https://github.com/ionathanch/ttzoo/blob/main/The_Type_Theory_Zoo.pdf
Page 16 to 20
I'm not too pleased at the big arbitrary summary of basic types that I need to introduce at the bottom of p. 16 but I really didn't want to write all the typing rules out here and I'm sure eventually I'll have a section or chapter on MLTT types where all of that can go
Also Jordy did not like the eta contraction rules lol
@pounce I mean I don't like them either, which is why I'm cancelling W types once and for all
@vdash it's ok I have glorious eta equivalences now where eta has no directional component
@vdash beta is a vector, eta is a scalar
@ionchy This is acceptable. I will allow this
@ionchy I think I might incorporate some eta conversion rules
I could add a reduction rule that reduces anything of type Unit to ()... This would be for literally any inductive type shaped like a unit...... That feels cursed