I’m not sure how you mean this. With inductives types, i can implement several notions of identity type, but if I’m forced to have primitives, then im limited by the language implementer’s foresight.
Conversation
You should not be able to implement any of the usual identity types inductively. They *force* the identity type to coincide with the disappointing accident that is definitional equality. Designers should factor equality out, so that equality can be *chosen*, not *imposed*.
2
1
7
It's strange to me that you say "you should not be able to". I get why you might not want such limited identity, but you think it should be forbidden or inexpressible?
1
It queers the pitch for other choices. Once you've nailed the identity type to definitional equality, there's no way back. It's a failure to separate usefully separable concerns.
2
1
I'm not thinking "it is expressible instead of something better", but "it is expressible because the system is expressive". Why not a better identity but also a notion of inductive type expressive enough to express a worse one?
2
Because the less picky identity type is not substitutive with respect to the more picky identity type, thus ceases to *be* the identity type.
2
I don't really want it to be (my concern is not really with the identity type). I'm more curious how you limit expressivity enough to rule out encoding an identity type, without harming expressivity.
3
2
If you have an identity type already, you don't "lose" anything in your inductive types thanks to "Fording" (a technique I've seen a lot but never heard called that until two days ago)
3
2
I'm not worried about that, I'm curious how you rule out exactly the identity type, and no other useful types.
2
3
The thing you ban that rules out an inductive identity type is using definitional equality between indices. If you can demand identity evidence (fording) you can recover something just as good that isn't overly intensional.
2
4
Do you have an example or reference to 'fording' that I can look at to learn more?
Aside from Conor's thesis (linked elsewhere)?
The technique itself is tweetable. Get rid of ambient definitional equalities and use identity instead:
data isZero : Nat -> Set where
isZ : isZero 0
becomes:
data isZero (n : Nat) : Set where
isZ : n ≡ 0 -> isZero n
1
2
This is a good example of unnecessary fording. You could have
data isZero 0 = isZ
| isZero (S n).
Now, that inverse image example: classic.
3
The joke about "Henry Ford equations" first appears in print in my thesis, although I'm sure I was telling it in 1998. It is rather more recent that the noun has been verbed, as a thing that you do to an inductive family to simplify the return indices of constructors.
3