[Agda] problem with `abstract'

[Sergei Meshveliani]

On Sun, 2016-07-17 at 12:51 +0200, Andreas Abel wrote:
> Thanks, I filed it as
> 
>    https://github.com/agda/agda/issues/2101
> 
> Currently,
> 
> (1) abstract definitions are abstract in type signatures always, and
> 
> (2) local definitions in an abstract definition are abstract as well.
> 
> Together this means, that Agda cannot see in the type signatures of 
> seconds>0[] and g that Pair is a product type.
> 

I doubt of whether I understand the rule. The program

  abstract
    h : ℕ → ℕ
    h n = s a
        where
        a : ℕ
        a = 0

   	s : ℕ → ℕ
       	s 0 = 0
       	s _ = 1

is type-checked, despite that `a' has a local definition.
(?)


> However, I think something is wrong with the current treatment of 
> abstract in where blocks.
> 
> Either, `abstract` should not be propagated to where blocks 
> automatically (the user can then decide which parts of the where block 
> should be abstract).
> 
> Or, `where` blocks should get a special status (IgnoreAbstractMode).
> 

Call the first solution (I), the second -- (II).

Suppose that you choose (II).
Then  
a) the below program for  f  will be correct, 
b) in other modules any call for  f  will be type-checked as abstract 
   (without looking into the implementation of f).

Will this be so?

And what about the scheme

    G x =  g (h x)
           where
           h1 : ...
           ...
           
           abstract 
             h2 : ...
             h2 = ...

           h : ...
           ...
           g : ...
?

I write this when abstracting the whole  G  leads to that some of its
calls are not type-checked, for some reason. Then, I abstract its part
-- a large piece of a proof implemented by  h2. 
And I hope that in type-checking any call of  G,  the implementation of
h2  will not be considered, so that the type check will be cheaper
(I do not know of whether this works).

What it will be with  G  under (I) and under (II) ?

Regards,

------
Sergei
 


> On 17.07.2016 11:28, Sergei Meshveliani wrote:
> > On Sat, 2016-07-16 at 23:55 +0200, Andreas Abel wrote:
> >> Sorry, I cannot see off-hand where the problem is.  Please provide
> >> some self-contained test (does not have to be minimal for now).
> >>
> >
> > -----------------------------------------------------------------
> > open import Data.Product  using (_×_; proj₂)
> > open import Data.List     using (List; []; map)
> > open import Data.List.All using (All) renaming ([] to []a)
> > open import Data.Nat      using (ℕ; _<_)
> >
> > abstract
> >   f :  (A : Set) → A → ℕ
> >   f A a =  g nil seconds>0[]
> >     where
> >     Pair : Set
> >     Pair = A × ℕ
> >
> >     nil : List Pair
> >     nil = []
> >
> >     seconds>0[] :  All (_<_ 0) (map proj₂ nil)
> >     seconds>0[] =  []a
> >
> >     g :  (pairs : List Pair) → All (_<_ 0) (map proj₂ pairs) → ℕ
> >     g _ _  =  0
> > --------------------------------------------------------------------
> >
> > Agda 2.5.1.1 reports
> >
> > home/mechvel/agda/tosave/bugs/july15-2016/Last.agda:16,42-45
> > Pair !=< (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))
> > of type Set
> > when checking that the expression nil has type
> > List (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))
> >
> > With removed `abstract', it is type-checked.
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
>