Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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:
module Unsafe (Unsafe, unsafe) where
class Unsafe where
_Unsafe :: ()
( Text "Function is marked as unsafe"
:$$: Text "Read function documentation for more info"
:$$: Text "To accept invariant, use ‘unsafe’"
=> Unsafe where
_Unsafe = error "Unsafe: internal error - unreachable code"
data WrapU u a = WrapU (Unsafe => a)
unsafe :: forall a. (Unsafe => a) -> a
unsafe a = magicDict (WrapU @() f) () () where
f :: Unsafe => () -> a
f _ = a
-- | BEWARE: this fails on empty list!
head' :: Unsafe => [a] -> a
head' (x:_) = x
useHead' :: Int
useHead' = unsafe (head' )
When you forget to handle Unsafe:
λ> head' 
• Function is marked as unsafe
Read function documentation for more info
To accept invariant, use ‘unsafe’
• In the expression: head' 
In an equation for ‘it’: it = head' 
can i instead pass on an Unsafe constraint?
eg useHead2 :: Unsafe => Int; useHead2 = head' ?
useHead2 :: Unsafe => Int; useHead2 = head' 
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 for Unsafe I guess
We could say it behaves like Rust's unsafe fn- though that's probably going to be changed to require unsafe in it's body
No, 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 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
oh interesting idea
I guess such model more fits some sort of Unsafe wrapper than constraint
But then, e.g. having to put separate unsafe around every pointer dereferencing would be cumbersome
I may want to say that "some block" is unsafe, but it would be nice if function bodies with Unsafe constraint weren't completely unsafe implicitly
Unsafe monad :joy:
not relevant code
but great name