[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

On 10.09.12 3:59 AM, James Deikun wrote:
> On Sun, 2012-09-09 at 21:49 +0200, Andreas Abel wrote:
>> On 09.09.12 6:55 AM, James Deikun wrote:
>>> On Fri, 2012-09-07 at 15:13 +0200, Andreas Abel wrote:
>>>> A consequence of making Agda aware of unused arguments is that certain
>>>> "phantom-type" tricks do not work anymore.
>>>>
>>>>      data D (phantom : Nat) : Set where
>>>>        c : D phantom
>>>>
>>>> If Agda may recognize 'phantom' as unused, then
>>>>
>>>>      D 0 = D 1
>>>>
>>>> and accordingly, D X = D 0 will not solve X to 0.
>>>
>>> Is this entirely true to begin with?  What will happen if you have:
>>>
>>>     f : {phantom : Nat} -> D phantom -> Nat
>>>     f (c {phantom}) = phantom
>>>
>>> Do you plan to have the data constructor lose injectivity along with the
>>> type constructor?  I suppose it probably would not be incoherent to do
>>> so (treating a data constructor as a constructor, properly speaking,
>>> only once the parameters are saturated), but it would seem an unusual
>>> choice...
>>
>> Mmh, good question.
>>
>> But actually, it might not be an issue, since your code seems to be
>> illegal already; my Agda rejects it, stating that c should have 0
>> arguments but has been given 1.
>
> Wow, it turns out the way Agda represents datatype constructors is
> considerably different than how I thought.  In particular, a constructor
> for a parametric datatype *does not have* a particular type, only a type
> scheme like `c : D _1' and therefore does not need an implicit argument
> to supply the type parameter; this is resolved as overloading instead.

Yes, and the philosophy behind it is bidirectional type-checking. 
Constructors are like lambda-functions, they do not inherently carry 
their unique type, but they are assigned a type.

> Thanks to that it turns out we can do this amusing thing:
>
>      Nz : Nat -> Set
>      Nz zero = Bot
>      Nz (suc n) = Top
>
>      data Phin (bound : Nat) : Set where
>        zero : {nz : Nz bound} -> Phin bound
>        suc : {nz : Nz bound} -> Phin (pred bound) -> Phin bound
>
>      toPhin : (n : Nat) -> Phin (suc n)
>      toPhin zero = zero
>      toPhin (suc n) = suc (toPhin n)
>
> If you then normalize toPhin 20 (say) with hidden argument printing
> turned on, you will observe that there are no numbers hidden into the
> result, only `tt's.  This reduces the size of a normalized Phin in
> memory by a logarithmic factor relative to a Fin.  (Without builtin
> optimization of Nats, this would be a linear factor.)  All because a
> constructor doesn't take arguments for type parameters.

I had expected of the Epic backend to compile Phin.suc as just Nat.suc, 
but it seems that it cannot see that elements of Nz n do not carry 
information and could be discarded altogether.

But if it did, Phin would be represented efficiently at runtime as 
integers, and toPhin as the identity.

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/