[Agda] What is the type of the diagonal function?
Jacques Carette
carette at mcmaster.ca
Thu Apr 25 01:36:23 CEST 2013
On 13-04-24 03:27 PM, Andreas Abel wrote:
> Sorry, I do not see where you are heading, so it is hard to be helpful.
I am trying to model what happens in a meadow, a field-like structure
where 1/0 is defined to be 0, along with the (total) axioms 1/(1/x) == x
and x*(x*1/x) == x. These axioms are understood to have computational
content, so are modelled as combinators [one for each direction of an
equality].
x*(x*1/x) == x is non-linear, unlike other axioms (like commutativity,
i.e. x*y = y*x) where each variable only occurs once on each side. So
in using the combinator which transforms x*(x*1/x) needs to know that
the same x occurs 3 times in the rhs. This is of course trivial to do
at the term level with a conditional. The aim is to do this at the type
level.
In other words, I want my combinator foo which transforms x*(x*1/x) into
x to only be applicable to values which are exactly of that kind [you
can model * and 1/ completely formally, as syntax for the purposes of
this problem, although that is not what I am doing].
It is ok to assume that x belongs in an enumerable type with decidable
equality, if that helps.
>
> [...] but frankly, I do not see the point of a singleton type, since
> it does not bear any more information than the unit type. If you want
> to store a y that is equal to x, why don't you take x right away?
Because I want to generate things like x*(x*1/x), then treat the result
as a "general product", and have the values drift apart from each
other. Then I will want to later have these values "come back
together", and use the eliminator. Which should not type if it is not
statically apparent that these are exactly x*(x*1/x).
[If it helps, this is related to one way of looking at the eta/epsilon
operators for a traced monoidal category].
Jacques
More information about the Agda
mailing list