Ah yes, see [6.8 Variations] where they touch on this.
Conversation
Cheers for the assistance, really helps! What would the advantage of having eta-expension be?
1
No problem! Well, there are a couple advantages, the biggest for the user is that more "obviously equal things" are judged equal by the system. For instance, \x. 0 + x = \x. x. But it also captures the universal properties for certain types.
1
1
I should be more careful with my examples.. that one holds in systems without eta for pi I expect. But composition with identity being the identity is an example of eta :)
1
1
Is this eta? github.com/jozefg/nbe-for
I'm guessing this is why you don't look at whether `f` is a lambda?
1
Yep exactly. Same with sigma below, you just convert everything to its eta long form.
1
You mentioned that this might interact poorly with non-termination. Why might that be, and could it lead me astray given I want a more Idrisy style of language, mixing total and unsure-if total stuff?
1
I guess I was worried about how you would get the eta-long form for [loop = loop] where [loop : A -> B]. Just termination check things before you evaluate them I guess if you don't want your evaler to loop.
1
1
Wondering what you think of kosmikus.org/PiSigma/PiSigm as a core language - it seems to have a better story regarding recursion and induction/coinduction, but I see Mini-TT referred to by you and more often 🤔
This Tweet was deleted by the Tweet author. Learn more