Skip to content

Instantly share code, notes, and snippets.

@clayrat clayrat/Const.idr

Created Aug 1, 2020
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.