[Agda] Agdas constraint solver too eager?!
James Deikun
james at place.org
Mon Sep 10 03:59:24 CEST 2012
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.
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.
More information about the Agda
mailing list