Baby's first dependent type: Free Crud in Idris

crud.idr

module freecrud

-- | a really crud(e) and naive attempt at porting over "dependently"-typed haskell code to idris. 
-- original haskell code here: https://gist.github.com/aaronlevin/437ceac6acc344f86ef9
-- This is my first idris "program."

-- | crud lib

data CrudVerb = Create | Read

data CrudLib : (A : Type) -> (P : CrudVerb -> A -> Type) -> (Q : A -> Type) -> Type -> Type where
  MkCrudLib : {A : Type}
            -> {P : CrudVerb -> A -> Type}
            -> {Q : A -> Type}
            -> (v : CrudVerb)
            -> (a : A)
            -> P v a
            -> (Q a -> b)
            -> CrudLib A P Q b

instance Functor (CrudLib v p q) where
  map f (MkCrudLib v a d g) = MkCrudLib v a d (f . g)

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  MkFree : f (Free f a) -> Free f a

-- | user code

data Product = MkProduct
data ProductData = MkProductData
data Order = MkOrder
data OrderData = MkOrderData

data CrudIndex = PCrud | OCrud

inputIndex : CrudVerb -> CrudIndex -> Type
inputIndex Create PCrud = ProductData
inputIndex Create OCrud = OrderData
inputIndex Read   PCrud = Product
inputIndex Read   OCrud = Order

outputIndex : CrudIndex -> Type
outputIndex PCrud = Product
outputIndex OCrud = Order

create : (i : CrudIndex) -> inputIndex Create i -> Free (CrudLib CrudIndex inputIndex outputIndex) (outputIndex i)
create i d = MkFree (MkCrudLib Create i d Pure)

createProduct : (inputIndex Create PCrud) -> Free (CrudLib CrudIndex inputIndex outputIndex) (outputIndex PCrud)
createProduct = create PCrud

x : Free (CrudLib CrudIndex inputIndex outputIndex) Product
x = createProduct MkProductData