I really like idea of Partial constraint in PS for capturing "unsafeness" in a way that doesn't affect return type - it can create "contracts" system similar to unsafe in Rust. Previously, my attempts to encode it in Haskell weren't ideal, because they required unsafeCoerce, which doesn't inline - luckily, magicDict seems to be effective substitute:
moduleUnsafe(Unsafe,unsafe)whereclassUnsafewhere_Unsafe::()instanceTypeError(Text"Function is marked as unsafe":$$:Text"Read function documentation for more info":$$:Text"To accept invariant, use ‘unsafe’")=>Unsafewhere_Unsafe=error"Unsafe: internal error - unreachable code"dataWrapUua=WrapU(Unsafe=>a)unsafe::foralla.(Unsafe=>a)->aunsafea=magicDict(WrapU@()f)()()wheref::Unsafe=>()->af_=a-- | BEWARE: this fails on empty list!head'::Unsafe=>[a]->ahead'(x:_)=xuseHead'::IntuseHead'=unsafe(head'[1])
λ> head' [1]
<interactive>:4:1: error:
• Function is marked as unsafe
Read function documentation for more info
To accept invariant, use ‘unsafe’
• In the expression: head' [1]
In an equation for ‘it’: it = head' [1]
I think of (Rust's) unsafe as "asking for acknowledgment of invariants connected with this function call" - but if unsafe block is assumed over whole function, then I'm not really asked to review every specific unsafe call, possibly ignoring their requirements
When I call multiple (or zero) unsafe functions in body of Unsafe => one, they may have different reasons for their "unsafeness" - possibly even colliding ones
I really like idea of
Partial
constraint in PS for capturing "unsafeness" in a way that doesn't affect return type - it can create "contracts" system similar tounsafe
in Rust. Previously, my attempts to encode it in Haskell weren't ideal, because they requiredunsafeCoerce
, which doesn't inline - luckily,magicDict
seems to be effective substitute:When you forget to handle
Unsafe
:Nice!
Nice!
Nice!
can i instead pass on an Unsafe constraint?
eg
useHead2 :: Unsafe => Int; useHead2 = head' [1]
?i'm not sure how instance resolution works for nullary constraints
Yes - not really sure how to go around that though
For
Partial
that makes complete sense, not that much forUnsafe
I guessWe could say it behaves like Rust's
unsafe fn
- though that's probably going to be changed to requireunsafe
in it's bodyNo, this design is better. It composes
Hmm, yeah - question is, do invariants captured by it compose too?
i don't see why unsafeness wouldn't just bubble like this
I think of (Rust's)
unsafe
as "asking for acknowledgment of invariants connected with this function call" - but ifunsafe
block is assumed over whole function, then I'm not really asked to review every specificunsafe
call, possibly ignoring their requirementsWhen I call multiple (or zero)
unsafe
functions in body ofUnsafe =>
one, they may have different reasons for their "unsafeness" - possibly even colliding onesoh interesting idea
I guess such model more fits some sort of
Unsafe
wrapper than constraintBut then, e.g. having to put separate
unsafe
around every pointer dereferencing would be cumbersomeI may want to say that "some block" is unsafe, but it would be nice if function bodies with
Unsafe
constraint weren't completelyunsafe
implicitlyUnsafe
monad :joy:https://github.com/Soares/Dangerous.hs
not relevant code
but great name
Haha, code above doesn't seem to work on 9.2 - and you don't really get to know why, because
magicDict
transformation fails implicitly :big_smile:btw I don't know if you saw this, but there's currently a discussion for a very similar/the same thing on the haskell cafe mailing list
(
Partial
)I didn't - it's from this month or earlier?
like, this week, or so
I see some
Foldable1
discussion - you mean that one?oops
sec
wrong list
https://mail.haskell.org/pipermail/libraries/2021-June/031258.html
Ah, ok, no problem :big_smile:
here's the thread
https://mail.haskell.org/pipermail/libraries/2021-June/thread.html
Ah, so that one's about
HasCallStack
it seemsyes, but the discussion morphed into discussing a
Partial
-like constraint, to act as an abstraction overHasCallStack
Ah found it now, thanks!