Enrico Tassi (Sep 18 2022 at 21:27): Enrico Tassi (Sep 18 2022 at 21:27):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?
Paolo Giarrusso (Sep 18 2022 at 22:34):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.”
Paolo Giarrusso (Sep 18 2022 at 22:38):(but I haven't read McBride's thesis; I'm just trusting what I linked)
James Wood (Sep 18 2022 at 22:47):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.
Kenji Maillard (Sep 19 2022 at 08:04):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).
Matthieu Sozeau (Sep 19 2022 at 08:17):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.
Enrico Tassi (Sep 19 2022 at 08:29):Thanks you all!
Enrico Tassi (Sep 19 2022 at 08:33):I did read Conor's theses when I was a master student... I loved it, but forgot everything ;-)
Enrico Tassi (Sep 19 2022 at 08:33):https://era.ed.ac.uk/bitstream/handle/1842/374/ECS-LFCS-00-419.pdf?sequence=1&isAllowed=y
Enrico Tassi (Sep 19 2022 at 08:33):bottom page 65!
Meven Lennon-Bertrand (Sep 19 2022 at 09:23):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…
Ali Caglayan (Sep 19 2022 at 11:40):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
Ali Caglayan (Sep 19 2022 at 11:41):https://github.com/HoTT/HoTT/blob/master/theories/Types/IWType.v
Ali Caglayan (Sep 19 2022 at 11:42):If indices matter for the equality type then they do generally for indexed inductive types (and vice versa since it is a special case)
Meven Lennon-Bertrand (Sep 19 2022 at 11:55):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?
Ali Caglayan (Sep 19 2022 at 11:56):Yes
Last updated: Jun 01 2023 at 12:01 UTC