@theruran @a_breakin_glass @chjara it's not as expressive as a univalent type system but that's intentional, canonicity and proof relevance/only definitional *equality* (you can have other equivalences with like setoids etc) are IMO desirable in practical computing, since two different implementations of the same computation are usefully distinct with regard to operational characteristics. (and canonicity just makes interoperation tasks 100x easier)

@theruran @a_breakin_glass @chjara this is based on System S, and is mostly prior art from Formality (jcb and victor maia) minus the reflection stuff, which isn't that theoretically interesting. just different practical goals. I haven't read Barendregt so I don't know how PTS classifications work, but I know every corner of the lambda cube can be classified in terms of PTS stuff, and this shares a corner with inductive CoC plus primitives (a la coq etc.)

@theruran @a_breakin_glass @chjara @vidak oh i mean i'm very aware of thatthis stuff is pretty recenty, like... last few monthsbut i built it for a human interface/semantic computing/linguistics (maybe?) project that I've been working on for a few years now

@theruran @a_breakin_glass @chjara and no, that package is *just* a typechecker/stratification checker (simple validation step that replaces complicated termination checking by instead using a combination of affine types and explicit copies)and a few runtimes- simple beta reduction (used for typechecking)- CPU-side interaction nets- GPU-side interaction netsactual long-running operation will be through Capretta's delay monad compose with capability-ish effect monads

@theruran @a_breakin_glass @chjara @vidak i just need to be less of a mess and get back to building some actual toolsi've had something reasonably usable for the sort of computing environment i want like three times now and each time i've ended up stuck on some bit of incidental complexity in something someone else implementedso this time it's all clean-sheet(though based in prior art, i wouldn't want to have to come up with my own consistency proof for this stuff)

@a_breakin_glass @chjara you just need a reflective dependent typed lambda calculus *coughs*

@theruran @a_breakin_glass @chjara may be unclear since i don't know if i've discussed this with you personallyhttps://github.com/noocene/welkin-corebut I made one/am working on one (few remaining runtime bugs to iron out)

@theruran @a_breakin_glass @chjara you can definitely use this to prove things, though, that's very important! especially wrt my distributed-systems goals, since I want to have arbitrary user-defined PORDTs that have guaranteed consistency through embedded proofs (among tons of other things)i don't know exactly what like the class of provable things is, but it's definitely a lot of them. should be equivalent to like non-cubical Agda or something

@theruran @a_breakin_glass @chjara @vidak *recent