Show newer

boundary separation is just η for paths send toot

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

Show thread

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

Show thread

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

Show thread

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
⊢ Γ boosted

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

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

Show thread

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

Show thread

oops i forgot everything about nbe again

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

Show thread

probably don't need all of these but fine

Show thread

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
types.pl

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