I’m struggling to even make things work at the moment; inefficiency would be a nice problem to have, from that perspective ^_^;;
Conversation
Yeah, well... I guess I have ideas how to make it work but that might not work in reality ; _ ;
just hate how positional all the currying and pairing stuff is - as much as it's nice in some cases then stuff lines up properly
1
1
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.
2
1
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'.
Re. substitution, this kind of reminds me of module cloning in WhyML: why3.lri.fr/doc/syntaxref. - but not sure. 🤔
1
Yes, it's the same thing. What is being verified here is that exp by a natural number is definable in any pointed magma, and that binary powering is correct in any monoid.
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.
2
Show replies