[Agda] Display of private things (for higher inductive types)
Guillaume Brunerie
guillaume.brunerie at gmail.com
Mon Aug 13 10:47:33 CEST 2012
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/
More information about the Agda
mailing list