[Agda] What is the type of the diagonal function?

[Andreas Abel]

Sorry, I do not see where you are heading, so it is hard to be helpful.

On 24.04.13 6:05 PM, Jacques Carette wrote:
> The naive version of diagonal, i.e.
> diag x = x , x
> has the 'obvious' type. But this is rather unsatisfactory because it
> loses all dependency information. So one idea is to use
>
> data <_> {a : Level} {A : Set a} (x : A) : Set a where
>      singleton : (y : A) → y ≡ x -> < x >

Why not just

        singleton : < x >

If you have y : A and p : y == x, you can still get < x >

   subst <_> p singleton : < x >

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?

> and then do
> diag x = x , singleton x refl

   diag x = x , singleton

> so that diag now has a very precise type [and good computational
> properties]. But this is not quite satisfactory either.
>
> Has anyone looked into creating a "diagonal" function with a precise
> type? Eventually, I want to be able to pattern-match on this, to enforce
> that my 'input' can only be such a dependent pair. [Actually, it gets a
> little trickier still, but this is the first interesting stumbling block].

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/