Show newer

re: shop talk 

I mean anything not covered otherwise should be covered by reduction on both sides

Show thread

re: shop talk 

I'm not really sure what the application/lambda/let rules are there for? Like when are those ever going to matter

Show thread

re: shop talk 

I think on paper I can do away with e=e as I've written it down bc we can sort of implicitly understand what "syntactic equality" means without needing to write down the tedium
So I can condense this into smth smaller I think

Show thread

re: shop talk 

In any case it's not so obvious that subtyping is transitive this way

Show thread

re: shop talk 

They actually put the congruence rules inside of the 1-step ones but I personally don't like that
The 1-step reductions should be "true" reductions where substitutions occur and the other ones, reflexivity and transitivity and congruence, are just "structural" ones

Show thread

re: shop talk 

The reduction rules (⊳*) contain the congruent, reflexive, transitive closure of the 1-step reductions

Show thread

re: shop talk 

afaict THIS is the definitive version of convertibility, where syntactic equality is interrupted by subtyping

Show thread

re: shop talk 

the subtyping is all tangled up with the congruence rules

Show thread

re: shop talk 

MetaCoq defines conversion as subtyping in both directions
hwhghwhgat

Show thread

re: shop talk 

eta: ∀ τ σ (e: (x: τ) → σ), λ x: τ. e x ≡ e
eta τ σ e = ?
nah there's nothing to reflect without eta

Show thread

re: shop talk 

maybe you get eta just from extensionality anyway

Show thread

re: shop talk 

I can validate my eta laws just by having them translate to a different set of eta laws right

Show thread

re: shop talk 

My thesis is going to have so many little details about things like this that have nothing to do with sized types lol

Show thread

re: shop talk 

untyped conversion... eta equivalence... cumulativity... long ago the three nations never lived in harmony actually it doesn't exist in any formal models

Show thread

re: shop talk 

fixed
I'm thinking about streams now. if induction on sized lists corresponds to well-founded induction on their size, what does coinduction to make streams correspond to...? it couldn't possibly be well-founded induction as well

Show thread

re: shop talk 

confirmed with Coq though, the guard checker says it's ok

Show thread

What's the dependent types of particle physics lol

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.