From bdfb6c64470b7e378ff107c9d71128b66e99e81d Mon Sep 17 00:00:00 2001 From: Thibaut Mattio Date: Wed, 29 Nov 2023 15:38:58 +0100 Subject: [PATCH] Add Practical OCaml to the Planet (#1806) --- data/planet-sources.yml | 3 + .../re-developing-tcp-from-the-grounds-up.md | 49 ++++++++ data/planet/practicalocaml/-hello--world-.md | 16 +++ ...-gadts-and-why-you-aint-gonna-need-them.md | 102 +++++++++++++++ ...d-fast-with-ocaml-modeling-a-web-router.md | 16 +++ ...pe-safe-state-machines-using-type-state.md | 117 ++++++++++++++++++ .../unix-module-considered-harmful.md | 26 ++++ 7 files changed, 329 insertions(+) create mode 100644 data/planet/hannes/re-developing-tcp-from-the-grounds-up.md create mode 100644 data/planet/practicalocaml/-hello--world-.md create mode 100644 data/planet/practicalocaml/a-quick-guide-to-gadts-and-why-you-aint-gonna-need-them.md create mode 100644 data/planet/practicalocaml/how-i-explore-domain-problems-cheaply-and-fast-with-ocaml-modeling-a-web-router.md create mode 100644 data/planet/practicalocaml/how-to-build-type-safe-state-machines-using-type-state.md create mode 100644 data/planet/practicalocaml/unix-module-considered-harmful.md diff --git a/data/planet-sources.yml b/data/planet-sources.yml index f968480ccd..df40f009d4 100644 --- a/data/planet-sources.yml +++ b/data/planet-sources.yml @@ -1,3 +1,6 @@ +- id: practicalocaml + name: Practical OCaml + url: https://practicalocaml.com/rss/ - id: ocamlpro name: OCamlPro url: https://ocamlpro.com/blog/feed diff --git a/data/planet/hannes/re-developing-tcp-from-the-grounds-up.md b/data/planet/hannes/re-developing-tcp-from-the-grounds-up.md new file mode 100644 index 0000000000..90783fac99 --- /dev/null +++ b/data/planet/hannes/re-developing-tcp-from-the-grounds-up.md @@ -0,0 +1,49 @@ +--- +title: Redeveloping TCP From the Ground Up +description: +url: https://hannes.robur.coop/Posts/TCP-ns +date: 2023-11-28T21:17:01-00:00 +preview_image: +featured: +authors: +- hannes +source: +--- + +

The Transmission Control Protocol (TCP) is one of the main Internet protocols. Usually spoken on top of the Internet Protocol (legacy version 4 or version 6), it provides a reliable, ordered, and error-checked stream of octets. When an application uses TCP, they get these properties for free (in contrast to UDP).

+

As common for Internet protocols, TCP is also specified in a series of so-called requests for comments (RFC). The latest revised version from August 2022 is RFC 9293; the initial one was RFC 793 from September 1981.

+

My Brief Personal TCP Story

+

My interest in TCP started back in 2006 when we worked on a network stack in Dylan (these days abandoned). Ever since, I wanted to understand the implementation tradeoffs in more detail, including attacks and how to prevent a TCP stack from being vulnerable.

+

In 2012, I attended ICFP in Copenhagen while a PhD student at ITU Copenhagen. There, Peter Sewell gave an invited talk "Tales From the Jungle" about rigorous methods for real-world infrastructure (C semantics, hardware (concurrency) behaviour of CPUs, TCP/IP, and likely more). Working on formal specifications myself in (my dissertation) and having a strong interest in real systems, I was immediately hooked by his perspective.

+

To dive a bit more into network semantics, the work done on TCP by Peter Sewell, et. al., is a formal specification (or a model) of TCP/IP and the Unix sockets API developed in HOL4. It is a label transition system with nondeterministic choices, and the model itself is executable. It has been validated with the real world by collecting thousands of traces on Linux, Windows, and FreeBSD, which have been checked by the model for validity. This copes with the different implementations of the English prose of the RFCs. The network semantics research found several issues in existing TCP stacks and reported them upstream to have them fixed (though, there still is some special treatment, e.g., for the "BSD listen bug").

+

In 2014, I joined Peter's research group in Cambridge to continue their work on the model: updating to more recent versions of HOL4 and PolyML, revising the test system to use DTrace, updating to a more recent FreeBSD network stack (from FreeBSD 4.6 to FreeBSD 10), and finally getting the journal paper (author's copy) published. At the same time, the MirageOS melting pot was happening at University of Cambridge, where I contributed OCaml-TLS, etc., with David.

+

My intention was to understand TCP better and use the specification as a basis for a TCP stack for MirageOS. The existing one (which is still used) has technical debt: a high issue to number of lines ratio. The Lwt monad is ubiquitous, which makes testing and debugging pretty hard, so utilising multiple cores with OCaml Multicore won't be easy. Plus it has various resource leaks, and there is no active maintainer. But honestly, it works fine on a local network, and with well-behaved traffic. It doesn't work that well on the wild Internet with a variety of broken implementations. Apart from resource leakage, which made me implement things such as restart-on-failure in albatross, there are certain connection states which will never be exited.

+

The Rise of µTCP

+

Back in Cambridge, I didn't manage to write a TCP stack based on the model, but in 2019, I restarted that work and got µTCP (the formal model manually translated to OCaml) to compile and do TCP-session setup and teardown. Since it was a model that uses nondeterminism, this couldn't be translated one-to-one into an executable program, but there are places where decisions have to be made. Due to other projects, I worked only briefly in 2021 and 2022 on µTCP, but finally in the Summer of 2023, I motivated myself to push µTCP into a usable state. So far I've spent 25 days in 2023 on µTCP. Thanks to Tarides for supporting my work.

+

Since late August, we have been running some unikernels using µTCP, e.g., the retreat website. This allows us to observe µTCP and find and solve issues that occur in the real world. It turned out that the model is not always correct (i.e., there is no retransmit timer in the close wait state, which avoids proper session teardowns). We report statistics about how many TCP connections are in which state to an influx time series database and view graphs rendered by Grafana. If there are connections that are stuck for multiple hours, this indicates a resource leak that should be addressed. Grafana was tremendously helpful to find out where to look for resource leaks. Still, there's work to understand the behaviour, look at what the model does, what µTCP does, what the RFC says, and eventually what existing deployed TCP stacks do.

+

The Secondary Nameserver Issue

+

One of our secondary nameservers attempts to receive zones (via AXFR using TCP) from another nameserver that is currently not running. Thus it replies to each SYN packet a corresponding RST. Below I graphed the network utilisation (send data/packets is positive y-axis, receive part on the negative) over time (on the x-axis) on the left and memory usage (bytes on y-axis) over time (x-axis) on the right of our nameserver. You can observe that both increases over time, and roughly every 3 hours, the unikernel hits its configured memory limit (64 MB), crashes with *out of memory*, and is restarted. The graph below is using the `mirage-tcpip` stack.

+

+

Now, after switching over to µTCP, graphed below, there's much less network utilisation and the memory limit is only reached after 36 hours, which is a great result. Though, still it is not very satisfying that the unikernel leaks memory. On their left side, both graphs contain a few hours of `mirage-tcpip`, and shortly after 20:00 on Nov 23rd, µTCP got deployed.

+

+

Investigating the involved parts showed that a TCP connection that was never established has been registered at the MirageOS layer, but the pure core does not expose an event from the received RST that the connection has been cancelled. This means the MirageOS layer piles up all the connection attempts, and it doesn't inform the application that the connection couldn't be established. Once this was well understood, developing the required code changes was straightforward. The graph shows that the fix was deployed at 15:25. The memory usage is constant afterwards, but the network utilisation increased enormously.

+

+

Now, the network utilisation is unwanted. This was hidden by the application waiting forever that the TCP connection getting established. Our bug fix uncovered another issue--a tight loop:

+ +

This is unnecessary since the DNS server code has a timer to attempt to connect to the remote nameserver periodically (but takes a break between attempts). After understanding this behaviour, we worked on the fix and redeployed the nameserver again. On the left edge, the graph has the tight loop (so you have a comparison), and at 16:05, we deployed the fix, Since then it looks pretty smooth, both in memory usage and in network utilisation.

+

+

To give you the entire picture, below is the graph where you can spot the `mirage-tcpip` stack (lots of network, restarting every 3 hours), µTCP-without-informing-application (run for 3 * ~36 hours), DNS-server-high-network-utilisation (which only lasted for a brief period, thus it is more a point in the graph), and finally the unikernel with both fixes applied.

+

+

Conclusion

+

What can we learn from that? Choosing convenient tooling is crucial for effective debugging. Also, fixing one issue may uncover other issues. And of course, the `mirage-tcpip` was running with the DNS server that had a tight reconnect loop. But, below the line: should such an application lead to memory leaks? I don't think so. My approach is that all core network libraries should work in a non-resource-leaky way with any kind of application on top of it. When one TCP connection returns an error (and thus is destroyed), the TCP stack should have no more resources used for that connection.

+

We'll take more time to investigate issues of µTCP in production, plan to write further documentation and blog posts, and hopefully soon will be ready for an initial public release. In the meantime, you can follow our development repository.

+

We at Robur are working as a collective since 2018 on public funding, commercial contracts, and donations. Our mission is to get sustainable, robust, and secure MirageOS unikernels developed and deployed. Running your own digital communication infrastructure should be easy, including trustworthy binaries and smooth upgrades. You can help us continue our work by donating (select Robur from the drop-down or put "donation Robur" in the purpose of the bank transfer).

+

If you have any questions, reach us best via eMail to team AT Robur DOT coop.

+ diff --git a/data/planet/practicalocaml/-hello--world-.md b/data/planet/practicalocaml/-hello--world-.md new file mode 100644 index 0000000000..9eccb2030a --- /dev/null +++ b/data/planet/practicalocaml/-hello--world-.md @@ -0,0 +1,16 @@ +--- +title: '{ hello = `world; }' +description: And here we are! After writing my share of ReScript at Practical ReScript, + I figured I'd start a blog for OCaml that would help consolidate my experiences + with it into some Practical advice, that you can use to start new projects, to contribute + to existing ones, hell even get a +url: https://practicalocaml.com/hello-world/ +date: 2023-08-23T00:30:16-00:00 +preview_image: +featured: +authors: +- Practical OCaml +source: +--- + +

And here we are! After writing my share of ReScript at Practical ReScript, I figured I'd start a blog for OCaml that would help consolidate my experiences with it into some Practical advice, that you can use to start new projects, to contribute to existing ones, hell even get a job as with OCaml!

Since I don't write OCaml every day, sometimes I'll tag in other people to help out.

But today is just about saying hello 👋

Some of the subjects you can expect to read about here are:

And definitely on topics like:

So if you've got any ideas, feel free to post at me in X: @leostera

diff --git a/data/planet/practicalocaml/a-quick-guide-to-gadts-and-why-you-aint-gonna-need-them.md b/data/planet/practicalocaml/a-quick-guide-to-gadts-and-why-you-aint-gonna-need-them.md new file mode 100644 index 0000000000..8af17e8e83 --- /dev/null +++ b/data/planet/practicalocaml/a-quick-guide-to-gadts-and-why-you-aint-gonna-need-them.md @@ -0,0 +1,102 @@ +--- +title: A quick guide to GADTs and why you ain't gonna need them +description: Ever wanted to use a GADT but did not know if you really needed them? + You probably don't. And here's why. +url: https://practicalocaml.com/a-quick-guide-to-gadts-and-why-you-aint-gonna-need-them/ +date: 2023-08-28T13:46:43-00:00 +preview_image: +featured: +authors: +- Practical OCaml +source: +--- + +

I've been seeing some more posts about how to use and when to use GADTs. GADTs (Generalized Abstract Data Types, I pronounce them "gats" like in "cats" but with a "g") are an extension to regular ADTs that is usually reserved for very specific scenarios, but its not always clear which those are and why.

So I figured I'd give this a shot, and write a super small primer on them, by example. We're gonna write a library that didn't need to use GADTs, and along the way we're gonna feel the pains that come with GADTs, and what specific things they are amazing for.

Buckle on to your camels! 🐫

GADTs by Example

Alright usually you'd write your variant as:

type role = 
+  | Guest of guest
+  | User of user

and use it as User(user) or Guest(guest). You can think of these constructors as little functions that go from some arguments to a value of type role. So really Guest "has type" guest -> role. And User has type user -> role.

A GADT will let you change (a little) the return type of these constructors. So let's see what our role example looks like with GADT syntax.

type role =
+  | Guest: guest -> role
+  | User: user -> role

Neat, right? I really like this syntax.

But in this case, our role type can't be segmented or parametrized. I mean you can just have role, it's not like an option or a list where you can have an int option or bool list and those are more specific types of option or list. This means we can really only return role in any of our constructors, so you probably don't need GADTs.

Let's look at an example that does not need GADTs but uses them anyway.

A Validation Library

We'll make a validation type that we can use to mark things as validated throughout our app:

type _ validation =
+  | Valid: 'thing -> 'thing validation
+  | Invalid: 'thing * string -> 'thing validation
+  | Pending: 'thing -> 'thing validation

Note how using our constructors returns different types. If you use Valid("hello") you get a string validation, if you use Invalid(2113, "not cool number") you get an int validation, and so on.

If we try to make some helper functions they may look like this:

let make : 'thing -> 'thing validation =
+  fun x -> Pending x
+ 
+let get : 'x validation -> 'x =
+  function
+  | Pending x -> x
+  | Valid x -> x
+  | Invalid (x, _) -> x
+  
+let errors : 'x validation -> string option =
+  function
+  | Invalid (_, err) -> Some err
+  | _ -> None 
+  
+let is_valid : 'x validation -> bool =
+  function
+  | Valid _ -> true
+  | _ -> false

You can imagine how we'll have to check every time we want to open up a validation, to see if its pending, valid, or invalid. This means other devs will have to remember to check if the validation passed before using the value.

I don't know about you but I'm 100% certain I will forget to do that at least once.

GADTs can help us here to reduce the space of all the possible types that our variant constructors create. Right now, we can essentially create any <type> validation by just passing the right value to the constructors. But we could change that, so that you can statically check a value has passed, is pending, or has failed validation. Our new GADT could look like this:

(* we'll make some abstract types to use for differentiating
+   the validation states *)
+type pending
+type failed
+type valid
+
+(* our new validation GADT *)
+type _ validation =
+  | Pending: 'thing -> pending validation
+  | Valid: 'thing -> valid validation
+  | Failed: 'thing * string -> failed validation

This means that our functions can have restricted type signatures and smaller implementations. The compiler now knows that there is only one possible type that matches the Valid constructor, so we can't consider the others.

let make x = Pending x
+
+let get (Valid x) = x
+
+let errors (Fail (_, err)) = err

Great! The downside is that this code doesn't actually type-check.  You can't pattern-match and get a value out of Valid x because the compiler "forgot" what type that value had. Let me show you what I mean. This function:

let get (Valid x) = x

Fails to type with this error:

File "lib/gadt.ml", line 18, characters 20-21:
+18 | let get (Valid x) = x
+                         ^
+Error: This expression has type $Valid_'thing
+       but an expression was expected of type 'a
+       The type constructor $Valid_'thing would escape its scope

And the type of x in the error is $Valid_'thing, which is a weird type. The compiler yells that it would escape its scope. That's how OCaml tells us "Hey I know there should be a type here but I...erhm...don't know anymore what that type *actually* was. So, yeah, can't let you use it. Sorry".

So how does one get this value out?

Turns out that while the compiler won't let this type escape, if you put many things together inside the same constructor, it will remember if the type was the same across all of them. For example, the compiler is completely happy here:

(* we introduce a function in our Valid arguments *)
+type 'validity validation = 
+  | Valid: 'thing * ('thing -> bool) -> valid validation
+  | ...
+  
+let get_that_bool (Valid (x, fn)) = fn x

because it understands that once you pack together a 'thing and a 'thing -> bool, then it's the same 'thing.  So this will work for any type.  And that's both quite powerful and also super non-obvious at first. Like, what is this useful for?

GADTs can help us hide type information, but still be able to use it later. In the last issue of Practical OCaml we created a route type for our web router that uses this pattern to hide the types that different route-handler functions use as inputs, and it lets us put together into a single list, a bunch of routes that have type-safe parameters/body parsing. Pretty cool.

Anyways, back to our question, to get our Valid value out, we will need to either:

We want to preserve the type of our value, so we're gonna do the first. Letting our value escape means actually putting 'thing in the return type of our constructors. Like this:

type _ validation =
+  | Valid: 'thing -> (valid * 'thing) validation
+  | ...

That's actually all we need. Now the compiler can infer the signature of our get function is (valid * 'thing) validation -> 'thing, and it lets us take that 'thing out. BAM. Done.

And yet our validation solution still doesn't help us actually validate anything. We don't have a function that goes from pending to valid, or from pending to invalid. Since our Pending variant doesn't know what a 'thing is, it also doesn't know how to validate it.  We'll start there:

(* we added a `fn` to our Pending constructor *)
+type _ validation =
+  | Pending: 'thing * ('thing -> bool) -> pending validation
+  | ...
+ 
+let validate (Pending (x, fn)) =
+  if fn x
+  then Valid x
+  else Invalid (x, "invalid value!")

We run the compiler, and see the same issue as before: Valid x would have type $Pending_'thing, because our Pending variant doesn't really expose it's internal 'thing type... yadda yadda...we can fix that too by letting 'thing escape:

type _ validation =
+  | Pending: 'thing * ('thing -> bool) -> (pending * 'thing) validation
+  | ...

Aaaand now we run into another issue. Oof. Valid x and Invalid (x, "invalid value!") have different types 🙈 – this is a very common "dead end".

For now, we are going to wrap 'em up in a result and it will push the problem to future you and me:

let validate (Pending (x, fn)) =
+   if fn x
+   then Ok (Valid x)
+   else Error (Invalid (x, "invalid value!"))

So now we can use our Extremely Type-Safe Validation Lib:

let _ =
+  let user_value = make 2113 (fun x -> x > 0) in
+  match validate user_value with
+  | Ok value ->
+      let age = get value in
+      print_int age;
+  | Error err ->
+      let err = errors err in
+      print_string err;
+

Hopefully implementing this has shown some of the reasons why GADTs while powerful are rather painful to work with.

For completeness's sake here's the full code:

type valid
+type invalid
+type pending
+
+type _ validation =
+  | Pending : 'thing * ('thing -> bool) -> (pending * 'thing) validation
+  | Valid : 'thing -> (valid * 'thing) validation
+  | Invalid : 'thing * string -> invalid validation
+
+let make x fn = Pending (x, fn)
+let get (Valid x) = x
+let errors (Invalid (_, err)) = err
+
+let validate (Pending (x, fn)) =
+  if fn x then Ok (Valid x) else Error (Invalid (x, "invalid value!"))

Conclusion: You Don't Need GADTs

Truth is that unless you are Jane Street and need to optimize the hell out of your compact arrays, or are writing a toy λ-calculus interpreter, you're probably better off without them.

GADTs can be super useful if you need to:

  1. hide type information
  2. restrict the kind of types that can be instantiated
  3. have more control over the relation between the input and return type of a function

But GADTs are not only hard to pronounce, they also come with a host of problems. The ones we've seen, and some more that we haven't that need solutions with wizardly names like locally abstract types or polymorphic recursion. Learning about this is fun and great, but sometimes can get in the way of shipping without substantially improving the quality of your product or developer experience.

So stick to simpler types until you run into one of those 3 problems and I promise you you'll be a productive, happy camelid 🚀

Have you implemented typed state machines in some other ways? Have anything to add or challenge? I'd love to hear it! Join the x.com thread.

Happy Cameling! 🐫

Thanks to @patricoferris for pointing out that if you do implement the above pattern, but move outside the current module (for ex. have a submodule for your valid, invalid, pending types), you may run into some undecidability problems that make pattern-matching non-exhaustive. Oof, many words. The gist is, if you see a "This pattern is non-exhaustive" error, try adding a private constructor to your type-tags:

type valid = private | Valid_tag
+type invalid = private | Invalid_tag
+type pending = private | Pending_tag

For a more detailed answer, check out this OCaml forum post.

diff --git a/data/planet/practicalocaml/how-i-explore-domain-problems-cheaply-and-fast-with-ocaml-modeling-a-web-router.md b/data/planet/practicalocaml/how-i-explore-domain-problems-cheaply-and-fast-with-ocaml-modeling-a-web-router.md new file mode 100644 index 0000000000..9cc961925b --- /dev/null +++ b/data/planet/practicalocaml/how-i-explore-domain-problems-cheaply-and-fast-with-ocaml-modeling-a-web-router.md @@ -0,0 +1,16 @@ +--- +title: 'How I explore domain problems cheaply and fast with OCaml: modeling a web + router' +description: "You've heard of Domain-Driven Design, now buckle up for Type-Driven + Domain..wait. Typed Domains Driving...nevermind. We're gonna use Only Types to Understand + our Domain Problems Very Fast! \U0001F680" +url: https://practicalocaml.com/how-i-explore-domain-problems-faster-and-cheaply-in-ocaml/ +date: 2023-08-24T13:29:21-00:00 +preview_image: +featured: +authors: +- Practical OCaml +source: +--- + +

Hello folks! Starting out the blog with a topic that I love: domain modeling.

Domain modeling is the art and science of figuring out how to map some messy, fuzzy, real-life ideas and things, into a computer program that we can execute.

It is usually easier to say than it is to do, so I figured I'd give you an example of how I've done domain modeling in the past and how I like to explore domain problems through it.

Shapes of Things

There's only so many kinds of data we can have in our programs. You have single things, you have collections of the same things. You have collections of different things that also happen to be a thing, and they can either be one of many things that are the same thing, or many things together making a thing!

Where I'm going with this is that the shapes of data that you normally work with come in a few packages.

We have many things that belong together but are distinct on their own. In OCaml we call these variants.

We have many things that belong together and form a single unit, where every piece has its own place, and the place doesn't have a name. In OCaml we call these tuples. But when these pieces don't have a place and instead have a name, in OCaml we call these records.

We have things that exist on their own and we don't know much about them. In OCaml we call these abstract types.

We have things that don't tell us everything that they are, but that can hide information from us. In OCaml we call these generalized abstract data types (GADTs, and I pronounce it like "cats" but with a G, try it out loud, its cool, no-one can hear you).

We have things that are collections of other things. Lists, arrays, hash tables, sets, queues, heaps, tuples.

And in fact, we can create most of these different shapes of data with some of the simpler ones. Records can made with tuples. Lists can be made with variants. And so on.

Okay, enough of this. Let's start using these shapes for some specific domain problems.

Modeling a Web Router

We'll start with one that most of you will likely be familiar with: a web router. That is a router that helps a web framework figure out where to send each request. There are many out there, and I'm not pitching you to write your own (but you should, because it's a good way to learn!).

But what really is a web router? It's a collection of patterns and handler functions. Not unlike a match expression really. It matches the pattern against a web request object, and if it succeeds it will execute the function that corresponds to it.

So we can start by defining what we know:

alt

Brilliant! Now we have our types in place, we can start exploring how they interact with each other.

A router typically will receive some form of request and turn it into a response. After all, we expect to reply to our users with something.

So then, to make a response, we need  to find a handler. We can do that by matching against every route until a pattern matches. When that happens it expects to receive a response.

Now slowly we are building up the right vocabulary not just around the problem, but also in the code that deals with it.

alt

Notice how we create a few new types for request and response, which are new Things we are working with.

We also created two new functions, one for matching a pattern against a request called matches; and a second one called route to create a response from a router and request.

And that's it. We have our first model for a router. We have a clearer understanding of what the moving pieces are, and how they connect together.

From here we can take it in many directions, but what I like to do is to do a second pass and challenge the model.

Challenging the model

In the process of challenging, we want to grab individual pieces and ask what's important about them, and how are they different than other things, and why are they really needed.

For example, why is a pattern a separate entity and not just a behavior of a handler? A handler could well ignore a request and just let the next handler handle it.

This would lead to a slightly different model, where a handler either tells us it has handled or ignored something, or the handler itself calls the next thing.

In the first case, we can model it by making a new type of that can be either an ignored handler result, or a handled handler result:

alt

This leads naturally to some implementations, such as folding over the list of routes, and bailing as soon as we find a route that returned Handled(res). This is super flexible when it comes letting the route itself decide how or if it will process a request.

But in the second case, we can see we have an even more powerful model. In this one we are making sure every handler receives the next handler, which it can call at any point, any number of times. This is what this second model looks like:

alt

This model leads to a recursive implementation, where we have to build our handlers in advance, so that the calls to next go in the right order. This can be much trickier than the prior models we saw.

Refining the Model

Once we find a model that we like, and in this case we'd like to stick with the first one, we can start doing some refinements.

Refining is the process of adding detail to the model, and it helps us see how it can materialize as a working application.

For example, we can take our pattern type and start looking into what shapes it can actually take. Usually, a domain expert here is the best person to ask: "what really is a pattern?"

In our case, we want to be able to match on the route URL or path; the kind of HTTP method they are using, or verb; and we'd like to know what is in the body.

To do this we expand our pattern type once to include some data, and in the process we define a new type for the HTTP method, since we knew we needed that and we roughly understand upfront the shape it has: it can be one of some options. The new pattern now looks like this:

alt

Excellent, but now what exactly happens in the body?

As it is above, it can either be present and be a string, or be not present. If it is Some(string) then either an empty string "" and the entire works of Shakespeare in Korean would be valid bodies. Is this really what we mean to say?

Here's where our refining doubles down, and asks if there's anything special about the body in this specific pattern, or in this specific route. So we're relating the current refining learnings with our past learnings.

Turns out the body should actually be something that the handler can in fact handle, so we need somehow to make it fit into what the handler expects.

So does the handler really expect a request? Or does it expect a specific kind of request? Let's see if we can be more specific in a few steps:

  1. Let our pattern be more specific about a request payload
  2. Make our handler be specific about the request payload
  3. Make our router work with our new handler

We will start by making our pattern take type parameter. At this point a type parameter usually means "here's a kind of data that is really a much larger group of data, where there are subgroups of it that can't be mixed".

alt

BUT there's a big problem here. We can't really create the pattern ahead of time, knowing what the payload will be like.

A pattern really is a specification for how to match against requests. So instead, we need to provide a way of reading the body into the 'payload type. Thankfully, we have first-class functions in OCaml, so this is an easy fix.

alt
Notice how our body now becomes a function that will receive a string and try to return a 'payload. If it can't, the it can always return an option. In practice we would probably use a result type here, but for the sake of this post an option is good enough.

Next up, we have our handler, which now should receive a type parameter for our payload and look a bit more like this:

alt
Our handler function type now receives a payload before a request.

And finally, it seems that our route and router type doesn't need much amending. Because we really just need a list of patterns and handlers, and that's exactly what they are, right?

Right?! 🙈

alt

Oh no. If we follow this current refinement and thread in a 'payload parameter to our route type, we will end up with a single type of payload in the list of routes. This is because the list type can only hold one type of elements, and every 'payload route is essentially a new type!

So we can either backtrack, and move this body parsing function inside the handler, to let the handlers figure out how to work with it. Or we can find another way of putting all these handlers together in a list, while maintaining the model as close to the domain.  

For this, we can use a special type of type OCaml has, that lets us hide information. The gist is this:

alt
Using a GADT to capture a route with a pattern and a handler, but hiding their payload parameter. {

Damn, there we go! 🔥 Now we have all the information we want and it seems to be nicely encapsulated in this route type.

This model actually leads to a rather complex implementation, because every time we unpack the Route, we must make use of both the pattern and the handler at the same time. That's the only requirement for using this information-hiding pattern: you can peak, but you can't leak the information.

For completeness sake, here's a small implementation that follows our model:

alt

Conclusions from Modeling a Router

Like this, we've quickly gone through several iterations of our model, tried to understand better what problem we are trying to solve, what are some of the constraints it has, and how our model leads to different implementations.

It is very important to understand that this first implementation is meant to be correct, and not necessarily optimal. But it can make a great first implementation to test things against, and eventually, help you optimize making sure you are not breaking good behavior!

I'd love to go on with some more examples, like:

  1. modeling regulatory compliance for betting companies
  2. modeling the publishability window of content in the music industry following geographic restrictions
  3. modeling the optimal publishing of photography content to a social network
  4. modeling an offline-first graph database for the edge
  5. and more!

But we're already over 2,000 words and I'd like you to get a glass of water and maybe stretch your legs. So let me know which modeling example you'd like to see in a next post.

If you liked this, please subscribe so you get the next issue of Practical OCaml right in your inbox, and share it with your camel friends on lobste.rs, hackernews, x.com, and so on.

Have you implemented typed state machines in some other ways? Have anything to add or challenge? I'd love to hear it! Join the x.com thread.

Happy Cameling! 🐫

diff --git a/data/planet/practicalocaml/how-to-build-type-safe-state-machines-using-type-state.md b/data/planet/practicalocaml/how-to-build-type-safe-state-machines-using-type-state.md new file mode 100644 index 0000000000..26ae4a0b78 --- /dev/null +++ b/data/planet/practicalocaml/how-to-build-type-safe-state-machines-using-type-state.md @@ -0,0 +1,117 @@ +--- +title: How to build type-safe State Machines using type-state +description: Tired of writing state machines full of invalid transitions? Type-state + may be what you're looking for. In this issue of Practical OCaml we show you how + to use it to build type-safe state machines. +url: https://practicalocaml.com/how-to-build-type-safe-state-machines-using-type-state/ +date: 2023-08-29T10:29:59-00:00 +preview_image: +featured: +authors: +- Practical OCaml +source: +--- + +

This will be a short one, but I hope it'll make you want to go refactor everything.

There are a lot of ways of writing state machines in typed languages, all varying in the degree of type-safety. Sure you can put everything in a record full of this option or have one variant per state and a bunch of repeated things...but today I wanna show you a way of doing state machines with something called type-state.

What this buys you is that you can offer a nice uniform API for your state machines while keeping the internal states cleanly separated.

Let's start from the beginning.

What is type-state?

Type state is kind of a weird term. You don't really have state in your types, right? Like you don't have a counter that keeps incrementing.

type counter = int
+let inc : counter -> counter = fun x -> x + 1
+
+let one: counter = inc 0
+let two: counter+1?  = inc one
+
Look ma! I made a counter that counts, but you can't see how much it counts on its type. But it's counting, I promise.

You can bend backwards to do this with some type schemes (which is a fancy word for "how to do something" or "pattern" that you may read around). Like a common way of doing this is to use type-params to keep adding types to something. For example:

type zero = Zero
+type 'a inc = Inc of 'a
+
+(* our `inc` function wraps whatever in an `inc` type *)
+let inc : 'a -> 'a inc = fun x -> Inc x
+
+let one: zero inc = inc Zero
+let two: zero inc inc = inc one
+let three: zero inc inc inc = inc two

And this sort of thing can be suuuper useful if you want to statically validate something. For example, let's say you have a fuel type and you can only accelerate your car if you have enough fuel. And enough fuel is defined as "one unit of fuel" or in types as "it's wrapped by one fuel type".

So we can start with a car without fuel, fuel it up, and then consume the fuel. And in the next example, you can see how the type annotation matches the amount of fuel a car has.

type no_fuel = No_fuel
+type 'a fuel = Fuel of 'a
+
+let fuel_up x = (Fuel (Fuel x))
+
+let run (Fuel x) = x
+
+let empty_car = No_fuel
+let full_car: no_fuel fuel fuel = empty_car |> fuel_up
+let full_car: no_fuel fuel = run full_car
+let full_car: no_fuel = run full_car
+
+(* this last one will be a type error! *)
+let full_car: no_fuel = run full_car
In this example we statically track the amount of fuel by using a fuel type that is essentially a counter. When we fuel up the counter goes up, when we run the counter goes down. We can only call run on a car with at least one fuel.

This fails because the last full_car that worked becomes a car with no fuel, and our run function requires a car with fuel.

But alas, this can get super complex quickly because:

  1. We're not used to this kind of programming in the types (unlike in programming languages like Idris or TypeScript)
  2. We don't have good debugging tools for this, and type errors can become strange quickly, especially if we use polymorphic variants, objects, or GADTs.

Okay, there's more to say about type-state, but this should be enough for now: type-state lets you rule out certain behaviors by putting in your types, information about the values.

Moving on...

Type-state state machines

Alright, we're ready to go. The pattern is pretty straightforward:

  1. We need a type for our thing, which will be a state machine
  2. We need a type parameter for the state the machine is in
  3. We want to save that state as a discrete value in our state machine type
type 'state fsm = { state: 'state }

That's it. That's the pattern. If it seems small it's because it is, but there's so much power to this pattern! Let's explore with an example.

Requesting Permissions as a Type-state machine

We'll build a tiny Permissions module that will help us check if a User has the right permissions to access a resource. There will be 3 states: Requested, Granted, and Denied. We'll always start on Requested, and we can move to Granted or Denied. If we are on Granted we should have access to the resource itself, if we are on Denied we should have access to some reason for why we were denied access.

So we start with our basics, the pattern:

type 'state t = { state: 'state };

Next, we're going to add the 3 states as distinct types:

type id
+type scope
+
+type 'resource granted = { resource : 'resource }
+type denied = { reason : string }
+type requested = { scopes : scope list }

Let's put this together with our t type. We will need to introduce a new type parameter for the 'resource, so we know what 'resource to use when we create our 'resource granted state. We'll also add some more metadata that is specific to a permission request but is shared across all states.

type ('state, 'resource) t = {
+  (* the state of the permission request *)
+  state : 'state;
+  (* other shared metadata *)
+  resource_id : id;
+  user_id : id;
+}

And now we can build our API on top of this, using our 'state type to guide the user to the functions they can use:

  1. We want to create a new Permissions Request that will be  requested t
  2. We want to call a function that returns either a granted t with our resource, or a denied t with a reason
  3. If we get a denied t we want to be able to see the reasons
  4. If we get a granted t we want to be able to use the resource.

Let's get to work!

We'll start with a constructor function, and a function to transition to our final states:

let make ~resource_id ~user_id ~scopes =
+  { state = { scopes }; resource_id; user_id }
+
+let request_access t =
+  match run_request t with
+  | Ok resource -> Ok { t with state = { resource } }
+  | Error reason -> Error { t with state = { reason } }

The basic machinery is done. We create, and the type system will infer correctly that the state should be requested, because a requested record includes scopes.

Then, our request_access function will return either (granted, 'resource) t or a (denied, 'resource) t wrapped in a result. We can use any variant for this, even a Future, but a result is already present so we'll go with that here.

Great, the next step is implementing our operations:

(* extract the reason from a `denied` state *)
+let reason { state = { reason }; _ } = reason
+
+(* do something with the resource in a `granted` state *)
+let with_resource { state = {resource}; _ } fn = fn resource
+
+(* get the resource out of a granted permission *)
+let get { state = {resource}; _ } fn = resource

And done. The types get inferred nicely here as well because the records are all disjoint. Now we can use our little state machine:

(* this would be our resource *)
+module Album =  struct
+  type t = string
+  let print = print_string
+end
+
+let _ =
+  let req: (_, Album.t) Permission_request.t =
+    Permission_request.make
+      ~resource_id:"spotify:album:5SYItU4P7NIwiI6Swug4GE"
+      ~user_id:"user:2pVEM9qgPvPeMslgnGDDOr"
+      ~scopes:[ "listen"; "star"; "playlist/add"; "share" ]
+  in
+
+  match Permission_request.request_access req with
+  | Ok res ->
+      Permission_request.with_resource res Album.print;
+      let album = Permission_request.get res in
+      Album.print album;
+  | Error res ->
+      print_string (Permission_request.reason res)

Pretty neat, right?

For completeness sake, here's our Permission_request module:

module Permission_request = struct
+  type id = string
+  type scope = string
+  type 'resource granted = { resource : 'resource }
+  type denied = { reason : string }
+  type requested = { scopes : scope list }
+
+  type ('state, 'resource) t = {
+    (* the state of the permission request *)
+    state : 'state;
+    (* other shared metadata *)
+    resource_id : id;
+    user_id : id;
+  }
+
+  let make ~resource_id ~user_id ~scopes =
+    { state = { scopes }; resource_id; user_id }
+
+  (* TODO(@you): you can implement here the logic for checking
+   * if you actually have permissions for this request :)
+   *)
+  let run_request : (requested, 'resource') t -> ('resource, string) result =
+   fun _t -> Error "unimplemented!"
+
+  let request_access t =
+    match run_request t with
+    | Ok resource -> Ok { t with state = { resource } }
+    | Error reason -> Error { t with state = { reason } }
+
+  let reason { state = { reason }; _ } = reason
+  let with_resource { state = { resource }; _ } fn = fn resource
+  let get { state = {resource}; _ } = resource
+end

Conclusions: Type-state is Great

Type-state is just another tool in your bat-belt to build great APIs with type-safety, and good ergonomics.

It has a cost, like everything else, but it enables you to grow your states and maintain them separately by using submodules, in a very natural way. After all they are different types!

I picked up this pattern from Rust libraries that model the state of sockets, database connections, and many other things, by doing exactly the same thing. Of course, having traits in Rust means we can extend the methods for a specific type-state, which means narrowing down even further the information you have to process when you go type req. and get the autocompletion list.

But at least in OCaml we can implement the pattern safely and maybe with time our autocompletion will get smarter and do the same filtering for us!

That's it. That's type-states for OCaml.

Have you implemented typed state machines in some other ways? Have anything to add or challenge? I'd love to hear it! Join the x.com thread.

Happy Cameling! 🐫

diff --git a/data/planet/practicalocaml/unix-module-considered-harmful.md b/data/planet/practicalocaml/unix-module-considered-harmful.md new file mode 100644 index 0000000000..c37d878004 --- /dev/null +++ b/data/planet/practicalocaml/unix-module-considered-harmful.md @@ -0,0 +1,26 @@ +--- +title: Unix Module Considered Harmful +description: 'Recently I was working on a socket pool for a new scheduler for OCaml + 5 (multicore baby!) and I ran into a strange issue. + + + This new socket pool works by spinning up a series of lightweight processes to accept + connections. Every one of those will wait for a client to' +url: https://practicalocaml.com/unix-module-considered-harmful/ +date: 2023-11-29T07:19:43-00:00 +preview_image: +featured: +authors: +- Practical OCaml +source: +--- + +

Recently I was working on a socket pool for a new scheduler for OCaml 5 (multicore baby!) and I ran into a strange issue.

This new socket pool works by spinning up a series of lightweight processes to accept connections. Every one of those will wait for a client to connect, and create a new lightweight process to handle a connection. Eventually, the client will terminate the connection and the relevant processes are terminated.

All good so far.

All of this accepting and connecting is done via file descriptors (a Unix.file_desc). In some cases they correspond to listening sockets, when used to accept new connections, and when connected to a client they become streaming sockets (so a socket used to send/receive data). But really all you have is an integer that's behind the Unix.file_desc type: the Unix file descriptor.

Okay, so what went wrong?

In one of my load tests, I consistently could reproduce that the entire application would just exit. No error messages, no prints, no stack traces. It was running and then at some point, it just wasn't.

I can't emphasize enough how much I dug through the entire runtime, adding more logging, and more safety nets, just to see if I was doing something wrong. A good day of work was lost to this.

Then asking around, after exploring all the options I could think of, I asked on the #multicore channel of OCaml Labs, and I got an answer from Stephen Dolan.

Turns out that:

🤦‍♂️

No return value, no exception, nothing of the sort. You have this entirely out-of-band input to your program that even in an impure functional language like OCaml feels like a sucker punch.

Why does this happen? Let's see.

The Unix module

The Unix module is the default way to interact with your operating system in OCaml. You've probably used Lwt_unix before or the -unix flavor of your favorite lib if you aren't using promises yet. All of those rely on Unix.

But really, this module is just super low-level bindings to syscalls.

🐉
Here be Dragons. We're digging deeper than usual here, so here's a little sword in case we find something dangerous: 🗡️

Syscalls, or "system calls", are little bridges between the boundaries of User space and Kernel space in your operating system:

And our Unix module is full of bindings to syscalls like write(2) that lets User space programs actually write files by asking Kernel space code to do the writing. Neat, right?

The fact that were are using these syscalls isn't obvious, but as you can see here in this snippet for Unix.write we are making an external call to a function called caml_unix_write:

(* lowest-level binding, directly calling C code *)
+external unsafe_write : file_descr -> bytes -> int -> int -> int
+                      = "caml_unix_write"
+
+(* slightly-higher level binding, that checks the buffer offset is ok *)
+let write fd buf ofs len =
+  if ofs < 0 || len < 0 || ofs > Bytes.length buf - len
+  then invalid_arg "Unix.write"
+  else unsafe_write fd buf ofs len

caml_unix_write will in turn call a C function called write which comes from libc on Unix-like operating systems that follow the POSIX standard, and will call WriteFile from the Windows APIs when compiling on Windows.

write from libc, and WriteFile from the Windows APIS. Those are the syscalls.

🙈
If I've lost you already because you wanted to learn about OCaml and now we're talking about C, then you will understand why I'm frustrated about this whole thing.

The important thing to know is that when you are using this module, many of the functions you will call there are not OCaml code. They are C code, and they reach into the depths of your operating system to do dangerous, wonderful, weird things.

On Unix systems, one of those is signals.

Unix Signals

Unix has a way of interrupting a process with a mechanism called signals. A process in turn can tell Unix how it's going to react to those signals, by setting a signal handler.

It's essentially a configurable, OS-triggered callback.

Some of these signals are very common. Like when you press Ctr+C to exit a long-running program, you're really sending a SIGINT signal, also known as an interrupt signal.

You can of course override this, and you see many REPLs do it, so that if you accidentally press Ctrl+C you get a chance to confirm this and exit or return to the program.

Signals, however, are not a part of the Unix module. If we want to configure them (and their handlers) we need to use the Sys module.

⁉️
What is the Sys module? It's a bag of sort of random stuff, and a few things that probably deserve to be in a module called Sys like what OS you're on. If you ask me, I'd rather we didn't have a Sys/Unix module at all, and just had proper abstractions for File, Socket, OS, Env, Process, etc. But c'est la vie. In the meantime, we have

In particular, we need to use the Sys.set_signal. This function lets you set the behavior for a particular signal, which can be one of:

Fixing The SIGPIPEs

The error we had described before is fixed with a single line of OCaml at the top of our program:

Sys.(set_signal sigpipe Signal_ignore);;

Mark the SIGPIPE signal to be ignored.

But the knowledge required to put that line there isn't trivial.

You need to know that the Unix module is just a wrapper around OS syscalls. And in here you'll want to know exactly which one, which may involve digging through some of the OCaml C libraries.

You need to know where to find the right doc for that syscall (is it BSD since macOS inherited a lot from it? That doesn't mention anything about SIGPIPEs, maybe the Linux syscall manual is relevant here?

alt
Linux system manual saving the day

And then you have to learn about Signals, how to catch them, and how to use the Sys module to do that. Granted this last part is the easiest since it's more actionable, but that second step?! Not as easy a leap to make.

Conclusion

This is most definitely not the kind of surprise you want to find when writing a type-safe, high-level functional programming language like OCaml.

Hell, I think Python does this better by throwing an IOError instead. That would've saved me hours of self-doubt.

If you really need this level of control, you may find it useful to mentally frame it as writing garbage-collected C, and behave accordingly. And please shield your users from all the gory details.

Otherwise, stay happy and away from the Unix module and look for alternatives. Use Bos for your OS interactions, stick to a higher-level library for sockets, and if it comes to it, isolate that part of your system.

I hope this gotcha won't get you the next time you're writing network code, and if you have any stories like this one, I'd be happy to share them on Practical OCaml too.