[Agda] parameters vs indices

[Henning Basold]

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

-------------- 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/1f618d48/attachment-0001.sig>