In some cases one can rephrase an indexed data type as a non-indexed one by adding parameters and equations which carry the same information. I can't find a reference for it. My memory says McBride, but I can't find it.
Anyone?
I remembered McBride calls it fording — that led me to https://hal.archives-ouvertes.fr/hal-02896776v5/document attributing it to McBride's thesis (https://era.ed.ac.uk/bitstream/handle/1842/374/ECS-LFCS-00-419.pdf) (where the actual word doesn't seem to appear):
Footnote 24: This technique has reportedly been coined “fording” by McBride [1999, §3.5]. Fording is in allusion to the Henry Ford
quote “Any customer can have a car painted any color that he wants, so long as it is black.”
(but I haven't read McBride's thesis; I'm just trusting what I linked)
As I understand it, in Conor's thesis/OLEG all indices are handled in what we would call the “Henry Ford” style, in that dependent pattern matching happens by generating loads of equations, using unification to solve most of them, and giving the user back propositional equations for anything tricky. The distinction we would make between indices and parameters-with-equations in Coq when defining an Inductive
instead happens at each elimination. That might explain why it's hard to find a firm reference, though indeed orally Conor often talks about “Henry Fording” in the context of Agda, where it means the same as in Coq.
I expect that any indexed datatype should be encodable using parameters + equalities. One tricky thing however is that the indices might need to be packed into a single telescope/iterated dependent sum when there are dependencies between indices. I don't think I know any reference showing that the encoding is intensionally doing what we want though -- In the sense that the encoding should be defined over some general schema for describing indexed inductive types and the original indexed inductive type and the encoded one should be at least equivalent (in HoTT sense).
I think the equivalence holds except for the universe levels of the two inductives (or you work in --indices-matter mode and then it should be the same). I thought Jasper Hugunin had proven more formally the equivalence but can't find it anymore.
Thanks you all!
I did read Conor's theses when I was a master student... I loved it, but forgot everything ;-)
https://era.ed.ac.uk/bitstream/handle/1842/374/ECS-LFCS-00-419.pdf?sequence=1&isAllowed=y
bottom page 65!
Matthieu Sozeau said:
I think the equivalence holds except for the universe levels of the two inductives (or you work in --indices-matter mode and then it should be the same). I thought Jasper Hugunin had proven more formally the equivalence but can't find it anymore.
The best reference I know of is called "Why not W?", indeed by Jesper Hugunin, in Types '20 post-proceedings. But it’s quite terse…
Matthieu Sozeau said:
I think the equivalence holds except for the universe levels of the two inductives (or you work in --indices-matter mode and then it should be the same). I thought Jasper Hugunin had proven more formally the equivalence but can't find it anymore.
It's in the HoTT library now
https://github.com/HoTT/HoTT/blob/master/theories/Types/IWType.v
If indices matter for the equality type then they do generally for indexed inductive types (and vice versa since it is a special case)
Ali Caglayan said:
It's in the HoTT library now
Nice! If I understand correctly, line 105 shows that the behaviour is _definitionally_ the intended one, right?
Yes
Last updated: Dec 05 2023 at 05:01 UTC