prox part 1 — type level programming in Scala

Intro

I started writing prox at the end of 2017 for two reasons. First, I never liked any of the existing solutions for running external processes and capture their input/output streams. And I just returned from the scala.io conference full of inspiration; I wanted to try out some techniques and libraries and this seemed to be a nice small project to do so.

Since then, prox has been proved to be useful, we are using it at Prezi in all our Scala projects where we have to deal with external processes. The last stable version was created last September, built on the latest cats-effect and fs2 libraries.

This is the first part of a series of blog posts dedicated to this library. In the first one, I’m going to talk about shapeless and type level programming techniques that are used to create a strongly typed interface for starting system processes. In future posts, I will explore replacing its dependencies such as using akka-streams instead of fs2 or ZIO instead of cats-effect. These different versions will be a good opportunity to do some performance comparison and to close the series with creating a new version of the library which is easier to use in the alternative environments.

Limiting redirection

When I started writing the library I wanted to explore how I can express some strict constraints on the type level:

• A process can have its input, output and error streams redirected, but only once
• Processes without redirected output can be piped to processes without a redirected input

In prox 0.2.1 a single system process is described by the following type:

but let’s focus first on the requirement to be able to redirect one of the streams maximum once. This is encoded by the IRS, ORS and ERS type parameters, which are all have to be subtypes of RedirectionState. RedirectionState is a phantom type; there are no values ever created of this type, it is only used in type signatures to encode whether one of the three streams are already redirected or not:

So for example with a simplified model of a process, Process[IRS <: RedirectionState, ORS <: RedirectionState, ERS <: RedirectionState], using the output redirection operator > would change the types in the following way:

How can we restrict the redirect function to only work on Process[_, NotRedirected, _]? We can define it as an extension method with an implicit class (once again this is a simplified version focusing only on the redirection state handling):

By forcing the ORS type parameter to be NotRedirected and setting it to Redirected in the result type, we can guarantee that this function can only be called on a process that does not have their output redirected yet. The target of the redirection is extensible through the CanBeProcessOutputTarget type class, as we will see later.

Dependent types

Reality is much more complicated, because of process piping and because the process types encode the redirection result types too. Let’s get back to our > function and see how we could modify it so it works with piped processes too. Anyway, how is process piping encoded in this library?

Two processes connected through a pipe are represented by the PipedProcess class. Both Process and PipedProcess implements the following trait:

We’ve already seen Process. PipedProcess is a bit more complicated:

To make > work on both, we can start by modifying its definition to work on any ProcessNode not just Process (omitting the output type params for now):

This has a serious problem though. The output type is ProcessNode and not the “real” process type, which means that we lose type information and all the other dependent typed operations will not work. We have to make the result type depend on the input!

We may try to use the RedirectionOutput type class like this:

Here the result (redirectOutput.Result) is a path dependent type. This may work in some simple cases but have two serious issues:

• It is not possible to use redirectOutput.Result in the parameter block of the function, so if another type class needed it as a type parameter we could not pass it.
• Further implicit resolutions and type level operations will quickly break as the compiler will not be able to unify the various path dependent types

The Aux pattern, used heavily in the shapeless library provides a nice pattern for fixing both problems. We start by defining a type class for describing the operation, in this case redirecting the output channel of a process:

The type class itself is straightforward. We have to implement it for both Process and PipedProcess set the Result type accordingly, then implement apply that sets up the actual redirection. But what the Aux type is for?

It solves the problems with the path dependent version if we use it like this:

By lifting the Result from the type class instance to a type parameter the compiler can now “extract” the calculated type from redirectOutput.Result to the > function’s Result type parameter and use it directly, both for other further type requirements or as we do here, in the result type.

This is the basic pattern used for all the operations in prox. You can check Luigi’s short introduction to the Aux pattern for a more detailed explanation.

Starting the processes

So far we just combined purely functional data structures in a complicated way. The result value may encode the launching of several system processes that are connected via pipes to each other and possibly other streams as we will see.

When we eventually decide to start these processes, we need a way to observe their status, wait for them to stop, get their exit code, and to access the data sent to the output streams if they were redirected. And we need this per process while launching the whole process graph in a single step.

First, let’s model a single running process:

and ProcessResult that represents an already terminated process:

Now we need to define a start extension method on ProcessNode that returns somehow one well-typed RunningProcess for each system process that it starts.

Let’s forget for a second about having multiple processes piped together and just consider the single-process case. For that, we would need something like this (the Out parameter is needed only for piping so I omitted it):

Now we can see why Process has those additional type parameters. It is not enough to encode whether the output and error channels were redirected or not, we also have to encode the expected result type of redirecting these. By storing these types in type parameters of Process we can easily imagine that by using the pattern described in the previous section, the result type can depend on what we redirected the process to.

Let’s see some examples of what this means!

• For a file system path, the result type is Unit, the redirection happens on OS level
• For a sink, the result type is Unit, only the sink’s side effect matters
• For a pipe with monoid elem type, the stream is folded by the monoid, the result type is T
• For a pipe with non-monoid elem type, the stream captures the elements in a vector, the result type is Vector[T]
• For a custom fold function, the result type is the function’s result type

The CanBeProcessOutputTarget type class we’ve seen earlier defines both the stream element type and the result type:

ProcessOutputTarget contains the actual IO code to build the redirection of the streams, I won’t get into details in this post. Note that there are similar type classes for error and input redirection too.

For two processes piped together we have to provide two RunningProcess instances with the proper result type parameters. So we can see that it is not enough that the redirection stores the result type in the process type, the start method must be dependent typed too.

One way to encode this in the type system would be something like this (simplified):

We encode piped processes with tuples of RunningProcess and single process with a single RunningProcess. To implement this we can make use of the shapeless library’s HList implementation.

HLists are heterogeneous lists; basically similar to a tuple, but with all the “usual” list-like functions implemented as dependent typed functions. Its type describes the types of all its elements, and you can split it to head/tail, append two, etc. And we can do it both on the type level (computing the result type of appending two HList’s, for example) and on the value level (appending the two values creating the third HList value).

We can implement the start method more easily by building a HList, while still keep the desired interface as shapeless implements a conversion from HList to tuples.

We can define two separate start functions, one producing HList and another the tuples (IO related parameters omitted):

The Start type class calculates both the tupled and the HList version’s result type. The implementation’s responsibility is to start the actual system processes and wire the streams together.

The interesting part is how we use type level calculations from shapeless to calculate the tuple and HList types for piped processes. This is all done using the technique I described earlier but may look a bit shocking first. Let’s take a look!

The way to parse this is to follow the type level computations performed through the Aux types in the implicit parameter list:

• PN1 and PN2 are the types of the two processes piped together
• The first two implicit definitions calculates the running process tuple and the running process HList types of these individual process nodes and “stores” the results in RP1, RPL1, RP2 and RPL2 type parameters. For example, if the two processes pipe together are single Process instances, then RP1 and RP2 would be some kind of RunningProcess, and the HLists would be one element long, like RunningProcess :: HNil.
• The last1 implicit parameter is a type level last function on the first process’s HList. This is required because PN1 itself can also be a sequence of piped processes, and we are connecting PN2 to the last of these. The RP1Last type parameter becomes the type of the last running process of the first process node.
• The next line rp1LastType is an additional constraint fixing the output stream element type of RP1Last to Byte. The piping implementation is not able to connect streams of arbitrary element types, as the process input is always required to be a byte stream.
• hcons2 is similar to the last1 but here we are calculating the type level head type of the HList called RPL2. The head will be in RP2Head and the tail HList in RP2Tail.
• In the prepend step we concatenate RPL1 with RPL2 using the Prepend operation, the result HList type is in RPL. This is the HList representation of the piped running process.
• Finally, we use the Tupler operation to calculate the tuple type from the HList, and store it in RPT.

The compiler performs the type level calculations and we can use the result types RPT and RPL to actually implement the start typeclass. This is the most complicated type level calculation in the library.

Final thoughts

As we’ve seen, Scala’s type system can bring us quite far in expressing a dependent typed interface. On the other hand, writing and reading code in this style is really hard, and if things go wrong, decoding the compiler’s error messages is not an easy task either. This is a serious tradeoff that has to be considered and in many cases, a more dynamic but much more readable and maintainable approach can be better.

With prox I explicitly wanted to explore these features of the Scala language.

In the next posts, we will ignore the type level parts of the library and focus on different streaming and effect libraries.