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

[Andrea Vezzosi]

abstract is also still pretty useful for performance in case you need
to hide some big term from the conversion checker.

On Fri, Jul 3, 2015 at 10:52 AM, Andreas Abel <abela at chalmers.se> wrote:
> 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/