Tweetovi
- Tweetovi, trenutna stranica.
- Tweetovi i odgovori
Blokirali ste korisnika/cu @andrasKovacs6
Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @andrasKovacs6
-
Did some benchmarking: https://github.com/AndrasKovacs/normalization-bench … Preliminary takeaway is that modern JIT platforms suck at lambda calculus.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
IMO, a nice observation in this paper is that we can specify QIITs/GATs without ever touching nasty raw syntax.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Posted some references on type theory implementation:https://math.stackexchange.com/questions/3466976/online-reference-book-for-implementing-concepts-in-type-theory …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
I have an Agda file containing some large countable ordinals and a big number: https://gist.github.com/AndrasKovacs/8d445c8457ea0967e807c726b2ce5a3a … Motivated by https://github.com/codyroux/name-the-biggest-number …, but now my number is so large it would be a major challenge to prove statements about its size.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
I previously thought that proving impredicativity consistent requires meta-level impredicativity.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
TIL from Dan Doel that vanilla predicative MLTT can prove impredicative System F consistent. https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/SystemFBooleanModel/BooleanModel.agda#L106 … Original discussion:https://math.stackexchange.com/questions/3402806/recursive-types-for-free-but-doesnt-this-contradict-the-fact-that-mathb …
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
I have a nice and general solution for the notorious "impredicative polymorphic" type inference problem, in a dependently typed setting.https://github.com/AndrasKovacs/elaboration-zoo/tree/master/experimental/poly-instantiation …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The trick is basically building binary trees from natural numbers, and after that it's pretty easy to represent other finitely branching trees.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Fun thing: it seems that all finitary inductive types are constructible from Pi, Sigma, universes, identity and natural numbers. No quotients or W-types needed. UIP/funext perhaps needed for some types but not for others.https://gist.github.com/AndrasKovacs/1f57b66108e7d61351d3a61a642ef066 …
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The answer which I've found is: if we add extensional equality to Jon Sterling's cumulative algebraic TT, internal cumulative subtyping is derivable. This seems to be the nicest formalization.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
This can be used (tedious, didn't formalize, but obviously works) to model Jon Sterling's cumulative algebraic TT. https://arxiv.org/abs/1902.08848
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Transfinite cumulative Russell-style inductive-recursive universes in Agda:https://gist.github.com/AndrasKovacs/092fb6075d3f32a16bf9608c070e71f6 …
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
"Propositional subtyping" would behave the same as extensional prop. equality. I.e., from a term proving propositional subtying, I get judgmental subtyping by "subtyping reflection".
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Question to twitter. Cumulative universes induce subtyping in Coq: https://subs.emis.de/LIPIcs/volltexte/2018/9199/pdf/LIPIcs-FSCD-2018-29_.pdf … I'm using this kind of cumulativity informally, but want to internally *prove* subtyping between some complicated types. Is there prior art for this "propositional" subtyping?
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
András Kovács proslijedio/la je Tweet
This will be fun. Anyone want to come and hack on Idris with me? https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1 …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
I'm at ZuriHac now, is there anyone who wants to chat?
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
He's going to give an invited talk about generalized sketches next week at our type theory club, I'm pretty excited about it.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
We belatedly found out last week at our university, that in fact Makkai has been teaching categorical logic for the whole past semester at the philosophy institute (!).
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Our shallow embedding is generally very helpful, but for purely syntactic translations it's absolutely killin it. I'm excited about what we could formalize, maybe I'll revisit my stuff on closure conversion for dependent types.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.