Cool! This reminds me of dimensional analysis, but with types instead of dimensions (and types have more structure cos “->” is not commutative).
Also, I guess because of dependent types’ connection with constructive mathematics, this works less well if you want to create a proof that uses excluded middle? I suppose you would end up with something of the type (P → ⊥) → ⊥ and then be stuck
(Minor point: is the reason you say “basically two options” for because you could also have h(h(fxx)) etc.? I guess we eventually prove that that would be the same function!)
Dimensional analysis is absolutely an instance of what I’m talking about!
As for only being able to do constructive stuff, you actually can do classical stuff as well, but you have to explicitly assume the law of the excluded middle. For example, if in Lean I write
axiom lem (P: Prop): P ∨ ¬P
then I can start doing classical reasoning.
Also, you’re totally right that you could also do h(h(fxx)) and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest possible way to do it you’ll solve the problem by the time you get to h(fxx).
Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!
Cool! This reminds me of dimensional analysis, but with types instead of dimensions (and types have more structure cos “->” is not commutative).
Also, I guess because of dependent types’ connection with constructive mathematics, this works less well if you want to create a proof that uses excluded middle? I suppose you would end up with something of the type (P → ⊥) → ⊥ and then be stuck
(Minor point: is the reason you say “basically two options” for because you could also have h(h(fxx)) etc.? I guess we eventually prove that that would be the same function!)
Dimensional analysis is absolutely an instance of what I’m talking about!
As for only being able to do constructive stuff, you actually can do classical stuff as well, but you have to explicitly assume the law of the excluded middle. For example, if in Lean I write
then I can start doing classical reasoning.
Also, you’re totally right that you could also do h(h(fxx)) and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest possible way to do it you’ll solve the problem by the time you get to h(fxx).
Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!