Just gave finished giving my #WITS22 talk about Records, Singleton Types, and Bundled + Unbundled structures. Slides are available here for those who are curious:
cofree.coffee/~totbwf/slides
Conversation
This is so cool 🥰 – I want to implement it sometime!
It's cool that you now have a form of labelled arguments too.
Is still feel a bit disturbed by the asymmetry between function and records though, but maybe I'm just a weirdo.
1
2
You can do it with curried families too, it's just a bit easier to work with the uncurried ones!
1
I guess what I mean is that we have records with labels, but not functions with labels. Like maybe it would be silly but I sometimes imagine something like:
f : { a : A, b : B -> c : C, d : D }
but yeah ofc I have no idea what I'm talking about 😵💫
2
1
Kind of like you have an input DAG and an output DAG, with labelled nodes
1
1
One thing I've idly pondered is how fields are ‘filled up’:
f : { a : A, b : B -> c : C, d : D }
thing : A
f.{a := thing} : {b : B -> a : A := thing, c : C, d : D }
f.{a := thing} : {b : B -> a : A, c : C, d : D }
f.{a := thing} : {b : B -> c : C, d : D }
This probably breaks a bunch of stuff I don't really understand though so idk. But yeah I find it interesting how things sort of go from ‘abstract’ to ‘concrete’. But maybe you could also have:
f.{a := thing} : { a : A := thing, b : B -> c : C, d : D }
1
But that might not be useful at all. And yeah this stuff could also be horrendous to use in practice so idk. Also IIUC singletons are weird too without cubical?