Const.idr

module Const

import Interfaces.Verified

%default total

data Const : Type -> Type -> Type where
  MkConst : a -> Const a b

getConst : Const a b -> a
getConst (MkConst a) = a

Functor (Const a) where
  map _ (MkConst b) = MkConst b

VerifiedFunctor (Const a) where
  functorIdentity g prf (MkConst x) = Refl
  functorComposition (MkConst x) g1 g2 = Refl

Monoid a => Applicative (Const a) where
  pure _ = MkConst neutral
  (MkConst f) <*> (MkConst fa) = MkConst (f <+> fa)

-- we run into diamond inheritance here :(
VerifiedMonoid a => VerifiedApplicative (Const a) where
  applicativeMap (MkConst x) g = ?wot0 --rewrite monoidNeutralIsNeutralR x in Refl
  applicativeIdentity (MkConst x) = ?wot1 --rewrite monoidNeutralIsNeutralR x in Refl
  applicativeComposition (MkConst x) (MkConst g1) (MkConst g2) = ?wot2 --rewrite semigroupOpIsAssociative g2 g1 x in ?wat
  applicativeHomomorphism x g = ?wot3 --rewrite monoidNeutralIsNeutralR neutral in Refl
  applicativeInterchange x (MkConst g) = ?wot4 --rewrite monoidNeutralIsNeutralR g in rewrite monoidNeutralIsNeutralL g in Refl