New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A "safe" subsection of the library #143

Closed
MatthewDaggitt opened this Issue Jun 27, 2017 · 36 comments

Comments

Projects
9 participants
@MatthewDaggitt
Contributor

MatthewDaggitt commented Jun 27, 2017

As discussed in #122 it is currently impossible to typecheck a development relying on the standard library with the --safe option because it does not isolate properly its uses of unsafe features.

The agreed upon course of action is that there will be a Safe.* subset of modules. The current module names will be kept the same and will re-export exactly what they currently contain, ensuring full backwards compatibility whilst making it possible to only rely on the subset that is recognised as being safe by Agda.

@gallais

This comment has been minimized.

Member

gallais commented Aug 1, 2017

I have come across something fairly nasty: Agda.Builtin.Int depends upon Agda.Builtin.String which uses a postulate to declare the String type. As a consequence any module importing Agda.Builtin.Int cannot be accepted by the current --safe option Agda has.

In other words either all Data.Integer.* and any other module depending upon them have to be in the unsafe part of the library or Agda needs to provide e.g. Safe.Agda.Builtin.Int without primShowInteger (and therefore without any dependence on Agda.Builtin.String).

gallais added a commit that referenced this issue Aug 1, 2017

[ re #143 ] First Attempt at a safe subsection
This should all be ok. The next step is to make sure that the tests
run by travis enforce the fact that all the modules in Safe/ are
compatible with --safe.

Rather than writing a crude sed script like I've done locally,
I should probably reuse the ideas in GenerateEverything.hs
@UlfNorell

This comment has been minimized.

Member

UlfNorell commented Aug 2, 2017

It sounds like maybe we should relax the requirements of --safe to accept postulates of type Set.

@gallais

This comment has been minimized.

Member

gallais commented Aug 2, 2017

I don't understand why Agda.Primitive doesn't trigger an error given that it does use postulate all over the place.

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

All the tests are green. I think the branch is more or less ready to be merged (and I'd like to avoid it diverging too much from master before merge because that's a lot of changes to maintain!). When / If Agda gets more liberal in terms of what it accepts as safe, we can move more things into Safe/. It should all be transparent from the users' point of view anyway.

The main issues I see are:

Wider Use

Do we want to ask people on the agda ML to try to check their developments with the current safe branch to make sure it doesn't break anything (e.g. we haven't forgotten to re-export any names anywhere)?

Or would it be enough to run Agda's stdlib-based test suite on the modified one? In which case I guess it's simply a matter of creating a dummy branch on agda/agda where we update the submodule to point to the safe branch.

Stylistic Issue

Do we want {-# OPTIONS --safe #-} as a header in all of the Safe/ modules or are we just happy with having travis check Safe/index.agda with the appropriate command line options? At the moment we have both the header and the travis separate check (the latter is necessary even though we have the headers because of agda/agda#2487).

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

Just had a look at the branch. What's the plan for maintaining this? Is every safe change to the non-safe part going to have to be copied over to the safe part manually?

Or is there some way of regenerating the safe part automatically?

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

The idea is to replace master with safe. Given that each unsafe module re-exports the content of its safe counterpart, it should be completely transparent for end users.

New definitions can be added either to the safe module if they are innocuous, or to the unsafe one if they're not. Data.Nat.Base is a pretty good example: pretty much all of its former content is now in Safe.Data.Nat.Base except for erase which is in Data.Nat.Base.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

Oh yes. Apologies, hadn't noticed that all the non-safe versions contents had been moved.

Given that each unsafe module re-exports the content of its safe counterpart, it should be completely transparent for end users.

Until they go browsing through it!

I'm a little worried about what this is going to do to library usability. For instance looking for the decidability of the divides relation _∣_, would currently only involve looking through Data.Nat.Divisibility. However it is now going to require browsing both Safe.Data.Nat.Divisibility and Data.Nat.Divisibility which are deep in different parts of the heirarchy. What's more you can't off-hand predict which one it's going to belong to.

This seems like a big impact on the average user who's not that concerned about rigorous safety. Can users who are concerned about safety not just type-check it on the command line using the --safe option? Won't that automatically highlight the unsafe terms used? Or does it over-estimate, and mark otherwise safe terms unsafe if they share a file with unsafe terms?

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

However it is now going to require browsing both Safe.Data.Nat.Divisibility and Data.Nat.Divisibility which are deep in different parts of the heirarchy. What's more you can't off-hand predict which one it's going to belong to.

The doc for the unsafe module systematically links to the safe one because it imports it.

Can users who are concerned about safety not just type-check it on the command line using the --safe option?

--safe only succeeds if all of the definitions in a module (and all the module it depends upon) are safe. Hence the need for a split: it is currently near impossible to typecheck a development relying on the standard library with the --safe option. I'm actually surprised that after 100+ articles using Agda published, no reviewer seems to have complained about this.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

The doc for the unsafe module systematically links to the safe one because it imports it.

Hmm... I guess so.

--safe only succeeds if all of the definitions in a module (and all the module it depends upon) are safe.

Whereas what it should ideally do is only check the definitions in other modules that are actually used. From my position of complete ignorance, this seems like it should be doable using some sort of flow analysis. I'm not sure if it is or not! If it is possible, wouldn't this be a far better solution than partitioning the standard library in two?

I guess its kind of the dual to agda/agda#2487. File options should be more strict with respect to imported definitions, and command line options need to be less strict....

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

Whereas what it should ideally do is only check the definitions in other modules that are actually used.

But then you'd have to call agda --safe on every single module attached to a paper to make sure the whole development is not using any dirty tricks. Right now you can simply generate an Everything.agda and typecheck that.

Edit: I should perhaps mention the existence of C-c C-z to search through definitions in scope. Which ought to be more efficient than navigating files when looking for a specific result.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

But then you'd have to call agda --safe on every single module attached to a paper to make sure the whole development is not using any dirty tricks

Aren't you going to have to do that anyway? Even if you've only used modules from the Safe hierarchy in the standard library, you still need to check that your own modules don't use any dirty tricks.

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

You can call agda --safe on a module Everything.agda importing all the modules in your development and it'll make sure everything is a-ok. Just like the travis test at the moment checks the whole of Safe/ simply by checking Safe/index.agda.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

Oh okay, that makes sense. Thank you for your patience and taking the time to explain it to me! I have experience with exactly one agda development and that's my own so I'm not fully versed in all the tricks...

Okay then perhaps there should be a --safe-narrow and --safe-broad option to cover both options. It just seems weird that a module that only uses safe definitions should be labelled as unsafe just because some of its dependencies happen to share a file with unsafe definitions. In fact the same thing should probably apply to other options like --without-k.

@gallais

This comment has been minimized.

Member

gallais commented Aug 3, 2017

Okay then perhaps there should be a --safe-narrow and --safe-broad option to cover both options

Won't the problem still be the same? You'll want --safe-narrow on all of the modules corresponding to a paper (ALL of the theorems have to be valid) but if it relies on the standard library, you'll need that constraint to magically change to --safe-broad whenever definitions rely upon that dependency.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 3, 2017

I have to confess I was imagining a scenario where issue agda/agda#2487 was fixed as well. Then it'll suffice to simply have the --safe-broad pragma at the top of each of your top level theorem files.

@fredrikNordvallForsberg

This comment has been minimized.

Member

fredrikNordvallForsberg commented Aug 6, 2017

I don't understand why Agda.Primitive doesn't trigger an error given that it does use postulate all over the place.

Perhaps more of a side remark, but this is because safe mode is explicitly turned off when Agda.Primitive is typechecked.

@jespercockx

This comment has been minimized.

Contributor

jespercockx commented Aug 7, 2017

Whereas what it should ideally do is only check the definitions in other modules that are actually used. From my position of complete ignorance, this seems like it should be doable using some sort of flow analysis. I'm not sure if it is or not! If it is possible, wouldn't this be a far better solution than partitioning the standard library in two?

Maybe it would make sense if Agda internally marks definitions that could have been checked with --safe as such, even if the flag is not enabled. That way, when importing a file without --safe, Agda can check for the definitions you actually use whether they are safe. Although this would probably require quite some refactoring of the other flags that are excluded by --safe.

@nad

This comment has been minimized.

Contributor

nad commented Oct 5, 2017

The agreed upon course of action is that there will be a Safe.* subset of modules.

I think I'd prefer M.Safe to Safe.M: In my opinion the word Safe is more noisy at the start than at the end. Furthermore M and M.Safe are close to each other, both alphabetically and in terms of the directory hierarchy.

@HuStmpHrrr

This comment has been minimized.

Contributor

HuStmpHrrr commented Mar 23, 2018

Hi people, I came around here from another similar issue #255. Pretty much the same request, though I don't get why the basic assumption is the language is unsafe? I'd prefer the other way since all definitions should come safe in the first place (except those unsafe by definition), and only after then we have unsafe stuff around the beautiful utopia?

@HuStmpHrrr

This comment has been minimized.

Contributor

HuStmpHrrr commented Mar 24, 2018

Hi people,

Let me put more stuff to emphasize my point. I think from engineering's perspective, we don't want to reinvent too much conventions, provided that there are ones working already.

One argument I am going to make is, it's largely convenient, if Agda can follow as much as conventions from Haskell as possible. It brings at least two advantages:

  1. It gets Haskell users much easier to follow what's going on on Agda's side;
  2. Things from Haskell tend to be long established. For those with little controversy, it would just save lots of time by not having to think about an alternative resolution. Though for those controversial, we can definitely pick and choose.

For this particular problem, packages from Haskell always put Unsafe at the end of the modules. e.g.

https://hackage.haskell.org/package/base-4.11.0.0
https://hackage.haskell.org/package/containers-0.5.9.1

One may also notice, that, for packages in Haskell, it has been a convention to put properties at the end of the modules, inlcuding .Unsafe, .Strict, .Lazy. All these make perfect sense, for again two reasons,

  1. M.Strict says that it's the strict version of M, while Strict.M is a bit hard to interpret. Same argument for .Unsafe, or any others;
  2. M.Unsafe style also helps when an auto-completion plugin is working property, which is a standard tool that hints regular uses to learn most about the libraries, whilst Unsafe.M is arguably absurd.

On the side whether we want to address .Safe or .Unsafe, I would argue for the latter. It's important that dependent type programming is built on top of complete safety. Therefore the language should itself be safely guarded. Then being practical comes afterwards. Arguably, with all those constraints like strict positivity, termination checking, it will be extremely frustrating, if one later discovers the implementation is unsafe caused by dependencies, if safety is not in the baseline. So my opinion is, unsafe code should be really exceptional, to the point that whenever such functionality is used, the user should explicitly type it out, by typing .Unsafe himself when importing modules. That can be considered as a virtual consensus that the user acknowledges the implementation the unsafe. Then the responsibility at that point is clear.

In fact, being able to fully trust the system and trust the safety of implementation is an important aspect of being practical for all dependent type languages.

I hope this one can be a bit more prioritized. I believe lots of people out there would consider picking Agda, solely because of its presumed safety from being a dependent type language.

@gallais

This comment has been minimized.

Member

gallais commented Mar 24, 2018

Is this worth being an 1.0 kind of issue? This would induce a big backwards-compatibility breakage but we would also have the guarantee it is going to be canon in the further releases.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Mar 24, 2018

I still feel that many of the current issues could be circumvented by making safe more discriminating and detect that there are no unsafe terms used, even if they live in modules that do contain unsafe terms (see agda/agda#2789).

I realise there's strong demand to get around its limitations in the mean time. I agree with @HuStmpHrrr , I far prefer the style of X.Y.Z.Unsafe over duplicating the entire hierarchy and having Safe.X.Y.Z. Things should be safe by default, and we only need to make people aware when they're using unsafe features. @gallais I know you put a lot of work into the safe branch. What do you think?

Is this worth being an 1.0 kind of issue? This would induce a big backwards-compatibility breakage but we would also have the guarantee it is going to be canon in the further releases.

I think so too. I have nearly completed all of my planned structural re-organisations. The last three are:

  • Membership and BagAndSetEquality (#94 & #155)
  • PartialOrderReasoning (see #185 )
  • Get rid of Fin.Dec

After that I don't anticipate any more major structural changes, so it seems like it would be a good time to at long last release version 1.0!

@HuStmpHrrr

This comment has been minimized.

Contributor

HuStmpHrrr commented Apr 4, 2018

I was thinking about it for the last couple days, and I hope I got a better picture of this.

I think it might not be the problem of this library (though it's indeed very nice if unsafe code can be extracted to submodules in the previously mentioned way). I do agree that it's going to be much better of, if the compiler can check the safety of every function, like @MatthewDaggitt suggested. One of the very important aspects of being able to do so, is to make tactics more realizable. Since tactics are macros and based on yet another bunch of postulates, there is no way if a program is written by tactics and can be safe. However, the program built by tactics itself can be entirely safe; while on the other hand, one can indeed embed unsafe code via tactics as well.

From that aspect, I believe adding such functionalities to the compiler will help largely to eliminate boring mechanical programming in agda, and that also means that it's more on what the compiler does, instead of what this particular library looks like.

@MatthewDaggitt MatthewDaggitt added this to To do in safeness Apr 11, 2018

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 11, 2018

So thought I'd get started on this. I have a quick question though:

  • Why doesn't the command:
    agda --safe src/Relation/Binary/HeterogeneousEquality/Quotients.agda
    
    throw an error? If I put {-# OPTIONS --safe #-} at the top of the file it detects the postulate, but it
    doesn't from the command line...
@asr

This comment has been minimized.

Member

asr commented Apr 11, 2018

Why doesn't the command:

agda --safe src/Relation/Binary/HeterogeneousEquality/Quotients.agda

throw an error?

When trying of reproducing the problem in Agda stable-2.5 branch I got the error:

$ make up-to-date-std-lib
...
cabal exec -- GenerateEverything
GenerateEverything: src/Relation/Binary/HeterogeneousEquality/Quotients.agda is malformed.
CallStack (from HasCallStack):
  error, called at GenerateEverything.hs:67:15 in main:Main
GNUmakefile:16: recipe for target 'Everything.agda' failed
@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 11, 2018

Hmm weird. I'm on a clean version of 2.5.3. I'm having the same problem with the --without-K option...

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 12, 2018

Tracked it down, it was another subtler instance of agda/agda#2487. As I'd compiled the whole library without --safe, the .agdai files were lying to me when I subsequently recompiled it all with --safe. I'm rapidly coming to the opinion that the --safe option currently doesn't provide anything much in the way of guarantees (either in-file or at the command line) 😞

@gallais

This comment has been minimized.

Member

gallais commented Apr 12, 2018

--safe + --ignore-interfaces is pretty reliable

@WolframKahl

This comment has been minimized.

Member

WolframKahl commented Apr 12, 2018

@nad

This comment has been minimized.

Contributor

nad commented Apr 13, 2018

I'm rapidly coming to the opinion that the --safe option currently doesn't provide anything much in the way of guarantees (either in-file or at the command line)

The --safe feature was originally implemented by someone who is no longer contributing to Agda, and it seems as if no regular developer is eager to maintain it. Fixing the documented bugs related to --safe requires some work, but I think it should be doable for someone who is not intimately familiar with the internals of Agda. Contributions are welcome.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 13, 2018

I'm rapidly coming to the opinion that the --safe option currently doesn't provide anything much in the way of guarantees (either in-file or at the command line)

Fixing the documented bugs related to --safe requires some work, but I think it should be doable for someone who is not intimately familiar with the internals of Agda. Contributions are welcome.

While I would love to, I feel I already spend far too much of my time of my PhD on internet routing protocols playing around with Agda! Sorry, I realise that my original comment perhaps came off as a complaint, it wasn't meant to be.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 13, 2018

I've started working on creating the various Unsafe modules (very similar to @gallais work on #122). It's all mostly okay (although haven't got to Data.Integer yet...) but the first problem I've come across is in Data.Nat.DivMod.

record DivMod (dividend divisor : ℕ) : Set where
constructor result
field
quotient :
remainder : Fin divisor
property : dividend ≡ toℕ remainder + quotient * divisor

The problem is that the remainder field is of type Fin divisor and not . For efficiency's sake (although apparently it doesn't work very well, see #150) we erase all the various proof that allows us to convert from to Fin divisor. The erasure uses trustMe which is, of course, unsafe. This then pollutes large parts of the following modules that depend on DivMod:

Data.Nat.Divisibility
Data.Nat.Primality
Data.Nat.Show
Data.Digit

There are three options that I see:

  1. Proceed as planned and stick all dependencies in Unsafe modules.
    • Advantages: A little more backwards compatible (although obviously all module imports will have to change).
    • Disadvantages: we label large sections of our Nat library as Unsafe, including our primality test which is a tad embarrassing.
  2. Change the type of _mod_ and the field remainder to rather than Fin divisor, and then create separate proofs that show they are all related in the right way.
    • Advantages: This would provide a faster and safe version of _mod_, and hence avoid polluting the safety of the rest of the library with the use of trustme. The proofs that the right properties hold, still exist, and users themselves can make the choice of whether or not to erase them for efficiency reasons.
    • Disadvantages: not backwards compatible
  3. Simply remove the erase calls:
    • Advantages: Completely backwards compatible and all the files automatically become safe.
    • Disadvantages: Performance gets even worse.

I'd prefer the 2nd option as it feels much more principled. Not all users will require the proofs, but those that do then have much finer grained control over how they use them. The non-backwards compatability is unfortunate but that's why we're labelling it v1.0?

@HuStmpHrrr

This comment has been minimized.

Contributor

HuStmpHrrr commented Apr 14, 2018

Disadvantages: Performance gets even worse.

I am astonished by the performance part. Might I ask how important performance is, and how many people are relying on it? Sorry about my ignorance...

What about irrelevance? I've not seen the description in official doc, but from my understanding, this should be the secrete magic to tame the tradeoff between complex proof flow and performance, is it not?

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Apr 16, 2018

I am astonished by the performance part. Might I ask how important performance is, and how many people are relying on it? Sorry about my ignorance...

No idea. I don't personally normalise any of my proofs. But given that Ulf has put significant effort into building agda-prelude with a strong focus on performance I gather it's definitely important for some people. Also issue #150 is is actually directly related to the performance of this part of the library.

What about irrelevance? I've not seen the description in official doc, but from my understanding, this should be the secrete magic to tame the tradeoff between complex proof flow and performance, is it not?

Again, as I never worry about actually normalising I've never had any need to dip into irrelevance. Maybe someone with more experience could chime in?

Overall, I think the consensus is that the standard library focuses on making proofs easier rather than on performance. Having said that, we should probably generally avoid making performance worse except for good reason. Hopefully we can come to some conclusion here whether or not safety is a good enough reason!

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Jul 6, 2018

#350 which has just been merged provides a way forward on this problem. It adds a new "safe" modular arithmetic library. The old library can then be placed in the Unsafe module. The dependencies have been updated to use the new library.

@MatthewDaggitt

This comment has been minimized.

Contributor

MatthewDaggitt commented Aug 30, 2018

Closed with 8885d7a

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment