[Agda] parameters vs indices

[Thorsten Altenkirch]

Hi Henning,

I was just observing that this is what you were doing. In this case the
category is the index type of the family hence a discrete category. In
general if we have P : I -> Set, Q : J -> Set, f : I -> J then

	Pi i:I . P i -> Q (f i) = Pi j:J . Lan_f P j -> Q j

where Lan_f P j = Sigma i:I . f i = j x P i is the left Kan extension of P
along f. After some currying you get exactly the constructor form you are
looking for. Indeed we observed a while ago that using left Kan extensions
you can bring constructors in universal form (you can find this in our
paper on indexed containers) but I didn't realize that this was relevant
for our current discussion.


Thorsten

On 12/07/2017, 14:21, "Henning Basold" <henning at basold.eu> wrote:

>Hi Thorsten,
>
>Interesting point! I haven't thought about using Kan extensions here.
>Would you be so kind to briefly hint at the categories and functors
>involved? Or is there even a reference for that?
>
>Another view on this arises by using that dependent coproducts are left
>adjoint to substitutions. This allows one to reduce dependent inductive
>types with indices to initial algebras, see Thm. 4.1 in
>http://dx.doi.org/10.4204/EPTCS.191.3
>
>Cheers,
>Henning
>
>On 12/07/17 14:14, Thorsten Altenkirch wrote:
>> Hi Henning,
>> 
>> this is a good point. What you are doing is using the left Kan extension
>> to reduce indexed datatypes to parametrized ones.
>> 
>> Cheers,
>> Thirsten
>> 
>> On 12/07/2017, 13:18, "Agda on behalf of Henning Basold"
>> <agda-bounces at lists.chalmers.se on behalf of henning at basold.eu> wrote:
>> 
>>> Hi Thorsten,
>>>
>>> Concerning the difference between parameters and indices: there are
>>>none
>>> in the presence of an equality type in the following sense. Note that
>>>in
>>> the case of indices the codomain of a constructor of a dependent
>>> inductive type is given by the type that we are constructing plus a
>>> substitution applied to it. This can equivalently be achieved by using
>>> parameters, equality constraints and identity substitutions. The
>>> All-example becomes then
>>>
>>> data All {a p} {A : Set a} (P : A → Set p) (u : List A) : Set p where
>>>  []  :                                        u = []     → All P u
>>>  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → u = x ∷ xs → All P u
>>>
>>> So even without indices one can still use inductively defined
>>>predicates
>>> over other types and there is no need to resort to large elimination.
>>> Though it is clear that the index-based definition is much nicer to
>>>work
>>> with, since it does not require the elimination of identity proofs.
>>>
>>> I hate to advertise my work, but you may find a description of
>>>inductive
>>> and coinductive dependent types that only uses _indices_ in
>>> http://dx.doi.org/10.4204/EPTCS.191.3 (category theoretical approach)
>>> and in http://dx.doi.org/10.1145/2933575.2934514 (syntactic theory).
>>> Last year at TYPES'16 I also talked about how this can be turned into a
>>> theory, in which the identity is not constructible as an inductive
>>>type,
>>> that is based purely on parameters. This allows the axiomatisation of
>>> the identity type à la observational type theory. To make such a theory
>>> conveniently usable, one would have to provide a front-end that allows
>>> us to still write inductive types like All and translates them into
>>> types with equality constraints, as I showed above. This is, however,
>>> all fairly uncharted territory, yet.
>>>
>>> My apologies for this shameless self-advertisement...
>>>
>>> Cheers,
>>> Henning
>>>
>>> On 11/07/17 12:26, Thorsten Altenkirch wrote:
>>>> Thank you. Now I remember, this actually allows us to write inductive
>>>> definitions when we were only able to write recursive ones due to size
>>>> constraints. The example in your 2nd link shows this nicely:
>>>>
>>>> data All {a p} {A : Set a} (P : A → Set p) : List A → Set p where
>>>> 	[]  : All P []
>>>> 	_∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)
>>>>
>>>> before we were only able to define this by recursion:
>>>>
>>>> All' : ∀ {a p}{A : Set a} (P : A → Set p) → List A → Set p
>>>> All' P [] = Lift ⊤
>>>> All' P (x ∷ xs) = P x × All' P xs
>>>>
>>>>
>>>> which is a bit sad since inductive predicates work often better.
>>>>
>>>> I was wondering about the semantics. One way would be to translate
>>>> forced
>>>> indices into recursive definitions but aybe there is a more direct
>>>>way.
>>>>
>>>> Thorsten
>>>>
>>>>
>>>>
>>>> On 11/07/2017, 12:02, "Roman" <effectfully at gmail.com> wrote:
>>>>
>>>>> Hi.
>>>>>
>>>>>> Why don't we force people to be Honest instead of just being Good?
>>>>>
>>>>> No need to force people when you can force indices:
>>>>>
>>>>> 
>>>>>https://hackage.haskell.org/package/Agda-2.5.2/docs/Agda-TypeChecking-
>>>>>Fo
>>>>> rc
>>>>> ing.html
>>>>>
>>>>> With forcing some things are smaller than without it, see e.g. this
>>>>> issue: https://github.com/agda/agda/issues/1676
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> This message and any attachment are intended solely for the addressee
>>>> and may contain confidential information. If you have received this
>>>> message in error, please send it back to me, and immediately delete
>>>>it.
>>>>
>>>> Please do not use, copy or disclose the information contained in this
>>>> message or in any attachment.  Any views or opinions expressed by the
>>>> author of this email do not necessarily reflect the views of the
>>>> University of Nottingham.
>>>>
>>>> This message has been checked for viruses but the contents of an
>>>> attachment may still contain software viruses which could damage your
>>>> computer system, you are advised to perform your own checks. Email
>>>> communications with the University of Nottingham may be monitored as
>>>> permitted by UK legislation.
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>
>> 
>> 
>> 
>> 
>> 
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please send it back to me, and immediately delete it.
>> 
>> Please do not use, copy or disclose the information contained in this
>> message or in any attachment.  Any views or opinions expressed by the
>> author of this email do not necessarily reflect the views of the
>> University of Nottingham.
>> 
>> This message has been checked for viruses but the contents of an
>> attachment may still contain software viruses which could damage your
>> computer system, you are advised to perform your own checks. Email
>> communications with the University of Nottingham may be monitored as
>> permitted by UK legislation.
>> 
>





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.