I had this weird (probably bad) idea to have records with 'abstract' fields that you could make concrete later - which would end up kind of being like functions? And you'd be able to have a 'default' field that your record would reduce to if all the fields were concrete.
Conversation
Records with abstract fields are kind of like functions. But there would be sugar on top to make it look more familiar. Hoping this might help with the issues around bundled and unbundled modules: alhassy.github.io/next-700-modul - but I dunno.
1
1
[Replying to this whole thread]. Like how you refer to my PhD student's work for the unbundling problem 😆. And yes, contexts should be at least DAGs, not lists. (mutual can involve local cycles too...). Records with abstract fields are quite common in math. 1/
1
2
Think of a concrete vector space (say of dimension 4) over an unknown field. You can also see this as a record definition with some manifest entries (i.e. definitional extensions). The change of perspective can at times be useful. 2/
1
3
In both cases, I think the best view is as a substitution [aka generalized term], mapping from the vector space context to the field that specifies part of it, and the rest is the identity. Yes, this is related to existentials, but where you slice off a whole leading context.
1
2
Oh cool! Didn't know they were your student! Yeah I first noticed the weirdness of bundling with traits in Rust - ie. do I use a type parameter or an associated type? Then in the 1ML paper where they showed that you can do stuff in the 'type class style' or the 'ML style'.
2
You should look at Arend, the theorem prover. It has a beautiful solution to the (un)bundling problem. The bundling problem ought to be regarded as an instance of a false choice - but most systems force it anyways.
1
2
Yeah! I've seen it before, it's pretty cool! Maybe I should re-investigate implementing that for records.
I guess I've been wondering if it's possible to allow some amount of out-of order application/construction, like labelled parameters/records in non-dependent type systems.
I guess there’s a difference between the syntactic appearance of these things and the order of information increase (borrowing from Type Inference in Context &c). If you know a depends on b, then it probably shouldn’t matter which order you write them in so long as you elab right
1
1
Show replies
For those reading, this is Arend's neat anonymous extension feature: arend-lang.github.io/about/arend-fe