[Agda] Display of private things (for higher inductive types)

[Guillaume Brunerie]

Yes, something like an "protected abstract" would be useful.

By the way, I noticed that there is a part in the wiki about my exact
problem, here:

http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Modules#private

It is said that it’s in general very hard to know how to display the
normal form of a term involving private definitions.
But I’m not sure I understand why, what about reducing the term as
long a no private definition appear and decide that the normal form to
be displayed is the last one not involving a private definition?

Cheers,
Guillaume

Le 26 juillet 2012, Andreas Abel <andreas.abel at ifi.lmu.de> a écrit :
> If I understand you correctly, you want to disallow matching on #I with the
> exception that I-rec is allowed.
>
> It seems that you need something like a concept of abstract tied to a
> module, such that only functions within the module can see through the
> definitions, but not those on the outside.  Something like "protected" in
> Java.
>
> Interesting.  Seems like a useful concept.
>
> Cheers,
> Andreas
>
>
> On 26.07.2012 16:07, Guillaume Brunerie wrote:
>>
>> Hello,
>>
>> As some of you know, the following trick is used in homotopy type theory
>> to have reduction rules for higher inductive types:
>>
>>  > private
>>  >   data #I : Set where
>>  >     #0 : #I
>>  >     #1 : #I
>>  >
>>  > I : Set
>>  > I = #I
>>  >
>>  > 0 : I
>>  > 0 = #0
>>  >
>>  > 1 : I
>>  > 1 = #1
>>  >
>>  > postulate
>>  >   seg : Id 0 1
>>  >
>>  > I-rec : (P : I -> Set) (x0 : P 0) (x1 : P 1) (p : Id (transport P seg
>> x0) x1) -> ((x : I) -> P x)
>>  > I-rec P x0 x1 p #0 = x0
>>  > I-rec P x0 x1 p #1 = x1
>>  >
>>  > -- + propositional reduction rules for [seg]
>>
>> The point is that the reduction
>>  > I-rec P x0 x1 p 0  -->  x0
>> is definitional.
>>
>> Now my problem is that when using C-c C-t or even C-c C-a in a goal
>> involving these definitions, "I" is reduced to something ugly (and not
>> even syntactically correct) like ".Interval.#I", and with more
>> complicated HIT this is sometimes very annoying (and with HIT with
>> parameters there is another problem, but I don't remember what it is
>> right now)
>>
>> Is there a workaround for that? Ideally the terms "I", "0" and "1"
>> should never be reduced.
>>
>> I tried to declare "I" abstract, but obviously the pattern matching
>> defining I-rec does not work anymore.
>>
>> Thanks,
>>
>> Guillaume
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/