Monad and Functor laws in Idris

gistfile1.hs

module verified

---------- Functor ----------

-- Need this to avoid "Incomplete term" error
fmapid : Functor f => f a -> f a
fmapid = fmap id

class Functor f => VerifiedFunctor (f : Set -> Set) where
  identity : (fa : f a) -> fmapid fa = fa
  dist : (fa : f a) ->
        (g : b -> c) -> (h : a -> b) -> fmap (g . h) fa = (fmap g) . (fmap h) $ fa

instance VerifiedFunctor Maybe where
  identity Nothing = refl
  identity (Just _) = refl

  dist Nothing _ _ = refl
  dist (Just _) _ _  = refl

instance VerifiedFunctor List where
  identity [] = refl
  identity (x::xs) = let ih = (identity xs) in ?idList

  dist [] _ _ = refl
  dist (x::xs) g h  = let ih = (dist xs g h) in
                        ?distList

---------- Monad ----------

-- Need this to avoid "Incomplete term" error
bindReturn : Monad m => m a -> m a
bindReturn = (>>= return)

class Monad m => VerifiedMonad (m : Set -> Set) where
  left_id : (a : A) -> (ma : m A) -> (f : A -> m A) -> return a >>= f = f a
  right_id : (a : A) -> (ma : m A) -> bindReturn ma = ma
  assoc : (a : A) -> (ma : m A) -> (f : A -> m B) -> (g : B -> m C) ->
             (ma >>= f) >>= g = ma >>= (\x => f x >>= g)

instance VerifiedMonad Maybe where
  left_id _ Nothing _ = refl
  left_id _ (Just _) _ = refl

  right_id _ Nothing = refl
  right_id _ (Just _) = refl

  assoc a Nothing f g = refl
  assoc a (Just x) f g = refl

instance VerifiedMonad List where
  left_id a [] f = ?leftidListNil
  left_id a (x::xs) f = ?leftidList

  right_id _ [] = refl
  right_id a (x::xs) = let ih = (right_id a xs) in ?rightidList

  assoc a [] f g = refl
  assoc a (x::xs) f g = let ih = (assoc a xs f g) in ?assocList

---------- Helper Properties -----------

concatMapDistributesOverAppend : (l : List A) -> (r : List A) -> (f : A -> List B)
    -> concatMap f (l ++ r) = concatMap f l ++ concatMap f r
concatMapDistributesOverAppend [] [] f = refl
concatMapDistributesOverAppend (x::xs) [] f = ?cConsNil
concatMapDistributesOverAppend (x::xs) r f =
    let ih = (concatMapDistributesOverAppend xs r f) in ?cConsCons

---------- Proofs ----------

verified.assocList = proof {
    intros;
    rewrite ih;
    rewrite (concatMapDistributesOverAppend (f x) (concatMap f xs) g);
    refine refl;
}

verified.cConsCons = proof {
    intros;
    rewrite (sym ih);
    rewrite (appendAssociative (f x) (concatMap f xs) (concatMap f r));
    refine refl;
}

verified.cConsNil = proof {
    intros;
    rewrite (sym (appendNilRightNeutral xs));
    rewrite (sym (appendNilRightNeutral (f x ++ (concatMap f xs))));
    refine refl;
}

verified.leftidListNil = proof {
    intros;
    rewrite (appendNilRightNeutral (f a));
    refine refl;
}

verified.leftidList = proof {
    intros;
    rewrite (appendNilRightNeutral (f a));
    refine refl;
}

verified.rightidList = proof {
    intros;
    rewrite ih;
    refine refl;
}

verified.idList = proof {
    intros;
    rewrite ih;
    refine refl;
}

verified.distList = proof {
    intros;
    rewrite ih;
    refine refl;
}