Is there any way to extend a record? { { a = 1 } with b = 2 }
hydraz
@plt-hokusai
Amc.extend_row @"b" 2 {a = 1}
Jonathan Coates
@SquidDev
IIRC with b = 2 works right, just only allows updating rather than extending?
Drew
@CoderPuppy
yeah
hydraz
@plt-hokusai
yes
Drew
@CoderPuppy
Where have you been talking about Amulet now?
hydraz
@plt-hokusai
private slack
maybe we should move it somewhere better but gitter is Uhh
Drew
@CoderPuppy
I don't think Gitter has improved (or changed at all) since Silica was active (late 2017?)
Jonathan Coates
@SquidDev
I've just been connecting over IRC, which makes it usable....
I think GitLab brought it, and then did nothing with it?
hydraz
@plt-hokusai
exactly
maybe we should have an amulet irc
Jonathan Coates
@SquidDev
Because the #urn one went so well :)
hydraz
@plt-hokusai
:p
Drew
@CoderPuppy
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