type safe multi-OS Propellor
Propellor was recently ported to FreeBSD, by Evan Cofsky. This new feature led me down a two week long rabbit hole to make it type safe. In particular, Propellor needed to be taught that some properties work on Debian, others on FreeBSD, and others on both.
The user shouldn't need to worry about making a mistake like this; the type checker should tell them they're asking for something that can't fly.
-- Is this a Debian or a FreeBSD host? I can't remember, let's use both package managers! host "example.com" $ props & aptUpgraded & pkgUpgraded
As of propellor 3.0.0 (in git now; to be released soon), the type checker will catch such mistakes.
Also, it's really easy to combine two OS-specific properties into a property that supports both OS's:
upgraded = aptUpgraded `pickOS` pkgUpgraded
type level lists and functions
The magick making this work is type-level lists. A property has a metatypes list as part of its type. (So called because it's additional types describing the type, and I couldn't find a better name.) This list can contain one or more OS's targeted by the property:
aptUpgraded :: Property (MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]) pkgUpgraded :: Property (MetaTypes '[ 'Targeting 'OSFreeBSD ])
In Haskell type-level lists and other DataKinds are indicated by the
' if you have not seen that before. There are some convenience
aliases and type operators, which let the same types be expressed
aptUpgraded :: Property (Debian + Buntish) pkgUpgraded :: Property FreeBSD
Whenever two properties are combined, their metatypes are combined
using a type-level function. Combining
will yield a metatypes that targets no OS's, since they have none in
common. So will fail to type check.
My implementation of the metatypes lists is hundreds of lines of code, consisting entirely of types and type families. It includes a basic implementation of singletons, and is portable back to ghc 7.6 to support Debian stable. While it takes some contortions to support such an old version of ghc, it's pretty awesome that the ghc in Debian stable supports this stuff.
extending beyond targeted OS's
Before this change, Propellor's Property type had already been slightly
refined, tagging them with
NoInfo, as described
in making propellor safer with GADTs and type families. I needed to
HasInfo in the type of properties.
But, it seemed unnecessary verbose to have types like
Property NoInfo Debian.
Especially if I want to add even more information to Property
Property NoInfo Debian NoPortsOpen would be a real mouthful to
need to write for every property.
Luckily I now have this handy type-level list. So, I can shove more
types into it, so
Property (HasInfo + Debian) is used where necessary,
Property Debian can be used everywhere else.
Since I can add more types to the type-level list, without affecting other properties, I expect to be able to implement type-level port conflict detection next. Should be fairly easy to do without changing the API except for properties that use ports.
As shown here,
pickOS makes a property that
decides which of two properties to use based on the host's OS.
aptUpgraded :: Property DebianLike aptUpgraded = property "apt upgraded" (apt "upgrade" `requires` apt "update") pkgUpgraded :: Property FreeBSD pkgUpgraded = property "pkg upgraded" (pkg "upgrade") upgraded :: Property UnixLike upgraded = (aptUpgraded `pickOS` pkgUpgraded) `describe` "OS upgraded"
Any number of OS's can be chained this way, to build a property that is super-portable out of simple little non-portable properties. This is a sweet combinator!
Singletons are types that are inhabited by a single value.
This lets the value be inferred from the type, which came in handy
in building the
pickOS property combinator.
Its implementation needs to be able to look at each of the properties at
runtime, to compare the OS's they target with the actial OS of the host.
That's done by stashing a target list value inside a property. The target
list value is inferred from the type of the property, thanks to singletons,
and so does not need to be passed in to
property. That saves
keyboard time and avoids mistakes.
is it worth it?
It's important to consider whether more complicated types are a net benefit. Of course, opinions vary widely on that question in general! But let's consider it in light of my main goals for Propellor:
- Help save the user from pushing a broken configuration to their machines at a time when they're down in the trenches dealing with some urgent problem at 3 am.
- Advance the state of the art in configuration management by taking advantage of the state of the art in strongly typed haskell.
This change definitely meets both criteria. But there is a tradeoff; it got a little bit harder to write new propellor properties. Not only do new properties need to have their type set to target appropriate systems, but the more polymorphic code is, the more likely the type checker can't figure out all the types without some help.
A simple example of this problem is as follows.
foo :: Property UnixLike foo = p `requires` bar where p = property "foo" $ do ...
The type checker will complain that "The type variable ‘metatypes1’ is
ambiguous". Problem is that it can't infer the type of
p because many
different types could be combined with the
bar property and all would
Property UnixLike. The solution is simply to add a type signature
p :: Property UnixLike
Since this only affects creating new properties, and not combining existing properties (which have known types), it seems like a reasonable tradeoff.
things to improve later
There are a few warts that I'm willing to live with for now...
Property (HasInfo + Debian) is different than
Property (Debian +
HasInfo), but they should really be considered to be the same type. That is, I
need type-level sets, not lists. While there's a type level sets library for
hackage, it still seems to
require a specific order of the set items when writing down a type signature.
ensureProperty, which runs one property inside the action
of another property, got complicated by the need to pass it a type witness.
foo = Property Debian foo = property' $ \witness -> do ensureProperty witness (aptInstall "foo")
That witness is used to type check that the inner property targets every OS that the outer property targets. I think it might be possible to store the witness in the monad, and have ensureProperty read it, but it might complicate the type of the monad too much, since it would have to be parameterized on the type of the witness.
Oh no, I mentioned monads. While type level lists and type functions and generally bending the type checker to my will is all well and good, I know most readers stop reading at "monad". So, I'll stop writing. ;)
Thanks to David Miani who answered my first tentative question with a big hunk of example code that got me on the right track.
Also to many other people who answered increasingly esoteric Haskell type system questions.
Also thanks to the Shuttleworth foundation, which funded this work by way of a Flash Grant.