#dependent-types

After watching Ollie Charles' talk on Strongly Typed Publish/Subscribe over Websocks via Singleton Types, I felt very inspired to try some type-level programming in Haskell. Along the way I stumbled across a really handy design pattern I thought I would share.

Recently I've been working with another person on creating a client for the Shopify API in Haskell. Being there are a few different http clients in haskell (http-client, http-conduit, and pipes-http), I wanted the library to keep the http-client implementation independent. After discussing a few different approaches, I settled on the Free Monad approach for its flexibility.

During this post I will detail how I used type families and singletons to make a complicated algebra very simple, flexible, and safe. Furthermore, this approach, albeit somewhat naive and repeated in a few other contexts (e.g. indexed free monads), can be applied to many situations to help make your code safer and flexible.

As a spoiler, the end goal will be to create a program like (note the varying data types for the create and read constructors):

createOrder :: Free CrudF Order createOrder = do product1 <- create SProduct (ProductData ...) product2 <- read SProduct 13 products <- read SProducts "select * from product" create SOrder (OrderData (product1:product2:products))

Contents:

A Naive Functor and its Free Monad

Failing to Minimizing The Number of Constructors

Using Type Families Index Our Types

Using GADTs to Generalize our Functor

Further: Not All Things Read Can Be Created

A General Algebra for describing CRUD for shopify types

Summary and Next Steps

1. A Naive Functor and its Free Monad

code: https://gist.github.com/aaronlevin/4fc1fcfdce947a41567b#file-01-naive-functor-hs

Shopify, being a powerful e-commerce platform, has a a lot of data types available thorugh its API. For each of these data types, we'll want our client to perform CRUD on them: create, read, update, and delete. We'll focus on two such data types throughout this post: Product and Order.

The first step to expressing the actions our client can express via Free Monads is to create a Functor to describe each action. We will create two main data types (Product and Order) as well as the data needed to construct them (ProductData and OrderData). You can think of Product and Order as being what lives in the database, whereasProductData and OrderData represent what we need to create a row in our database. Their internals are largely irrelevant, the only thing you should keep in mind is that the four of them are different from each other.

Our naive functor will look like this:

{-# LANGUAGE DeriveFunctor #-} module Main where import Control.Monad.Free (Free(Free,Pure)) -- | Product data type data Product = Product { productId :: Int , productName :: String } -- | data we need to construct a product data ProductData = ProductData String -- | main Order data type data Order = Order Int String [Product] -- | data we need to construct an Order data OrderData = OrderData String [Int] -- | Our initial Crud Functor data CrudF a = CreateProduct ProductData (Product -> a) | ReadProduct Int (Maybe Product -> a) | UpdateProduct Product a | DeleteProduct Int a -- | ^ Product CRUD | CreateOrder OrderData (Order -> a) | ReadOrder Int (Maybe Order -> a) | UpdateOrder Order a | DeleteOrder Int a -- | ^ Order CRUD deriving (Functor) -- | Our Free Monad (uses the free library) type ShopifyAlgebra a = Free CrudF a main :: IO () main = print "01-naive-functor"

With our CrudF functor and the free monad it generates (ShopifyAlgebra) we can create smart constructors to express some programs. Here is an example one that Creates a Product, reads a product, and then creates an order using the two products.

-- | An example mini-program that creates a product, reads a product, -- | updates its name, and uses those products to create an order. programCreateOrder :: ShopifyAlgebra Order programCreateOrder = do newProduct <- createProduct $ ProductData "OG Bent Wind LP" existingProduct <- readProduct 17 let productIds = catMaybes [ Just productId $ newProduct , productId <$> existingProduct ] createOrder $ OrderData "amazing new order!" productIds

2. Failing to Minimizing The Number of Constructors

code: https://gist.github.com/aaronlevin/4fc1fcfdce947a41567b#file-02-wont-compose-hs

This all looks great, and we can write interpreters against our free monad (ShopifyAlgebra). However, a quick look at the Shopify API and we'll notice we're going to need 4 x 20 = 80 new CrudF constructors, which means 80 new smart constructors , which also means every interpreter we write is going to have to pattern match over 96 CrudF constructors! This is unwieldy!

How do we get around this? Well, one naive attempt would be to generalize our CrudF functor. For example, we might try:

data CrudF2 a d i next = Create2 d (a -> next) | Read2 i (Maybe a -> next) | Update2 a next | Delete2 i next deriving (Functor)

But now our constructors won't compose! For example:

createProduct2 :: ProductData -> Free (CrudF2 Product ProductData Int) Product createProduct2 productData = Free $ Create2 productData Pure createOrder2 :: OrderData -> Free (CrudF2 Order OrderData Int) Order createOrder2 orderData = Free $ Create2 orderData Pure

Notice the types after Free, mainly: CrudF2 Product ProductData Int versus CrudF2 Order OrderData Int. The Functors do not match, so we cannot create general programs that create Products and create Orders! This is terrible!

3. Using Type Families to Index Our Constructors

code: https://gist.github.com/aaronlevin/4fc1fcfdce947a41567b#file-03-type-families-index-constructors-hs

Notice that our CrudF2 constructors had a general pattern. Mainly:

Create2 {type for creating data a} (a -> next) Read2 {type to find a} (Maybe a -> next) Update2 a next Delete2 {type to find a} next

If only we could say: given some type a, map that type to the type required to create it, the type required to find it. This is exactly what Type Families are handy for!

Without going into the theory too deeply, we essentially want a type level function that maps our type to another type when used in the context of our CRUD functor. I will start by showing how you achieve this for the Create constructor, and we will add more later.

To start, we'll need a host of extensions in addition to our original data types. These extensions, most importantly TypeFamilies and DataKinds, will allow us to do type-level programming and promote our types to kinds and our values to types! Therefore, for (almost) each type in our module there will be an associated kind, and for each value constructor an associated type.

{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Main where -- | we continue to use our original data types. However, with these -- | extensions, each type is promoted to a kind, and each value to -- | a type. -- | Product data type data Product = Product { productId :: Int , productName :: String } -- | data we need to construct a product data ProductData = ProductData String -- | main Order data type data Order = Order Int String [Product] -- | data we need to construct an Order data OrderData = OrderData String [Int]

Now, the first thing we need is a way to index the types we can do CRUD with. The most naive way to capture this is to create a datatype (which, with DataKinds, will be promoted to the kind level):

data Crudable = ProductCRUD | OrderCRUD

Now Crudable represents types we do CRUD with. With DataKinds we now have the kind Crudable and the types 'ProductCRUD and 'OrderCRUD (it's customary to prefix promoted types with a single apostrophe ').

As per Ollie's talk and the general singletons approach to type-level programming in Haskell, we'll need a glue or pathway between the type/value-level programming and the kind/type-level programming. For this we create a singleton using GADTs:

data SCrudable (c :: Crudable) where SProductCRUD :: SCrudable 'ProductCRUD SOrderCRUD :: SCrudable 'OrderCRUD

Armed with our Crudable index and SCrudable singleton type, we can write some type families to define some type-level functions:

-- | type family that maps a Crudable type to the type required to create it type family CreateData (c :: Crudable) :: * where CreateData 'ProductCRUD = ProductData CreateData 'OrderCRUD = OrderData

What this type families tells us is that if we have a type of kind Crudable we can map this to the data required to create it. This encodes at the type-level the fact that we need ProductData to create Products and OrderData to create Orders. However, we'll also need a map between Crudable and our base types Product and Order, so we'll create another type family for this:

-- | type family that maps a Crudable type to its base type. This binds -- | our Crudable kind to the types we're actually interested in. type family CrudBase (c :: Crudable) :: * where CrudBase 'ProductCRUD = Product CrudBase 'OrderCRUD = Order

Now we are ready to re-write our CrudF functor. For now, we'll just re-write the Create constructor:

-- | new CrudF functor. "c" represents a type of kind Crudable. data CrudF3 (c :: Crudable) next = Create3 (CreateData c) (CrudBase c -> next)

Are we done? Unfortunately no. We're almost there, but we haven't made it all the way yet. In fact, at this point we haven't really gained very much. For example, if we tried to create a smart constructor to actually use this functor, you'll notice a problem:

-- | a new smart constructor. Use gratuitous pattern matching to show that· -- | the right types are inferred via the CreateData type family create3 :: SCrudable c -> CreateData c -> Free (CrudF3 c) (CrudBase c) create3 SProductCRUD productCreateData@(ProductData _) = Free $ Create3 productCreateData Pure create3 SOrderCRUD orderCreateData@(OrderData _ _) = Free $ Create3 orderCreateData Pure

Do you notice the issue? We've gained nothing! Our type is still Free (CrudF3 c) (CrudBase c), which, after the appropriate type family is applied, we have either Free (CrudF3 'ProductCRUD) (Product) or Free (CrudF3 'OrderCRUD) (Order). Because 'ProductCRUD and 'OrderCRUD are different types (albeit of the same kind Crudable), we will not be able to combine smart constructors in the following way:

-- | will not compile falseProgram = do newProduct <- create3 SProductCRUD (ProductData "heitkotter") newOrder <- create3 SOrderCRUD (OrderData "chargeback" [productId newProduct]

This won't compile because the Functor in newProduct and the Functor in newOrder are different.

Is all hope lost?

4. Using GADTs to Generalize our Functor

code: https://gist.github.com/aaronlevin/4fc1fcfdce947a41567b#file-04-gadts-to-the-rescue-hs

GADTs to the rescue! What we want to do is quantize over types of kind Crudable. We can do this with GADTS. If we keep all our types and type families, but update our CrudF functor:

data CrudF4 next :: * where Create4 :: SCrudable c -> CreateData c -> (CrudBase c -> next) -> CrudF4 next -- | our functor is sufficiently complex and GHC can no longer derive our -- | Functor for us. instance Functor CrudF4 where fmap f (Create4 c d g) = Create4 c d (f g)

Awesome! Now our CrudF4 functor is parameterized over a single type! Which means we can write smart constructors and create a working version of the above mini-program:

-- | smart constructor. we wont do pattern matching here. we only did it above -- | to highlight the usage of type families create4 :: SCrudable c -> CreateData c -> Free CrudF4 (CrudBase c) create4 c d = Free $ Create4 c d Pure -- | mini program that creates two products and an order workingProgram :: Free CrudF4 Order workingProgram = do newProduct1 <- create4 SProductCRUD (ProductData "Lewis - L'Amour") newProduct2 <- create4 SProductCRUD (ProductData "Lewis - Romantic Times") let productIds = productId <$> [newProduct1, newProduct2] create4 SOrderCRUD (OrderData "Lewis gripper" productIds)

This is amazing. We now have a Free Monad that can create Products and Orders with the same Functor! Additionally, our smart constructor can handle different data types depending on the context (SProductCRUD or SOrderCRUD).

A sensible question might be: could we achieve this without Type Families and Data Kinds, using a regular GADT? The answer is no. How could we write a smart constructor for such a type? More importantly, how would we write a valid interpreter for such an algebra? Our interpreter would have to handle the entire Hask category of types.

5. Going Further: Not All Things Read Can Be Created

code: https://gist.github.com/aaronlevin/4fc1fcfdce947a41567b#file-05-going-further-hs

Not only can we now express more general miniprograms indexed by different types, we can also express CRUD for types that may only handle the R (read) part of it! Let me show you.

Let's exapnd on our previous example by adding another Crudable type, ProductsR, which will represent the fact that our API exposes an endpoint to read a list of products, but not necessarily create a list of products. We will also be adding a Read constructor to CrudF, which means we'll need another type family to map our types to the type required to read them (usually this is an Integer to fetch an object from a database).

-- | new stuff! data Crudable = ProductCRUD | ProductsR | OrderCRUD -- | type family that maps a Crudable type to the type required to read it type family ReadData (c :: Crudable) :: * where ReadData 'ProductCRUD = Int ReadData 'ProductsR = String ReadData 'OrderCRUD = Int -- | type family that maps a Crudable type to the type required to create it -- | note that we dont include ProductsR as we cant create lists of products. type family CreateData (c :: Crudable) :: * where CreateData 'ProductCRUD = ProductData CreateData 'OrderCRUD = OrderData -- | we add ProductsR = [Product] to our CrudBase type family type family CrudBase (c :: Crudable) :: * where CrudBase 'ProductCRUD = Product CrudBase 'ProductsR = [Product] CrudBase 'OrderCRUD = Order -- | Here we add `Read5` to our GADT data CrudF5 next :: * where Create5 :: SCrudable c -> CreateData c -> (CrudBase c -> next) -> CrudF5 next Read5 :: SCrudable c -> ReadData c -> (Maybe (CrudBase c) -> next) -> CrudF5 next instance Functor CrudF4 where fmap f (Create5 c d g) = Create5 c d (f g) fmap f (Read5 c d g) = Read5 c d (f g)

Note that our CreateData type family is purposefully non-total as we cannot actually create lists of products. The intuition is that Shopify's HTTP endpoint might expose something like GET /api/products which returns a list of products, but it might not expose POST /api/products. However, we'd still like to express the fact that we can read lists of products through our API.

The beauty in this approach is that it is impossible to write a program that creates lists of products. We will get a compile time error! Check for yourself:

-- | smart constructor. we wont do pattern matching here. we only did it above -- | to highlight the usage of type families create5 :: SCrudable c -> CreateData c -> Free CrudF5 (CrudBase c) create5 c d = Free $ Create5 c d Pure -- | smart constructor for reading read5 :: SCrudable c -> ReadData c -> Free CrudF5 (Maybe (CrudBase c)) read5 c d = Free $ Read5 c d Pure -- | mini program that creates two products and an order workingProgram :: Free CrudF5 Order workingProgram = do (Just products) <- read5 SProductsR "select * from products" let productIds = productId <$> products create5 SOrderCRUD (OrderData "Lewis gripper" productIds)

The above program compiles. But the one below will not:

-- | this will not compile falseProgram :: Free CrudF5 [Product] falseProgram = create5 SProductsR [ProductData "Kit Ream"]

If you try to compile this you will get:

Couldn't match expected type ‘Main.CreateData 'Main.ProductsR’ with actual type ‘[Main.ProductData]’

It's not the most helpful method, but the key to it is here: expected type: Main.CreateData 'Main.ProductsR. Since CreateData was a non-total type family, CreateData SProductsR isn't defined and GHC throws an error!

6. A General Algebra for describing CRUD for shopify types

We are now ready for an entire CRUD algebra for Shopify types! You can see a full example with all constructors here: https://github.com/aaronlevin/haskell-shopify/blob/master/src/Network/API/Shopify/Client.hs

Near the bottom I've also provided an HTTP interpreter built on top of http-client for those curious as to what that might look like.

7. Summary and Next Steps

We started by attempting to wrap the Shopify API by using a Free Monad to express the possible actions against it. Starting with only two types, Product and Order, we saw that a naive functor expressing our actions would have eight constructors. As there are over twenty other types we'd need to wrap in the Shopify API, this would result in almost one hundred value constructors for our naive functor. Our first attempt at minimizing the constructors resulted in an algebra that wasn't composable across types, i.e., we were not able to express programs that created, updated, read, and deleted multiple types at once. To overcome this limitation, we used Type Families, Data Kinds, and GADTs to index our Functor, and the generated Free Monad, with types. This technique turned out to be flexible enough to capture actions against read-only endpoints (i.e. can't be created, updated, or deleted) as well.

There still remains a lot more to be done. For example, we could create a singleton type for each CRUD verb and reduce our CrudF to a single constructor. This would mean our type families might look like: type family CreateData (v :: CRUD) (c :: Crudable) :: *. Another step would be to expose this as a library via some Crudable typeclass, although I haven't thought too much about what this would look like (or if its possible in broader generality).

8. Bye

I hope this was valuable and that it gives some insight into how type-level programming in haskell may be practical and fun?