[Agda] with match changes the result type of a function
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Mar 6 19:56:56 CET 2013
If I give "result", then I get
t != tt of type ⊤
when checking that the expression result has type P tt
Are you sure it works for you? If yes which system do you have?
Cheers,
Andreas
On 06.03.13 4:43 AM, Darryl McAdams wrote:
> For what it's worth, the problematic code as quoted here type checks for
> me. That is to say, this statement:
>
> "Note that result is not accepted"
>
> is false on my system.
> - darryl
> ------------------------------------------------------------------------
> *From:* Dominique Devriese <dominique.devriese at cs.kuleuven.be>
> *To:* Serge D. Mechveliani <mechvel at botik.ru>
> *Cc:* Agda List <agda at lists.chalmers.se>
> *Sent:* Tuesday, March 5, 2013 11:05 AM
> *Subject:* Re: [Agda] with match changes the result type of a function
>
> Serge,
>
> I've taken a brief look at your code, and I think this is a simplified
> version of your problem:
>
> module test where
>
> data ⊤ : Set where tt : ⊤
>
> data P : ⊤ → Set where
> pt : P tt
>
> test : (t : ⊤) → P t
> test t with t
> test t | tt = {!result!}
> where postulate result : P t
>
> Note that result is not accepted despite the fact that it has exactly
> the declared type of test's result, which I believe is what you are
> seeing in your code as well. The problem is that test's result type
> is changed when you do a with-match on t, by substituting tt for t. A
> solution is to replace your use of with by an explicit helper
> function, where you can tightly control exactly which occurrences of
> the with-scrutinee are replaced by the pattern:
> test₂ : (t : ⊤) → P t
> test₂ t = go t t
> where go : (t : ⊤) → (t' : ⊤) → P t
> go t tt = result
> where postulate result : P t
>
> By the way, in your case, the occurrence of the with-scrutinee in the
> result type of your function is hidden by some calls, but Agda looks
> through this and I believe the problem is the same as what I've
> described above.
>
> Regards
> Dominique
>
>
> 2013/3/5 Serge D. Mechveliani <mechvel at botik.ru <mailto:mechvel at botik.ru>>:
> > On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:
> >> Sorry, I cannot explain this, because I cannot run your example
> >> (incomplete). --Andreas
> >>
> >
> >
> > http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip
> >
> > contains the precise Main.agda and readme.agda
> > (please, read first readme.agda).
> > I am sorry: the proggram is large.
> > I tried to present a small example, but have failed.
> > Of course, it can be reduced, say, 10 times, but this would need a
> > considerable effort.
> > It looks like I am currently stuck in my attempt to write a library.
> >
> > Thank you in advance for help,
> >
> > -------
> > Sergei
> >
> >
> >
> >> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:
> >> >Dear all,
> >> >the attachement t.agda.zip
> >> >
> >> >contains a small code example where the same declaration of kind
> >> > postulate p : <signature>
> >> >is taken in Agda-2.3.2 MAlonzo
> >> >as a correct type for p or not -- depending on whether p is set
> >> >directly after ` = ' or in the last branch for `with'.
> >> >
> >> >Can you, please, explain this?
> >> >
> >> >
> >> >
> >> >_______________________________________________
> >> >Agda mailing list
> >> >Agda at lists.chalmers.se <mailto: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 <mailto:andreas.abel at ifi.lmu.de>
> >> http://www2.tcs.ifi.lmu.de/~abel/
> >>
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> 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