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
Replying to
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.
Replying to
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
Show replies