[Agda] parameters vs indices

[Henning Basold]

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

-------------- 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/d69ab5c5/attachment.sig>