Show newer

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

Show thread

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"

Show thread

Uh oh I'm going down a rabbit hole of eta equivalences

Show thread

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

Show thread

For a moment I forgot "semantics" also means operational semantics/reduction rules etc. and I thought ppl were referring to, like, a model of a calculus in some theory

*Your Internet connection is unstable" yes Zoom. I know. I can hear everyone's voices sounding like broken springs this you do not need to tell me

Surely someone has done it before and I just don't know what that kind of reduction rule is called

Show thread

You also need a reduction rule that reduces case expressions/eliminators with identical branches to the branch in order to preserve confluence I think, but I don't have time to prove this

Show thread

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

Show thread

@ionchy logical relations, kripke logical relations, step-index models, Church-rosser, iswim, full abstraction

How is normalisation and termination different?
How is normal form and canonical form different?
How is subject reduction and preservation different?
How is type safety and type soundness different?

I respect all directions of research in type theory. That being said, , and I look forward to finally defeating it tomorrow

type safety, canonicity, type preservation, subject reduction, progress, confluence, normalization, termination, consistency
There are so many words

All it takes for a hashtag to trend is literally just five different people tooting it apparently

Show thread

I chime in with a haven't you people ever heard of
closing the g*ddamn

Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.