Have either of you looked at some of the new fancy type theories? Cubical or Quantitative?
Jonathan Coates
@SquidDev
I know Cubical exists, because the Agda people won't shut up about it. That's about the extend of my knowledge - I know hydraz has done more work on this.
hydraz
@plt-hokusai
i've played with cubical agda and read the hott book
i have a wip qtt checker but it is very wip
Jonathan Coates
@SquidDev
Is QTT the one Idris 2 uses?
Drew
@CoderPuppy
Yep
hydraz
@plt-hokusai
yep
Drew
@CoderPuppy
combining linear and dependent types
Jonathan Coates
@SquidDev
Yeah, I really should have remembered this...
Drew
@CoderPuppy
One thing about it that seems interesting is that I think it allows dropping the parametricity of Π(A : Type).
hydraz
@plt-hokusai
i mean, you can already do that with Typeable
or in a dependently typed language, codes for types
Drew
@CoderPuppy
so it might allow typed tactics (a la VeriML) directly in the language
hydraz
@plt-hokusai
i don't like matching on Type
i think matching is for inductive families only and Type is not an inductive family
Drew
@CoderPuppy
I actually found an oddity with that, Agda doesn't support matching on types but they used to make type constructors injective which is similar they stopped that because someone found a contradiction, but I think that's just because positivity checking wasn't applied to type constructors (because you can't match on them)
Benedict Allen
@exerro
Woah, actually conversation on gitter
InternetUnexplorer
@InternetUnexplorer
Oh hey some activity
I seem to have missed it by a bit, but hello
João Victor
@jv110
hello
João Victor
@jv110
where else can I see you?
Andrew Kvapil
@viluon
Can't wait for the Silica release
@oeed has been working on it for so long, it has to be epic by now