Conversation

Jacques Carette
@jjcarett2
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
Jacques Carette
@jjcarett2
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
Brendan Zabarauskas
@brendanzab
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
Jacques Carette
@jjcarett2
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
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
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
Rob Rix‎
@rob_rix
but I think that works out most neatly when you can guarantee fully saturated application. partial application leaves things in a much more complicated state.
1
1
Rob Rix‎
@rob_rix
e.g. in Σ n : Nat . Fin n, if you could “partially apply” it to the Fin n parameter then I think the only sensible options are: - derive n from Fin n - require it to be completely polymorphic in n; i.e. Π n : Nat . Fin n both seem not generally possible for arbitrary type cons.
1
Rob Rix‎
@rob_rix
in particular I think we can do the former for Fin but not the latter; and if the constructed type loses information (e.g. if odd n then Bool else String) you might be able to do the latter but not the former? does that hold water?
1