No clear haskell API about sudbury HOT 13 OPEN

What we can support without much further work is to set up a socket connection, to split incoming bytes into WirePackages, and to serialize WireMessages. To decode WirePackages, we need to understand the protocol: but the way this protocol data is handed to the library differs between use cases. For example, a debugging tool will read the XML files. But a C program hands it to us as a bunch of pointers to C structs (in particular, upon creating an object via the wl_registry). We need to support all those use cases. Probably the best solution is for sudbury to take a structure that tells us which message contains which arguments, to be handed over when using the wl_registry (or any other untyped object-creating message, for that matter).

If we have that, we can decode WirePackages into WireMessages. If we also add some tool that translates XML data into that structure, I think we have all the ingredients for a protocol dumper (à la wayland-tracker).

from sudbury.

I worked on this for a while but hit a few bumps. I sent a message to the haskell-cafe mailing list. So no real progress on this issue yet, but I just wanted to report having worked on it.

from sudbury.

Okay, since 3eab352 we can read XML data into a protocol object and process it into another object which can be used to track which wayland ID has which . I will now write code that generates this same data from a C pointer to a struct wl_interface (as used in the C ABI). This way we can unify the Haskell API and the C ABI.

from sudbury.

(TODO: reduce code duplication by parameterising whether the particular protocol flavor has the cross-references as Strings or as actual Interfaces/ArgEnums. This will need type fixpoints, as in Sergey's response to my haskell-cafe question.)

from sudbury.

(This TODO is now implemented by 72279ed.)

from sudbury.

I've started trying to write some client code that interfaces with a compositor in a rather "raw" form.

main :: IO ()
main = do
  s <- connectWithDefault
  let fd = Fd $ fdSocket s
  cliArgs <- getArgs
  prot <- case cliArgs of
            [] -> readProtocol
            xmlLoc:_ -> parseFile xmlLoc
  case prot of
    Nothing -> die "Couldn't parse XML protocol"
    Just prot' -> do
      let get_registry = WireMessage 1 1 [WireArgBox SNewIdWAT 2]
          get_registry_package = messageToPackage get_registry
          bytes = wirePack get_registry_package
      sendToWayland fd (BL.toStrict $ BB.toLazyByteString bytes) [] >>= print
      return ()

It now seems to me that type safety must be the first step towards a Haskell API. In particular I'm thinking of using quasiquoting to be able to replace the explicit WireMessage (etc) constructors by, e.g., let (get_registry_package, registry) = [wl|display.get_registry] display which would construct the same get_registry message as the above code, and which would also construct an appropriate [wl|wl_registry] object (where [wl|wl_registry] would now be an appropriate type).

from sudbury.

Over the past few months I've tried to think of an ideal haskell API.

One thing that has been bugging me is that we can't "pass around" references to arbitrary wayland objects, as they might be invalidated later on: so we can't just pass the user code a wl_shm_pool, for instance, as it might get destroyed at a later time. It might even be destroyed by that very same user, but that doesn't matter: we shouldn't rely on the user code being smart enough to forget about destroyed objects. In fact there are cases where the user code can't entirely forget about destroyed objects, namely in the form of wayland zombie objects (which are like zombie processes, in the sense that they're objects that exist only because they still have children).

So I'm starting to think we should only allow the user to specify how to handle the current tree of objects, and the various current modifications on it, rather than these objects being some kind of return value of a "get me the latest messages" request. In other words, we should have the user... fold (?) on the object tree? And then wayland messages are some kind of zipper (?) on that tree?

Another element of this problem is the following. In most situations, user code will want to take the wayland point of view of the computer, and use changes of the wayland model to update some internal state: for example, if a new client connects to a compositor and creates a window (which means that the client sends a series of messages to the compositor), that means the compositor should now make space for the window on the screen, and present the user with ways to manipulate this new window, keep track of the window size and position, etc. That means that wayland state should cohere in some way with the internal state of user code (which may exist both compositor-side and client-side). Is there a way to present the wayland state so that it is easy for these two states in one piece of code to cohere in the right way? Or at least to make this state coherence testable?

Ideas are very, very welcome.

from sudbury.

So more concretely, and at the same time more vaguely: in Haskell language, what is a stateful communication protocol?

from sudbury.

One possible definition is to say that the wayland state and the user code's state are both state transition systems. Then to say that the states cohere means something like that there is a bisimulation relation between them, with the bisimilar states being picked out by a state update function. Then one can also make sense of what it means for these states to update asynchronously. This is nice because we can now make precise mathematically what it means for wayland to be asynchronous, and there is hope we can test if it is true.

The disadvantage is that we are going to have to be a whole lot more explicit about our states and their transitions.

I'll try to write this up in some detail, although this might take a few weeks.

from sudbury.

Also, this is a really nice approach to making everything type safe.

from sudbury.

I will also read this and then write a proof of concept.

from sudbury.

Here's one attempt at encoding a display::error message. You can run the following by saving it as script.hs (or whatever) and executing stack script.hs.

#!/usr/bin/env stack
{- stack script
    --resolver lts-12.2
    --package vinyl
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedLabels #-}
import GHC.TypeLits
import Data.Vinyl

-- The type of messages display::error (see wayland.xml)
type DisplayError =
  ElField ("displayerror" :::
          FieldRec '["object_id" ::: Int, "code" ::: Word, "message" ::: String])

-- One sample message
err1 :: DisplayError
err1 = #displayerror =:
  (  #object_id =: 3
  :& #code =: 18
  :& #message =: "You sent the wrong message earlier, sorry!"
  :& RNil
  )

main = print err1

Result:

$ stack script.hs
displayerror :-> {object_id :-> 3, code :-> 18, message :-> "You sent the wrong message earlier, sorry!"}

from sudbury.

The advantage of the above approach over C's approach of generating appropriate function stubs is that it allows to write type-safe code that is generic in the actual message being sent. This is invaluable for writing debugging programs. A program may be written in the above style that is type-safe, even before the protocol is known: only at compile time (so crucially: after development time) does the protocol need to be decided.

At the same time, if a programmer wishes to interact with a specific part of the protocol (e.g. interact with the mouse, because the programmer is writing a compositor), the above approach is a type-safe approach for exchanging messages. The messages can be stored as objects, and passed around freely - in contrast with C style messages which, from a libwayland user point of view, don't really exist as stand-alone objects.

So I am to use this approach to allow users to write code that is independent of the protocol, yet is type safe in the sense that mistaking one message for another, or one message's argument for another, yields an informative compile-time error.

from sudbury.