[Agda] parameters vs indices

Wed Jul 12 16:07:42 CEST 2017

Hi Thorsten,

Thank you for the clarification! I actually was not aware that this was
already in your indexed container paper. Time to go back and read it
again ;)

Henning

On 12/07/17 15:35, Thorsten Altenkirch wrote:
> 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.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170712/8a26451e/attachment.sig>