sealing unsafe

Stream: lean4

[Siddharth Bhat]

Is there some way to prevent unsafe from propagating outwards? Once again, my use case is dubious, but it would be useful to prototype something. I'm really looking for something like unsafePerformIO: IO a -> a. Lean seems to have at most unsafeIO, which infects the outer scope with unsafe annotations.

[Henrik Böving]

You can refer to an unsafe definition using the implemented by attribute as for example done here https://github.com/leanprover/lean4/blob/31969765d278416470dcecf118c31aa714bd38ce/src/Init/Data/Array/Basic.lean#L108-L130

[Siddharth Bhat]

The actual problem: I'm trying to make generated paths relative for doc-gen4. There are paths that look like ./build/doc//./Init/Control, which I want to normalize. It appears that rustc calls out to realpath. I'd like to quickly test that this solves the problem for me before I pull in an IO into the monad transformer stack...

[Reid Barton]

You can't have IO a -> a without unsafe because it would break the logic.

[Siddharth Bhat]

Henrik Böving said:

You can refer to an unsafe definition using the implemented by attribute as for example done here https://github.com/leanprover/lean4/blob/31969765d278416470dcecf118c31aa714bd38ce/src/Init/Data/Array/Basic.lean#L108-L130

Wow that's neat! OK, let me try that

[Siddharth Bhat]

@Reid Barton Yes, I'm aware what I'm asking for is unsound :)

[Reid Barton]

Well Lean is sound, so the answer is no

[Reid Barton]

(hopefully :upside_down:)

[Siddharth Bhat]

Lean also hassorrys, which it allows, and whose presence tracks in the kernel(?). I imagine it could hypothetically do something similar for unsafePeformIOSealed: IO a -> a?

[Henrik Böving]

Regarding your normalization thingy, is FilePath.normalize strong enough for this?

[Reid Barton]

Well, more practically for any inhabited a (like String) you can make IO a -> a using unsafe/implementedBy

[Siddharth Bhat]

@Henrik Böving no, the implementation of FilePath.normalize has a TODO for this.

I was hoping I could quickly write out a correct implementation. But it seems like Rust calls out to C for this. This makes me feel that calling out to realpath is the sanest thing to do

[Henrik Böving]

Hm it seems the reason cannonical would need IO is because it also does stuff such as resolving symlinks. Other than that the implementation in libc just looks like a ton of C string hackery.

[Yakov Pechersky]

How does pathlib do it in Python?