[ new ] Factoring out unsafe parts of the library

[MatthewDaggitt]

The latest attempt at factoring out the parts of the library that will not type check with the --safe option. See issue #143.

All modules are now safe except:

• IO(.Primitives)
• Reflection
• Relation.Binary.PropositionalEquality.TrustMe
• Any of the new modules Data.X.Unsafe

The main changes necessary:

• Built-in types such as Char, String, Word etc. have all had their meaningful equality checks marked as unsafe.
• Relation.Binary.HeterogeneousEquality.Quotients(.Examples) had function extensionality postulated. I've made these safe by moving extensionality to a module parameter. Therefore users can still postulate extensionality for themselves and use the definitions, but it no longer pollutes the library.

Open questions:

• Can we come up with safe equality checks for built-ins?
• Can we incorporate testing with the --safe option into make tests?

[gallais]

Would it make sense for X.Unsafe to re-export X? This way if you're importing
X and realize you're missing an unsafe function, you can simply append .Unsafe
to the import.

[gallais]

Regarding your questions:

Can we come up with safe equality checks for built-ins?

Without adding new primitives? I doubt we can.

Can we incorporate testing with the --safe option into make tests?

Sure (it's a matter of generating a file importing all the modules whose name does not end in Unsafe).
I'll look into it (for travis first).

[gallais]

We're hitting the Agda.Builtin.Coinduction problem: it postulates 3 names and, as such,
can't be typechecked with --safe.

Is there a reason why Agda.Builtin.Coinduction is not like Agda.Builtin.Size where
names don't need to be postulated to be bound to a BUILTIN? I tried modifying my
Agda.Builtin.Coinduction by hand to remove the postulates and got a scope error.

Edit: the same will probably be true of Agda.Builtin.Char and Agda.Builtin.String.

[MatthewDaggitt]

Would it make sense for X.Unsafe to re-export X? This way if you're importing
X and realize you're missing an unsafe function, you can simply append .Unsafe
to the import.

Hmm I can see the advantage. On the other hand it's then not immediately clear which parts being used are unsafe and which are safe. The export hierarchy is also getting a little bit complicated at that point. e.g. Data.Nat.Unsafe exports everything in Data.Nat which in turn exports everything from Data.Nat.Base... I'm happy to be convinced though.

We're hitting the Agda.Builtin.Coinduction problem: it postulates 3 names and, as such,
can't be typechecked with --safe.

Ah of course. I missed this problem. I've been running find . -name "*.agdai" -type f -delete then agda --safe, but what I really should have been doing is agda --safe --ignore-interfaces.

The only solution to this problem that I can see is to extend the mechanism of explicitly turning --safe off for Primitive files to Built-ins as well... Depends if there are any things in the Builtin modules that truly are unsafe...

Guess we should open an issue on the main Agda repository...

[WolframKahl]

I'd be more likely to continue to import X, and, for documentation: ``` open import X.Unsafe using (unsafeXfunction) ```

[gallais]

and, for documentation:

Good point, I like this approach.

Guess we should open an issue on the main Agda repository...

+1

[gallais]

(Provided that I make sure travis is using Agda's master on experimental) we should now
be able to merge safe into experimental. 🍾

[MatthewDaggitt]

(Provided that I make sure travis is using Agda's master on experimental) we should now
be able to merge safe into experimental. champagne

Do we need to merge this into experimental? Unless you've changed something that I haven't noticed, I'm pretty sure its compatible with the current version of Agda. It just won't type check with --safe... but that's no different from the situation at the moment 😄

[gallais]

Good point. You would need to comment out this line in .travis.yml: https://github.com/agda/agda-stdlib/blob/safe/.travis.yml#L75

[gallais]

I'm so hyped by this. 🎆

[MatthewDaggitt]

I'm so hyped by this. fireworks

I'm glad, it's been a long time coming!