`Unsafe` constraint - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

TheMatten

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 :: ()

instance TypeError
           (    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' [1])
TheMatten

When you forget to handle Unsafe:

λ> 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]
Sandy Maguire

can i instead pass on an Unsafe constraint?

Sandy Maguire

eg useHead2 :: Unsafe => Int; useHead2 = head' [1]?

Sandy Maguire

i'm not sure how instance resolution works for nullary constraints

TheMatten

Yes - not really sure how to go around that though

TheMatten

For Partial that makes complete sense, not that much for Unsafe I guess

TheMatten

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

Sandy Maguire

No, this design is better. It composes

TheMatten

Hmm, yeah - question is, do invariants captured by it compose too?

Sandy Maguire

i don't see why unsafeness wouldn't just bubble like this

TheMatten

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

TheMatten

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

TheMatten

I guess such model more fits some sort of Unsafe wrapper than constraint

TheMatten

But then, e.g. having to put separate unsafe around every pointer dereferencing would be cumbersome

TheMatten

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

Sandy Maguire

https://github.com/Soares/Dangerous.hs

Handles computations that can exit early and log warnings - Soares/Dangerous.hs