defer-typed-hol.es

ive connected the two dots, etc

boundary separation is just η for paths send toot

cubes!!!!!!!!

no that wont work cos in xtt you also need to check the endpoints of unconstrained dimensions. so idk what to do that isn't just checking everything 2ⁿ times. and like, keeping track of which dimensions are actually used where to keep n low

"something" being, i guess, at every equality application looking at the argument and going "is it 0? is it 1?"

look a type system post haven't seen one of them in a while

i feel like i might be like, 20% of the way to understanding nbe

like the typed stuff is mostly so you know what to η expand, it looks like? and the other big thing about it is to use closures or whatever to make application less repetitive. i thought "so what" cos i read explicit substitutions and immediately put closures in my main syntax like a dipshit, but i guess that is kind of a fucked up thing to do

idk how to do cube stuff in it tho. maybe you just shove the whole dimension environment into the eval step and do,,, *~*something*~*

⊢ Γ boosted

Time to consult the ancient scrolls (Luo 1992)

even in idris i cannot escape singletons

⊢ Γ boosted

actually this breaks the way everyone else is using absurd so nm lol

(but thx for putting up with my nonsense ionchy 💚💚)

if someone with a github account feels like writing a PR for idris2 to make the argument of absurd be zero i would appreciate it a lot

otherwise i guess i'll make an account

insert normalise xyz snowclone joke here

oops i forgot everything about nbe again

also λ, →, ⇒, obv

not to make the problem worse but it would be nice if u could write ⟦x + y⟧ for [|x + y|] imo

probably don't need all of these but fine

i like how idris has five ways to write effectful code

sugar free: (+) <$> act1 <*> act2 or act1 >>= \x => act2 >>= \y => pure (x + y)¹ do: do x <- act1; y <- act2; pure (x + y) comprehensive: [x + y | x <- act1, y <- act2] idiom: [|act1 + act2|] !!!!: pure (!x + !y) ¹since (<$>) (<*>) (>>=) are just functions these don't count as two ways imo

Show older

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