Data Families Make Types and Free Monads More Librarious

At the end of my post Type Families Make Life and Free Monads Simpler I conjectured whether it would be possible to write a “CRUD” library around the Free CrudF monad. The exact meaning of a library in this context is somewhat nuanced. What libraries look like when you’re doing type-level programming wasn’t clear to me initially. After learning and working with dependent types in Haskell I’ve settled on a better understanding that sometimes feels like “Java Spring for Types.”

In this post I will outline how we can use Open Type and Data Families to write libraries that users configure at the type-level. We will do this by creating a generalized Free CrudF monad, continued from my previous post, whose types are configured by the user. Along the way we’ll learn about Type and Data Families and how to assist GHC with type checking.

1. Recap
2. User-Defined Type and Data Families
3. Crud Library
4. User-Provided Types and Kinds
5. Y U No Compile, Dr. Interpreter?
6. Using Typeclass Constraints to Support the Type Checker
7. God’s in its own heaven; all’s right with the world

All code samples for this post can be found here.

1. Recap

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-01-recap-hs

If you recall from our last adventure, the primary type-level machinery for the Free CrudF monad consisted of a data type to index the types we perform CRUD on, in addition to some type families:

-- | User code. Our types.
data Product = Product
data ProductData = ProductData Int
data Order = Order
data OrderData = OrderData

-- | a universe of data types that we perform crud on
data Crudable = ProductCRUD
              | ProductsR
              | OrderCRUD

-- | singleton support to traverse the type and kind level
data SCrudable (c :: Crudable) where
    SProductCRUD :: SCrudable 'ProductCRUD
    SProductsR   :: SCrudable 'ProductsR
    SOrderCRUD   :: SCrudable 'OrderCRUD

-- | a type family mapping elements from our Crudable universe
-- to the data required to Read them. This can be read as: "to
-- read a Product, we need an Int. To read Products we need a
-- String. To read an Order we need an Int
type family ReadData (c :: Crudable) :: * where
    ReadData 'ProductCRUD = Int
    ReadData 'ProductsR   = String
    ReadData 'OrderCRUD   = Int

-- | a type family mapping elements from our Crudable universe
-- to the base types we return when performing certain crud
-- operations
type family CrudBase (c :: Crudable) :: * where
    CrudBase 'ProductCRUD = Product
    CrudBase 'ProductsR   = [Product]
    CrudBase 'OrderCRUD   = Order

-- | the CrudF functor. Remember how it uses the SCrudable singleton to
-- manifest a c of kind Crudable and then the type families to map that kind
-- to the required types.
data CrudF next :: * where
    Read :: SCrudable c -> ReadData c -> (Maybe (CrudBase c) -> next) -> CrudF next

We’ve omitted quite a bit of detail for the sake of a recap. We haven’t included any interpreters, smart constructors, or even the full set of CRUD verbs (only Read is present). For the full code, see here.

The main question posed in this post is how do we turn the above into a library? We’re used to writing libraries at the value level, but the type-level is a little different. There are a few places we need to introduce abstraction for the library’s clients:

1. We need our universe of types (Crudable) to be user-defined.
2. We need our SCrudable singleton-support to be user-defined.
3. We need our type families to be user-defined.
4. Because we’re doing a bit of refactoring, we’ll ensure our CrudF GADT has a single constructor (instead of four).

When I first started thinking about this I had absolutely no idea how I would accomplish 1 and 2. Thankfully, @a_cowley had sent me some unrelated code a few months ago and I remembered seeing the keyboard data family. I figured this would be the best place to start (thanks Anthony!)

2. User-defined Type and Data Families

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-02-user-defined-type-and-data-families-hs

We begin with a little refactoring of our previous code. First, we define a universe of CRUD verbs used to index some of our type families.

-- | A universe of CRUD verbs used to collapse `CrudF` into a single constructor
data CRUD = Create | Read | Update | Delete

-- | singleton support for the CRUD universe
data CrudVerb (c :: CRUD) :: * where
    SCreate :: CrudVerb 'Create
    SRead   :: CrudVerb 'Read
    SUpdate :: CrudVerb 'Update
    SDelete :: CrudVerb 'Delete

In our original CrudF code, our type families were closed. By this we mean they were not extendable by user code. We defined them over a universe (or index) of types of kind Crudable. In order for us to expose this code as a library, we need to use Open Type Families. Open Type Families will allow a user to provide their own type-level functions satisfying the properties of the type family. This is not dissimilar to typeclasses, except at the type level.

We will define two open type families: one for input data and another for output data. This representation will capture the types of data required as input for an operation and the type of data required as output for an operation. By this we mean: “when you’re performing a Create operation, input refers to the data required to perform that operation and output refers to the data returned by that operation. The types of input and output will depend on a type of kind CRUD and a user-defined type of kind k.

-- | an open type family mapping types of kind CRUD and types of a user-defined kind k
-- to the type of input data required.
type family InputData (c :: CRUD) (a :: k) :: *

-- | an open type family mapping types of kind CRUD and type sof a user-defined kind k
-- to the type returned by the operation
type family ReturnData (c :: CRUD) (a :: k) :: *

You can think of InputData and ReturnData as functions at the type level with a signature like: InputData :: CRUD -> k -> *.

Now that we’ve created type families that can be defined by users of our library, we need a way to abstract the original universe of kind Crudable. This is where Data Families come in. Recall that our Crudable kind and its singleton support SCrudable served two purposes: one, it afforded us an index for types that we want to permit CRUD actions on, and two, SCrudable created a bridge between the type and the kind level.

How do we allow users to define kind universes and type-kind bridges? Data Families!

As a convention, the kind k will be reserved for the universe of types that the user will provide as an index. In the previous post, this would have corresponded to Crudable. Our user-implemented data family will encapsulate mapping from types of kind k to types of kind *. We name this data family CrudSing as it represents the user-supplied singleton support for our CRUD library.

-- | data family to map types of kind k to types of kind *
data family CrudSing :: k -> *

3. Crud Library

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-03-crud-library-hs

With the CRUD universe of types, the InputData and ReturnData type families, and the CrudSing data family, we are now ready to define our CrudF functor! We present the program in entirety thus far:

-- | A universe of CRUD verbs used to collapse `CrudF` into a single constructor
data CRUD = Create | Read | Update | Delete

-- | singleton support for the CRUD universe
data CrudVerb (c :: CRUD) :: * where
    SCreate :: CrudVerb 'Create
    SRead   :: CrudVerb 'Read
    SUpdate :: CrudVerb 'Update
    SDelete :: CrudVerb 'Delete

-- | an open type family mapping types of kind CRUD and types of a user-defined kind k
-- to the type of input data required.
type family InputData (c :: CRUD) (a :: k) :: *

-- | an open type family mapping types of kind CRUD and type sof a user-defined kind k
-- to the type returned by the operation
type family ReturnData (c :: CRUD) (a :: k) :: *

-- | data family to map types of kind k to types of kind *
data family CrudSing :: k -> *

-- | abstract CrudF functor!
data CrudF :: [k] -> * -> * where
    CrudF :: CrudVerb v
          -> CrudSing c
          -> InputData v c
          -> (ReturnData v c -> a)
          -> CrudF fs a

This datatype might seem a little puzzling, so let’s start by describing it at the type level. If you read the CrudF kind, it states: "given a type-level list of kind k and a type of kind *, return a type of kind *.” The first question that comes to mind concerns the presence of the type-level list of kind k ([k]). There is a subtle reason for this. Recall that we quantify over types of kind CRUD and the user-provided k. As CRUD is closed, we don’t have to parameterize our CrudF type with it, but since k is user-provided, we need to encode the types of kind k the user is defining somewhere. We also know there will be many types of kind k used in our data type, and we need this encoded somewhere as well. Therefore, we encode the types of kind k featured in CrudF by parameterizing our functor with [k]. If this nuance is tripping you up now, it should become more apparent as we continue.

At the value-level, the CrudF type reads mostly straightforward. Given a CrudVerb v and CrudSing c, i.e. given a crud verb and a user-provided singleton, v and c will specify a type of kind CRUD and k respectively. These types are then passed to the InputData and ReturnData type families to specify the input and return data used to construct CrudF.

To use CrudF as a free monad, we need to provide a functor instance:

instance Functor (CrudF fs) where
    fmap f (CrudF v s i g) = CrudF v s i (f . g)

Now we can write some smart constructors. Here’s an example for the create verb:

create :: CrudSing f
       -> InputData 'Create f
       -> Free (CrudF fs) (ReturnData 'Create f)
create s d = Free $ CrudF SCreate s d Pure

This basically completes our library. We will next show what user code looks like and this will lead us to a snake in the grass!

4. User-Provided Types and Kinds

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-04-user-provided-types-and-kinds-hs

As a client of our CrudF library, we need to:

1. Define our universe of types (in the previous post this was Crudable and in our library this is the kind k).
2. Provide an instance of the CrudSing data family.
3. Provide instances for the InputData and ReturnData type family.

Lets start by defining some basic types that we will work with (as in the previous post, Product and Order). Then we’ll define our universe and provide instances for the data families and type families.

-- | User code. Our types.
data Product = Product
data ProductData = ProductData Int
data Order = Order
data OrderData = OrderData

-- | A universe to index types we do crud over. This was `Crudable` in the
-- previous post and is `k` in our library.
data MyCrud = ProductCRUD | OrderCRUD

-- | instance of the `CrudSing` data family.
data instance CrudSing (a :: MyCrud) where
    SProduct :: CrudSing 'ProductCRUD
    SOrder   :: CrudSing 'OrderCRUD

-- | type family instances. This maps the Input and Output
-- data required and returned for each CRUD operation.
type instance InputData  'Create ProductCRUD = ProductData
type instance InputData  'Read   ProductCRUD = Int
type instance InputData  'Update ProductCRUD = Product
type instance InputData  'Delete ProductCRUD = Int
type instance ReturnData 'Create ProductCRUD = Product
type instance ReturnData 'Read   ProductCRUD = Product
type instance ReturnData 'Update ProductCRUD = Product
type instance ReturnData 'Delete ProductCRUD = Product

type instance InputData  'Create OrderCRUD = OrderData
type instance InputData  'Read   OrderCRUD = Int
type instance InputData  'Update OrderCRUD = Order
type instance InputData  'Delete OrderCRUD = Int
type instance ReturnData 'Create OrderCRUD = Order
type instance ReturnData 'Read   OrderCRUD = Order
type instance ReturnData 'Update OrderCRUD = Order
type instance ReturnData 'Delete OrderCRUD = Order

As a client, usage of the library is fairly straight forward. We provide some data family and type family instances that feels very much like basic configuration (Java Spring for Types!).

So far so good. Now let’s write some smart constructors:

-- | Smart constructor for creating products. Non-eta-reduced for clarity.
createProduct :: InputData 'Create 'ProductCRUD -> Free(CrudF '[ProductCRUD, OrderCRUD]) Product
createProduct d = create SCreat SProduct d

You can see here where the type-level list of kind k comes in ('[ProductCRUD, OrderCRUD]). We also use the fact that InputData is a type family and don’t bother specifying ProductData as the type input to createProduct (even though InputData 'Create 'ProductCRUD = ProductData). This means that if we change the input we don’t have to update our constructors, reinforcing the idea that we configure our program at the type level (Java Spring for Types!).

5. Y U No Compile, Dr. Interpreter?

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-05-y-u-no-compile-hs

Now, what does an interpreter look like? For brevity, we present a simple, non-exhaustive interpreter below:

-- | sample, non-exhaustive interpreter. that won't compile :(
-- gratuitous pattern matching to show the correct type is inferred
interpreter :: Free (CrudF '[ProductCRUD, OrderCRUD]) a -> IO a
interpreter (Pure a) = return a
interpreter (Free (CrudF SCreate SProduct (ProductData _) g)) = interpreter $ g Product
interpreter (Free (CrudF SCreate SOrder _ g))                 = interpreter $ g Order

If you try to compile this you will get a brutal and somewhat misleading message:

05-y-u-no-compile.hs:93:34:
    Could not deduce (k ~ MyCrud)
    from the context (v ~ 'Create)
      bound by a pattern with constructor
                 SCreate :: CrudVerb 'Create,
               in an equation for ‘interpreter’
      at crud2.hs:121:26-32
      ‘k’ is a rigid type variable bound by
          a pattern with constructor
            CrudF :: forall (k :: BOX)
                            (fs :: [k])
                            a
                            (k :: BOX)
                            (v :: CRUD)
                            (f :: k).
                     CrudVerb v
                     -> CrudSing f
                     -> InputData v f
                     -> (ReturnData v f -> a)
                     -> CrudF fs a,
          in an equation for ‘interpreter’
          at crud2.hs:121:20
    Expected type: CrudSing f
      Actual type: CrudSing a0
    In the pattern: SProduct
    In the pattern: CrudF SCreate SProduct (ProductData _) g
    In the pattern: Free (CrudF SCreate SProduct (ProductData _) g)

    (... repeat ...)

To my naive eyes, this message is intractable. The main point is that GHC is having a hard time with type inference. When I initially saw this I was dumbfounded. How could GHC not infer these types? After all, we’re pattern matching on SCreate so obviously GHC should know, right away, that v is 'Create. However, if we consider the type of our GADT, we know that the user-provided types we need have been quantified over and are not known to GHC after construction of the data type (i.e. when pattern matching). Recall, that the fully quantified type for the CrudF constructor is:

-- | CrudF constructor with explicit quantification
CrudF :: forall (v :: CRUD) (f :: k) (fs :: [k]) (a :: *)
      .  CrudVerb v
      -> CrudSing f
      -> InputData v f
      -> (ReturnData v f -> a)
      -> CrudF fs a

As we quantify over (f :: k), we erase any knowledge of f. Most importantly, we do not know if it is even contained in fs :: [k]! For example, it’s possible that f = 'OrderCRUD and fs = ['ProductCRUD].

Is all hope lost?

6. Using Typeclass Constraints to Support the Type Checker

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-06-using-typeclass-constraints-to-support-the-type-checker-hs

How can we fix this? I was stumped on this for quite some time. Thankfully, I had seen the solution in some code @a_cowley sent to me a few months earlier.

The solution is to create a constraint forcing f :: k to be contained in the type-level list fs :: [k]. This is done by defining a special data type and a typeclass.

-- | type checking support. This is similar, but not the same, as an HList.
data Elem (x :: k) (xs :: [k]) where
    Here :: Elem x (x ': xs)
    There :: Elem x xs -> Elem x (y ': xs)

-- | typeclass to assist with type checking.
class Implicit a where
    implicitly :: a

-- | if the first `x` of kind `k` in `Elem` matches the head of the list
-- then `Elem x (x ': xs))` is an instance of `Implicit`
instance Implicit (Elem x (x ': xs)) where
    implicitly = Here

-- | If `x` is not at the head of the list, then we constrain
-- instances to those for which `Elem x xs` is an instance. This guarantees
-- us to roll through `Elem`.
instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where
    implicitly = There implicitly

In our case, where [k] ~ ['ProductCRUD, 'OrderCRUD], if we constrain the CrudF constructor to Implicit (Elem f fs) then we will have the following class environment available (there will be many more permutations, but for the sake of our discussion, this is enough):

implicitly :: Elem 'ProductCRUD ('ProductCRUD : 'OrderCRUD : [])
implicity = Here

implicitly :: Elem 'OrderCRUD ('ProductCRUD : 'OrderCRUD : [])
implicitly = There (Here :: Elem 'OrderCRUD ('OrderCRUD : [])) :: Elem 'OrderCRUD ('ProductCRUD : 'OrderCRUD : [])

implicitly :: Elem 'Create '[]
implicitly = Here

Now, we just amend our data type and smart constructor:

-- | new CrudF constructor with type checking hints
data CrudF :: [k] -> * -> * where
    CrudF :: Implicit(Elem f fs)
          => CrudVerb v
          -> CrudSing f
          -> InputData v f
          -> (ReturnData v f -> a)
          -> CrudF fs a

-- | smart constructor also needs type checking hints.
create :: Implicit(Elem f fs)
       => CrudSing f
       -> InputData 'Create f
       -> Free (CrudF fs) (ReturnData 'Create f)
create s d = Free $ CrudF  s d Pure

With this type-checking support, GHC can now infer that when you pattern match on CrudF ['ProductCRUD, 'OrderCRUD] that the f is constrained to be an element of the list by virtue of the Implicit(Elem f fs) constraint and it can then infer the right type of f! And now our program compiles!

7. God’s in its own heaven; all’s right with the type checker

code: https://gist.github.com/aaronlevin/ce387cd891503540a5fd#file-07-gods-in-its-own-heaven-hs

And that’s it! The full code, with client code is below and everything type checks!

It’s worth revisiting what we have accomplished. First we took some dependently typed haskell code and turned it into a library. Because we were dealing with user-defined abstractions at the type and kind level, this required the use of open Type Families and Data Families. Everything was going well until we hit a snag with the type checker, but we were able to use typeclass constraints to give hints to the compiler.

It’s questionable how useful our Free CrudF monad is. However, the main takeaway is the nature of how type-level libraries are used. In a dialectical gesture that would impress even Hegel, our programs become a vehicle for the configuration of types; the core logic safely abstracted from us. This is a very empowering style of programming.

Now, go forth and create libraries at the type level!

-- | kitchen sink of extensions

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}

module FreeCrud where

import Control.Monad.Free(Free(Free, Pure))

-- the library portion is below

-- | type checking support, thanks to @a_cowley
data Elem (x :: k) (xs :: [k]) where
    Here :: forall x xs. Elem x (x ': xs)
    There :: forall x xs y. Elem x xs -> Elem x (y ': xs)

class Implicit a where
    implicitly :: a

instance Implicit (Elem x (x ': xs)) where
    implicitly = Here

instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where
    implicitly = There implicitly

-- | Index of types that can be crudded / singleton support
data family CrudSing :: k -> *

-- | crud verbs used to collapse `CrudF` to a single constructor
data CRUD = Create | Read | Update | Delete
data CrudVerb (a :: CRUD) :: * where
    SCreate :: CrudVerb 'Create
    SRead   :: CrudVerb 'Read
    SUpdate :: CrudVerb 'Update
    SDelete :: CrudVerb 'Delete

-- | open type families to index data types
type family InputData  (v :: CRUD) (a :: k) :: *
type family ReturnData (v :: CRUD) (a :: k) :: *

-- | The new CrudF functor
data CrudF :: [k] -> * -> * where
    CrudF :: Implicit(Elem f fs)
          => CrudVerb v
          -> CrudSing f
          -> InputData v f
          -> (ReturnData v f -> a)
          -> CrudF fs a

-- | functor instance
instance Functor (CrudF fs) where
   fmap f (CrudF v s i g) = CrudF v s i (f . g)

-- | sample smart constructor
create :: Implicit(Elem f fs)
       => CrudSing f
       -> InputData 'Create f
       -> Free (CrudF fs) (ReturnData 'Create f)
create s d = Free $ CrudF SCreate s d Pure

-- | User code

data Product = Product
data ProductData = ProductData Int
data Order = Order
data OrderData = OrderData

-- | index of crudable types
data MyCrud = ProductCRUD | OrderCRUD

-- | data family instance
data instance CrudSing (a :: MyCrud) where
    SProduct :: CrudSing ProductCRUD
    SOrder   :: CrudSing OrderCRUD

-- | type family defs
type instance InputData  'Create ProductCRUD = ProductData
type instance InputData  'Read   ProductCRUD = Int
type instance InputData  'Update ProductCRUD = Product
type instance InputData  'Delete ProductCRUD = Int
type instance ReturnData 'Create ProductCRUD = Product
type instance ReturnData 'Read   ProductCRUD = Product
type instance ReturnData 'Update ProductCRUD = Product
type instance ReturnData 'Delete ProductCRUD = Product

type instance InputData  'Create OrderCRUD = OrderData
type instance InputData  'Read   OrderCRUD = Order
type instance InputData  'Update OrderCRUD = Order
type instance InputData  'Delete OrderCRUD = Int
type instance ReturnData 'Create OrderCRUD = Order
type instance ReturnData 'Read   OrderCRUD = Int
type instance ReturnData 'Update OrderCRUD = Order
type instance ReturnData 'Delete OrderCRUD = Order

-- | sample smart(er) constructor
createProduct :: InputData 'Create 'ProductCRUD -> Free (CrudF '[ProductCRUD, OrderCRUD]) Product
createProduct = create SCreate SProduct

-- | sample, non-exhaustive interpreter
interpreter :: Free (CrudF '[ProductCRUD, OrderCRUD]) a -> IO a
interpreter (Pure a) = return a
interpreter (Free (CrudF SCreate SProduct (ProductData _) g)) = interpreter $ g Product
interpreter (Free (CrudF SCreate SOrder _ g)) = interpreter $ g Order