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
Replying to
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 😵💫
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 }
1
Show replies
Replying to
Ah, I misunderstood you :) This is a totally valid gripe, and named arguments are good + cool and we should have them everywhere
1