1. 29
  1. 8

    I think you’ve overstated the freedom that unsafe provides in your first footnote. It really just lets you dereference certain pointers, but all of the type checking still works. I think it’s important to dispel this myth since there’s a misconception that “you can do anything in unsafe Rust, so there’s no benefit over C/C++”.

    From the book:

    Those superpowers include the ability to:

    • Dereference a raw pointer
    • Call an unsafe function or method
    • Access or modify a mutable static variable
    • Implement an unsafe trait

    It’s important to understand that unsafe doesn’t turn off the borrow checker or disable any other of Rust’s safety checks: if you use a reference in unsafe code, it will still be checked.

    1. 5

      Yeah, it’s important to understand that unsafe really just means you can deref raw pointers. With that power (combined with pointer casts) you can circumvent any safety check, but those checks are not disabled.

      Unsafe Rust is still a safer and more explicit language than C/C++, but just as powerful. The cost is increased verbosity.

    2. 4

      Is there a way in Rust to create a type that blows up if it gets released by falling out of scope?

      I ask this because I wonder if you could do some type trickery to ensure that (for example) a file was explicitly closed at one moment (instead of relying on implicit closing from falling out of scope)

      In any case this is really neat stuff.

      1. 5

        Implement a destructor that panics. It’s called a “drop bomb”.

        The static version of it is analyzing of the destructor got linked.

        1. 3

          Clever. I’d hate to have to decrypt that error message tho.

          1. 4

            I appreciate that! For the reasoning why Rust doesn’t (currently?) have full linear types, see https://gankro.github.io/blah/linear-rust/

            It’s a surprisingly huge design space once you get into the details.

      2. 3

        If you like this idea, check out dependent types and indexed monads, essentially a much more powerful/general way of accomplishing similar things. Here’s the Idris tutorial that deals with this topic: http://docs.idris-lang.org/en/latest/st/introduction.html

        Here’s how it’s more powerful:

        STrans : (m : Type -> Type) -> -- ignore  this
                 (resultType : Type) -> -- result type of the operation
                 (in_res : Resources) -> -- resources the operation gets
                 (out_res : resultType -> Resources) -> -- how it changes them

        STrans is the Idris type constructor that encodes, shockingly, a state transition. You use it to write functions that operate on resources, which can be types tagged as state as in State Integer. The most important elements of this type are in_res : Resources, a list of resources (states) the operation has as a precondition, and out_res : resultType -> Resources, a function which computes the operation’s effects (postconditions) from its result. These are all a part of the operation’s/function’s type!

        Here’s an example operation from the tutorial:

        addElement : (vec : Var) -> (item : a) ->
                     STrans m () [vec ::: State (Vect n a)]
                          (const [vec ::: State (Vect (S n) a)])
        addElement vec item = do xs <- read vec
                                 write vec (item :: xs)

        There are two things to notice here, first it’s the concrete STrans type: in_res here contains one element, a variable vec of type ‘vector of length n’, and out_res is a function which always returns a list containing the vec of type ‘vector of length n+1’. The type of the variable changed. If you were to implement this stateful operation without changing the type of vec in the correct way, by increasing its size by one, it would not compile. The second important thing to notice is that STrans’s compose. read and write are also STrans programs. In practice, you use Control.ST, which is a less verbose type which reduces to STrans.

        While STrans provides a lot of generality, it’s also rather easy to roll your own equivalents, and the Idris book has you implementing various stateful systems completely from scratch (without relying on Control.ST) using GADTs. For example, here’s an ATM type:

        -- type
        data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
          InsertCard  : ATMCmd  ()  Ready         (const CardInserted)
          GetPIN      : ATMCmd  PIN CardInserted  (const CardInserted)
          EjectCard   : {auto prf : HasCard state} -> ATMCmd () state (const Ready)
          CheckPIN    : PIN -> ATMCmd PINCheck CardInserted
                                  (\check => case check of
                                                  CorrectPIN => Session
                                                  IncorrectPIN => CardInserted)
          GetAmount : ATMCmd Nat state (const state)
          Dispense : (amount : Nat) -> ATMCmd () Session (const Session)
          Message : String -> ATMCmd () state (const state)
          Pure    : (res : ty) -> ATMCmd ty (state_fn res) state_fn
          (>>=)   : ATMCmd a state1 state2_fn ->
                    ((res : a) -> ATMCmd b (state2_fn res) state3_fn) ->
                    ATMCmd b state1 state3_fn
        -- program
        atm : ATMCmd () Ready (const Ready)
        atm = do InsertCard
                 pin <- GetPIN
                 pinOK <- CheckPIN pin
                 case pinOK of
                       CorrectPIN => do cash <- GetAmount
                                        Dispense cash
                       IncorrectPIN => EjectCard

        Notice the similarity to STrans on the first line. The arguments for ATMCmd correspond to resultType, in_res, and out_res. The program atm cannot be started outside the Ready state, and cannot be implemented as resulting in anything but a Ready state (that’s what its ATMCmd type states). You can start with even more primitive examples which don’t even take into account that out_res is a function, but merely hard-code the result state (meaning that the operation cannot fail).

        1. 3

          That’s exactly the pattern why I think decision to use Rust’s borrow checker in Facebook Libra’s new contract language, Move is a stroke of genius.

          1. 3
            1. Neat! Great explanation.
            2. This still feels like a super awkward way to encode these sorts of usage constraints.

            Take the initial example:

            struct HttpResponse(Box<ActualResponseState>);
            struct HttpResponseAfterStatus(Box<ActualResponseState>);

            This is a single-type-tag/class-based encoding of state, which can work in the small, but immediately leads to an explosion of classes and therefore match cases and other dispatch branches.

            Hence the follow-up variation:

            struct HttpResponse<S: ResponseState> {

            but this is still awkward.

            First, the state is a required, positional type parameter. You could introduce an AnyResponseState phantom, but that’s not really what you want, since you may want to be parametric polymorphic, not existential, so now generalizing over HttpResponse states makes this type parameter viral.

            Meanwhile, if you add additional type parameters, you’re introducing a breaking change. For example, what if you want to also encode, at the type-level, the state of a websocket connection initiation? You’d need some kind of wrapper type, since you can’t reasonably add static metadata to the response post-hoc.

            But, perhaps most importantly, this is just an unnatural way to express these constraints.

            To go back to the open/closed file example. Ideally, you’d like to be able to write a more natural constraint, such as fn close(file) if open?(file)

            1. 1

              This seems to confuse “borrow checking” with type checking. The file example is not the same as the HTTP example. The actual type-based pattern should be possible in any language with parametric types and static type checking.

              The use of borrow for state checking is more unusual and requires that to be baked into the compiler.

              1. 3

                True, the file example is using borrow checking rather than types. I think later they’re making the case that the borrow checker can enforce the typestate pattern in the case of typestate transitions causing side-effects. This would be difficult to do in a language without proper move semantics to invalidate the previous state.