Show newer
jonoodle :dragnloaf: boosted

I just need elasticsearch to stay alive for like a minute

did I post the original thread on here as well lol
the paper might honestly predate this place being a real contender for announcing actual things lol

Show thread

never mind I've just realized that my other problem isn't a problem at all and that type checking is failing because it's supposed to fail. good thing the principled manners of the type system is there to catch me when I'm thinking silly things even though I think it's the type system that's wrong all the time lol

Show thread

I wish I could know what levels variables were used at going on
I would rather not have to unify-and-solve for them

Show thread

puzzles for tomorrow. for now I've got to go home bc I have computer architecture early tmrw morning and learning more Verilog :/

Show thread

but I can also grow the level by cumul
then it doesn't matter what level the variable is
blasphemous

Show thread

hm. this is a different bug but I think I could justify shrinking the level of any variable from the context. that's very strange

Show thread

I'm not sure how to proceed. I can't just make up a larger level to check against a. I suppose I could synth the type of a and compare against the type of b, but then I'd need to reconcile the mismatching levels, and it seems rather incorrect to take a max of levels here rather than isolated in a cumulativity judgement. I don't think I want to make b a a check judgement, I don't think, since dependent applications aren't? but if b a were checked against B at a particular level I could infer the type of a, making sure that its level isn't too big, and then reconstruct A → B to check against b at the given level

Show thread

I've never seen the James Yoo singing lore...

this is the rule

Γ ⊢ b ⇑ A → B @ j
Γ ⊢ a ⇓ A @ j
---------------
Γ ⊢ b a ⇑ B @ j

except this breaks when b gets inferred at a smaller level such that a fails to check at that level lol

Show thread

lmao my inference algorithm is having trouble with domains at smaller levels

jonoodle :dragnloaf: boosted

my original twitter thread was good imo
I don't think anything has changed since then

Show thread

what am I supposed to say abt the paper other than "it's out" I barely remember the contents

lmao I got it to type check but I don't know why and I have a bunch of inferred arguments I can't mentally deduce

Show thread
(Set
(lsuc (lsuc (lsuc (lsuc (lsuc ℓ)))) ⊔
lsuc (lsuc (lsuc (lsuc (lsuc ℓ₁))))
⊔ lsuc (lsuc (lsuc (lsuc (lsuc ℓ₂))))
⊔ lsuc (lsuc _ℓ₂_72)
⊔ lsuc (lsuc _ℓ_75)
⊔ lsuc (lsuc _ℓ₁_76)))
is not less or equal than
(Set (lsuc (lsuc ℓ) ⊔ lsuc (lsuc ℓ₁) ⊔ lsuc (lsuc ℓ₂)))

hell world

Show thread

Agda please I beg stop solving down to lzero I just need a placeholder whilst I think

Show thread
Show older
types.pl

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