Type-level DI Container prototype by Mark Seemann
A fairly pointless Haskell exercise.
This article is part of a series called Type-safe DI composition.
People sometimes ask me how to do Dependency Injection (DI) in Functional Programming, and the short answer is that you don't. DI makes everything impure, while the entire point of FP is to write as much referentially transparent code as possible. Instead, you should aim for the Functional Core, Imperative Shell style of architecture (AKA impureim sandwich).
Occasionally, someone might point out that you can use the contravariant Reader functor with a 'registry' of services to emulate a DI Container in FP.
Not really, because even if you make the dependencies implicitly available as the Reader 'environment', they're still impure. More on that in a future article, though.
Still, what's a DI Container but a dictionary of objects, keyed by type? After I read Thinking with Types I thought I'd do the exercise and write a type-level container of values in Haskell.
Module #
The TLContainer module requires a smorgasbord of extensions and a few imports:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module TLContainer (Container (), nil, insert, get) where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
import Fcf
import Unsafe.Coerce (unsafeCoerce)
Notice that the module only exports the Container type, but not its data constructor. You'll have to use nil and insert to create values of the type.
Data types #
The Container should be able to store an arbitrary number of services of arbitrary types. This doesn't sound like a good fit for a statically typed language like Haskell, but it's possible to do this with existential types. Define an existential type that models a container registration:
data Reg where Reg :: a -> Reg
The problem with existential types is that the type argument a is lost at compile time. If you have a Reg value, it contains a value (e.g. a service) of a particular type, but you don't know what it is.
You can solve this by keeping track of the types at the type level of the container itself. The Container data type is basically just a wrapper around a list of Reg values:
data Container (ts :: [k]) where UnsafeContainer :: [Reg] -> Container ts
The name of the data constructor is UnsafeContainer because it's unsafe. It would enable you to add multiple registrations of the same type. The container shouldn't allow that, so the module doesn't export UnsafeContainer. Instead, it defines sufficient type-level constraints to guarantee that if you try to add two registrations of the same type, your code isn't going to compile.
This is the principal feature that distinguishes Container from the set of tuples that Haskell already defines.
Registration #
The module exports an empty Container:
nil :: Container '[] nil = UnsafeContainer []
Not only is this container empty, it's also statically typed that way. The type Container '[] is isomorphic to ().
The nil container gives you a container so that you can get started. You can add a registration to nil, and that's going to return a new container. You can add another registration to that container, and so on.
The distinguishing feature of Container, however, is that you can only add one registration of a given type. If you want to register multiple services of the same type, register a list of them.
Code like insert readReservations $ insert readReservations nil shouldn't compile, because it tries to insert the same service (readReservations) twice. To enable that feature, the module must be able to detect type uniqueness at the type level. This is possible with the help from the first-class-families package:
type UniqueType (t :: k) (ts :: [k]) = Null =<< Filter (TyEq t) ts
This type models the condition that the type t must not be in the list of types ts. It almost looks like regular Haskell code at the term level, but it works at the type level. Null is a type that can be evaluated to Boolean types at compile-time, depending on whether a list is empty or not.
This enables you to define a closed type family that will produce a compile-time error if a candidate type isn't unique:
type family RequireUniqueType (result :: Bool) (t :: k) :: Constraint where RequireUniqueType 'True t = () RequireUniqueType 'False t = TypeError ( 'Text "Attempting to add the type " ':<>: 'ShowType t ':<>: 'Text " to the container, but this container already contains that type.")
Combined with the UniqueType alias, you can now define the insert function:
insert :: RequireUniqueType (Eval (UniqueType t ts)) t => t -> Container ts -> Container (t ': ts) insert x (UnsafeContainer xs) = UnsafeContainer (Reg x : xs)
This function enables you to register multiple services, like this:
container :: Container '[LocalTime -> IO [Reservation], Reservation -> IO ()] container = insert readReservations $ insert createReservation nil
If, on the other hand, you attempt to register the same service multiple times, your code doesn't compile. You might, for example, attempt to do something like this:
container' = insert readReservations container
When you try to compile your code, however, it doesn't:
* Attempting to add the type LocalTime
-> IO
[Reservation] to the container,
but this container already contains that type.
* In the expression: insert readReservations container
In an equation for container':
container' = insert readReservations container
|
36 | container' = insert readReservations container
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
As a proof of concept, that's good enough for me. A type-safe set of uniquely typed registrations.
Retrieval #
Given that Container is a wrapper over a list of existential types, it seems as though the type information is lost. It isn't, though. Consider the type of the above container value. At the type level, you can see that it contains two services: one with the type LocalTime -> IO [Reservation], and another with the type Reservation -> IO (). Not only that, but the compiler can see the position of each of those types. Due to the way insert is implemented, that order corresponds to the order of Reg values.
First, define a type alias to find the index of a type t in a list of types ts:
type FindElem (t :: k) (ts :: [k]) =
FromMaybe Stuck =<< FindIndex (TyEq t) ts
This is again the first-class-families package in action. FindIndex finds a Nat that represents the index if the type is there. If it isn't there, the type is equivalent to Stuck, which is the type-level equivalent of undefined. Nat is a KnownNat instance, whereas Stuck isn't, which now enables you to define a constraint:
type IsMember t ts = KnownNat (Eval (FindElem t ts))
The IsMember constraint limits t to belong to ts. With it, you can now define a helper function to find the index of a type t in a list of types ts:
findElem :: forall t ts. IsMember t ts => Int findElem = fromIntegral . natVal $ Proxy @(Eval (FindElem t ts))
Because of the IsMember constraint, we know that t must be a member of ts. You can't call findElem if that's not the case; your code wouldn't compile.
You can now define a function to retrieve a service from a Container:
get :: forall t ts. IsMember t ts => Container ts -> t get (UnsafeContainer xs) = unReg $ xs !! findElem @t @ts where unReg (Reg x) = unsafeCoerce x
The get function first finds the index of the type t in ts. It then uses the (unsafe) list index operator !! to get the correct Reg value out of x. While the use of !! is generally considered unsafe (or, at least, partial) in Haskell, we know that the element is there because of the IsMember constraint.
Furthermore, because of the way insert builds up the container, we know that the service inside the existential type Reg must be of the type t. Thus, it's safe to use unsafeCoerce.
Example #
Imagine that you've created the above container. You can now retrieve services from it as necessary.
For example, to implement a HTTP GET resource that returns a list of reservations for a given date, you could do something like this:
getReservations :: LocalTime -> IO (HTTPResult [Reservation]) getReservations date = do let svc = get container :: LocalTime -> IO [Reservation] reservations <- svc date return $ OK reservations
Nothing much happens here. You could imagine that proper input validation of date is done before the service is invoked, or that some mapping operation is done on reservations before the function returns them. I omitted those steps, since they're not what matters. What matters is that that you can use get to safely get a service of the type LocalTime -> IO [Reservation].
Likewise, you could implement an HTTP POST resource that clients can use use to create new reservations:
postReservation :: Reservation -> IO (HTTPResult ()) postReservation dto = do let svc = get container :: Reservation -> IO () svc dto return $ OK ()
Since the compiler knows that container also contains a service of the type Reservation -> IO (), this still compiles.
If, on the other hand, you attempted to implement a single HTTP GET resource, the following wouldn't compile:
getSingleReservation :: LocalTime -> String -> IO (HTTPResult Reservation) getSingleReservation date email = do let svc = get container :: LocalTime -> String -> IO (Maybe Reservation) mres <- svc date email case mres of Just r -> return $ OK r Nothing -> return $ NotFound
The get container line doesn't compile because container doesn't contain a service of the type LocalTime -> String -> IO (Maybe Reservation), and the compiler can tell.
If you truly want to add that feature, you'll have to first register that service with the container:
container :: Container '[ LocalTime -> String -> IO (Maybe Reservation), LocalTime -> IO [Reservation], Reservation -> IO ()] container = insert readReservation $ insert readReservations $ insert createReservation nil
Notice that the type of container has now changed. It now contains three services instead of two. The getSingleReservation action now compiles.
Uniqueness #
The Container shown here is essentially just a glorified tuple. The only distinguishing trait is that you can define a tuple where two or more elements have the same type, such as (String, Bool, String), whereas this isn't possible with Container. You can define a Container '[String, Bool], but not Container '[String, Bool, String].
Why is this desirable?
This stems from a short and (friendly, I hope) Twitter discussion initiated by Bogdan Galiceanu. We were discussing whether it'd be more appropriate to use SingleOrDefault to manipulate a service in a DI Container, or foreach.
"Yeah, I wasn't explicit and clarified in a second tweet. I didn't mean in the services example, but in general where it helps if the reader's mental model of the code has 1 item from the collection, because that's how it is in real life. SingleOrDefault would enforce this."
The point being made here is that while you have a dictionary of collections, you expect certain (if not all) of these collections to be singleton sets.
I'm so happy that people like Bogdan Galiceanu share their thoughts with me, because it gives me a wider perspective on how programmers interact with APIs. If you take the API of the .NET Core DI Container as given, you almost have to think of its entries in this way.
I think, on the other hand, that this indicates a missed opportunity of API design. I replied:
"Yes, this could be a requirement. I think, though, that if that's the case, you've unearthed another invariant. That's what object-oriented design is about.
"Different invariants imply a change of type. If there can only be one of each element, then a set is more appropriate."
Twitter isn't a medium that makes it easy to elaborate on ideas, but what I meant was that if a container should contain only a single instance of, say, IFoo, it'd be clearer if the type system reflected that. Thus, when resolving IFoo, the return type should be IFoo, and not IEnumerable<IFoo>.
On the other hand, if you meant to register a collection of IBar services, when resolving IBar, the return type should be IEnumerable<IBar> (or, even better, IReadOnlyCollection<IBar>).
The Container shown here has this desired property: You can't insert the same type more than once. If you want to insert multiple IBar values, you must insert a [IBar] (list of IBar). Thus, you can't get a single IBar, but you can get a list: [IBar].
That was my motivation for the rule that each type can only appear once. In Haskell it's possible to implement such a rule at the type level. I don't think it'd be possible in a language like C# or F#, but you could implement it as a run-time check.
Conclusion #
You can implement a type-level container of values in Haskell. The contents are completely parametrically polymorphic, so while you can insert pure values like String, Bool, or Reservation into it, you can also add functions and impure actions like Reservation -> IO ().
Why is this interesting? It really isn't, apart from that I found it an interesting exercise in type-level programming.
The idea of a type-safe DI Container is, however, marginally more compelling, so I'll return to that topic in a future article.
