[Agda-dev] One more point for my false-golfing score

[Andreas Abel]

On 01.07.2015 22:58, Ulf Norell wrote:
> I would be all for removing 'abstract'.

Mmh, after all the effort I have put in to make sense of it...

   https://code.google.com/p/agda/issues/list?can=1&q=label%3AAbstract

The standard library does not use abstract a lot, maybe some other of 
Nisse's developments rely on it!?

*Some* mechanism for abstract data types and opaque definitions should 
be there, I guess this is no question.

Cheers,
Andreas


> On Wed, Jul 1, 2015 at 9:40 PM, Andrea Vezzosi <sanzhiyan at gmail.com
> <mailto:sanzhiyan at gmail.com>> wrote:
>
>     What positivity do postulates get?
>
>     On Wed, Jul 1, 2015 at 9:07 PM, Andreas Abel <abela at chalmers.se
>     <mailto:abela at chalmers.se>> wrote:
>      > On 01.07.2015 17:49, Wolfram Kahl wrote:
>      >>
>      >> On Wed, Jul 01, 2015 at 08:21:58AM +0200, Andreas Abel wrote:
>      >>>
>      >>> Subject: [Agda-dev] One more point for my false-golfing score
>      >>>
>      >>> -- https://code.google.com/p/agda/issues/detail?id=1599
>      >>>
>      >>> data ⊥ : Set where
>      >>>
>      >>> abstract
>      >>>
>      >>
>      >> Nice to know that ``abstract'' is not only a premature optimisation,
>      >> but also unsound.
>      >>
>      >> (I used ``abstract'' my early Agda2 days to get more theories
>      >>   trough my memory constraints, but as Agda got better,
>      >>   at some point its advantages essentially disappeared,
>      >>   and its disadvantages made me abandon it,
>      >>   so I am not using ``abstract'' anymore.
>      >> )
>      >
>      >
>      > Thanks for the feedback.  "abstract" lacks a theory, so I am not too
>      > surprised it is unsound.  It also has seen limited use, probably
>     also since
>      > it does not work reliably.
>      >
>      > The API for abstract things is very confusing, I just spend hours
>     trying to
>      > understand what is going on inside of Agda.  Basically, if you
>     ask for
>      > information about an abstract identifier and you are not in
>     abstract mode,
>      > you get the answer that it is a postulate.  That lead to the
>     failure of
>      > positivity checking---there is nothing to check about postulates
>     after all.
>      > The problem was that the abstract mode had not been entered when
>     it came to
>      > check these abstract definitions.
>      >
>      > Here it shows that Agda does not have a safe kernel.  If safety
>     checks like
>      > positivity are omitted by accident of the programmer, Agda
>     happily still
>      > lets you use the (uncertified) definition and prove False in
>     sequence.
>      >
>      > In the long run, such a design is not sustainable.  There will be
>     no end to
>      > exploits.  Without proper double-checking facilities or internal
>      > certificates Agda will never be safe.
>      >
>      >> If you take out the ``abstract'' and the indentation,
>      >> you get a positivity-check error message that sounds like
>      >> it might be ``fixed'' even for continued use of ``abstract''...  ;-(
>      >
>      >
>      > I did not understand what you meant by this.
>      >
>      > Cheers,
>      > Andreas
>      >
>      > --
>      > Andreas Abel  <><      Du bist der geliebte Mensch.
>      >
>      > Department of Computer Science and Engineering
>      > Chalmers and Gothenburg University, Sweden
>      >
>      > andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>      > http://www2.tcs.ifi.lmu.de/~abel/
>      > _______________________________________________
>      > Agda-dev mailing list
>      > Agda-dev at lists.chalmers.se <mailto:Agda-dev at lists.chalmers.se>
>      > https://lists.chalmers.se/mailman/listinfo/agda-dev
>     _______________________________________________
>     Agda-dev mailing list
>     Agda-dev at lists.chalmers.se <mailto:Agda-dev at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda-dev
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/