[Agda] with match changes the result type of a function

[Darryl McAdams]

Yeah, it works fine for me.



$ agda --version
Agda version 2.3.2




Full code that I used was




open import Data.Unit

module Experiment where

data P : ⊤ → Set where
  pt : P tt

test : (t : ⊤) → P t
test t with t
test t | tt = result
  where postulate result : P t

 

- darryl




________________________________
 From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Darryl McAdams <psygnisfive at yahoo.com> 
Cc: Agda List <agda at lists.chalmers.se> 
Sent: Wednesday, March 6, 2013 1:56 PM
Subject: Re: [Agda] with match changes the result type of a function
 
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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130306/62a511ac/attachment-0001.html