[Agda] Datatype parameters and indices

[Jan Malakhovski]

Let me rephrase that.

I think you're saying that there is no such thing as polymorphic `P`
because making `A` an implicit argument to a constructor might make it
too big (*).  Instead, for each `A` there is a _distinct_ datatype `P A`.
Each of which has its own constructor `pack`. When I use `pack`,
Agda selects an overloading just as if there was a set of completely
different datatypes with the same constructor name `pack`. The syntax
{A = Nat} is just a hint, not an application.

Sounds reasonable, but I think I'm able to cheat around (*):

~~~~
record ⊤ : Set where
  constructor tt

-- Not universe level polymorphic
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

data NTag : Set where
  packnTag : NTag

NForm : Set → NTag → Set
NForm A packTag = A

N′ : Set → Set
N′ A = Σ NTag (NForm A)
    
packn′ : {A : Set} → A → N′ A
packn′ a = packnTag , a

test1 : N′ ⊤
test1 = (packn′ tt)

test2 : N′ (N′ ⊤)
test2 = packn′ test1
~~~~

`packn′` here has the same type as `packn`, but fits into the type
`N′ : ... → Set`.  As far as I can understand, `test2` shows that the
universe level is not growing with nesting and the question about the
justification for "the type of the constructor does not fit in the sort"
remains. What is the point of this restriction if I can circumvent it?

Correct me if I'm wrong somewhere.

Thanks,
  Jan

P.S. Oops. Sorry for the duplicate, forgot to add the Cc.

On Fri, 25 Jan 2013 18:03:39 +0100
Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> [This is a candidate for a FAQ.]
> 
> That P passes but N not is an artefact of data type declarations.
> 
> Parameters are actually *absent* from constructors, so pack is really
> 
>    pack : ?A -> P ?A
> 
> for ?A to be instantiated according to the context where pack occurs. 
> The syntax
> 
>    pack {A = Nat} zero
> 
> is valid, but the instantiation of parameter of A to Nat should only 
> regarded as a hint to the type checker, and not an actual setting of an 
> argument of pack.
> 
> In contrast, packn actually expects a first argument of type Set, which 
> is too big for type N : ... -> Set, so Agda complains.
> 
> Hope that helps,
> 
> Andreas
> 
> On 25.01.13 12:05 AM, Jan Malakhovski wrote:
> > Hello everyone,
> >
> > A question that doesn't leave me for a while (like a year or so).
> >
> > If I remember right, a dozen of versions ago the following code did type check.
> >
> > ~~~~
> > data P (A : Set) : Set where
> >    pack : A → P A
> >
> > data N : Set → Set where
> >    packn : {A : Set} → A → N A
> > ~~~~
> >
> > Now it complains:
> >
> > ~~~~
> > The type of the constructor does not fit in the sort of the
> > datatype, since Set₁ is not less or equal than Set
> > when checking the constructor packn in the declaration of N
> > ~~~~
> >
> > I can't help but wonder about a justification for this.
> > It is said that parameters transform into constructors' implicit arguments, but the code above makes me think that, strictly speaking, it isn't the case.
> >
> > Best regards,
> >    Jan
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
> -- 
> 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/