Free CRUD pt. II

01-recap.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module FreeCrud where

-- | some user 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

02-user-defined-type-and-data-families.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module FreeCrud where

-- | 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 -> *

03-crud-library.hs

-- | kitchen sink of extensions

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module FreeCrud where

-- | 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

04-user-provided-types-and-kinds.hs

-- | kitchen sink of extensions

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module FreeCrud where

-- | 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

-- | 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 = Product
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 = Order
type instance ReturnData 'Update OrderCRUD = Order
type instance ReturnData 'Delete OrderCRUD = Order

05-y-u-no-compile.hs

-- | kitchen sink of extensions

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module FreeCrud where

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

-- | 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 :: 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 :: 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 = Product
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 = Order
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 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

06-using-typeclass-constraints-to-support-the-type-checker.hs

-- | kitchen sink of extensions

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverlappingInstances #-}
{-# 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

07-gods-in-its-own-heaven.hs

-- | kitchen sink of extensions

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverlappingInstances #-}
{-# 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 = Product
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 = Order
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 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