[Agda] parameters vs indices

[Andreas Abel]

Hi Thorsten,

I think a semantics could be developed in the direction of how Conor and 
Pierre-Evariste perceive inductive types in

 
https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/journal-2013-catorn-jfp/paper.pdf

In the definition of the inductive type, they case on pattern indices to 
determine which constructors should inhabit that particular slice of the 
inductive family.

Cheers,
Andreas

On 11.07.2017 11: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
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/