[Agda] Datatype parameters and indices

[Andreas Abel]

Hi Jan & list,

On 27.01.13 12:06 AM, Jan Malakhovski wrote:
> Aha, thank you! Exactly the type of answer I was looking for.  Your
> `Bad` example sheds a light on the nature of parameter/index
> distinction in Agda and, that's even more valuable for me, on the
> nature of type parameters in MLTT by itself.

Great!

> As for `packp`, I guess I could, but I was chained by ΠΣ thinking :)
>
> By the way, is it critical to have `Bad : Set -> Set` and not
> `Bad : Set`? I think the latter should suffice and `Set → Set` is
> rejected by Agda for another reason already.

Ah, of course, my bad.  It should be a 'Set'.

> P.S. I think it would be nice to share your answer with the rest of the
> mailing list. If you are going to forward it, feel free to forward (or
> remove) my comments as well.

It was early morning, so I must have accidentially missed the 'Reply 
all' button.

To spread the results of the discussion, could you imagine to summarize 
it and integrate it into the Wiki page?

   http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Data

This would be greatly appreciated!!

Cheers,
Andreas

> On Sat, 26 Jan 2013 08:09:17 +0100
> Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
>> Could you have made your point also by just defining
>>
>>     packp : {A : Set} -> A -> P A
>>     packp {A} a = pack {A = A} a
>>
>> ?  Of course, you can have a constructor-like thing that has the type of
>> packn.
>>
>> That N is rejected is an artefact of the parameter/index separation by
>> telescope and function type.  What we really want to rule out is
>>
>>     data Bad : Set -> Set where
>>       packb : {A : Set} -> A -> Bad
>>
>> because that really must store type A, it is what you call an
>> existential type in Haskell.  [This is really bad, because Bad is
>> isomorophic to the inhabited sets, and bad is a sets itself, so you have
>> Set:Set and Hurken's paradox.]
>>
>> In
>>
>>     data N : Set -> Set where
>>       packn : {A : Set} -> A -> N A
>>
>> the type A does not have to be stored in the constructor, since it is
>> determined by the context in which a value of type N A is used.  So,
>> really A is a parameter here and not an index.  But Agda does not do
>> this smart analysis.  It just treats A as an index because it is
>> quantified over in the constructor and not in the data telescope.
>>
>> More background on why parameters are not stored in constructors can
>> maybe found in Edwin Brady's work
>>
>>     "Inductive families need not store their indices".
>>
>> In Idris, both P and N would just be written as
>>
>>     data P : Set -> Set where
>>       pack : A -> P A
>>
>> and the analysis that A is a parameter is done automatically.  That is
>> an idea we should port to Agda; it would avoid confusion about
>> parameters and indices...
>>
>> Cheers,
>> Andreas
>>
>> On 26.01.13 12:51 AM, Jan Malakhovski wrote:
>>> 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
>>>
>>> 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


-- 
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/