Theory Applicative_Sum
subsection ‹Sum types›
theory Applicative_Sum imports
Applicative
"HOL-Library.Adhoc_Overloading"
begin
text ‹
There are several ways to define an applicative functor based on sum types. First, we can choose
whether the left or the right type is fixed. Both cases are isomorphic, of course. Next, what
should happen if two values of the fixed type are combined? The corresponding operator must be
associative, or the idiom laws don't hold true.
We focus on the cases where the right type is fixed. We define two concrete functors: One based
on Haskell's \textsf{Either} datatype, which prefers the value of the left operand, and a generic
one using the @{class semigroup_add} class. Only the former lifts the \textbf{W} combinator,
though.
›
fun ap_sum :: "('e ⇒ 'e ⇒ 'e) ⇒ ('a ⇒ 'b) + 'e ⇒ 'a + 'e ⇒ 'b + 'e"
where
"ap_sum _ (Inl f) (Inl x) = Inl (f x)"
| "ap_sum _ (Inl _) (Inr e) = Inr e"
| "ap_sum _ (Inr e) (Inl _) = Inr e"
| "ap_sum c (Inr e1) (Inr e2) = Inr (c e1 e2)"
abbreviation "ap_either ≡ ap_sum (λx _. x)"
abbreviation "ap_plus ≡ ap_sum (plus :: 'a :: semigroup_add ⇒ _)"
abbreviation (input) pure_sum where "pure_sum ≡ Inl"
adhoc_overloading Applicative.pure pure_sum
adhoc_overloading Applicative.ap ap_either
lemma ap_sum_id: "ap_sum c (Inl id) x = x"
by (cases x) simp_all
lemma ap_sum_ichng: "ap_sum c f (Inl x) = ap_sum c (Inl (λf. f x)) f"
by (cases f) simp_all
lemma (in semigroup) ap_sum_comp:
"ap_sum f (ap_sum f (ap_sum f (Inl (o)) h) g) x = ap_sum f h (ap_sum f g x)"
by(cases h g x rule: sum.exhaust[case_product sum.exhaust, case_product sum.exhaust])
(simp_all add: local.assoc)
lemma semigroup_const: "semigroup (λx y. x)"
by unfold_locales simp
locale either_af =
fixes B :: "'b ⇒ 'b ⇒ bool"
assumes B_refl: "reflp B"
begin
applicative either (W)
for
pure: Inl
ap: ap_either
rel: "λA. rel_sum A B"
proof -
include applicative_syntax
{ fix f :: "('c ⇒ 'c ⇒ 'd) + 'a" and x
show "pure (λf x. f x x) ⋄ f ⋄ x = f ⋄ x ⋄ x"
by (cases f x rule: sum.exhaust[case_product sum.exhaust]) simp_all
next
interpret semigroup "λx y. x" by(rule semigroup_const)
fix g :: "('d ⇒ 'e) + 'a" and f :: "('c ⇒ 'd) + 'a" and x
show "pure (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
by(rule ap_sum_comp[simplified comp_def[abs_def]])
next
fix R and f :: "('c ⇒ 'd) + 'b" and g :: "('c ⇒ 'e) + 'b" and x
assume "rel_sum (rel_fun (eq_on UNIV) R) B f g"
then show "rel_sum R B (f ⋄ x) (g ⋄ x)"
by (cases f g x rule: sum.exhaust[case_product sum.exhaust, case_product sum.exhaust])
(auto intro: B_refl[THEN reflpD] elim: rel_funE)
}
qed (auto intro: ap_sum_id[simplified id_def] ap_sum_ichng)
end
interpretation either_af "(=)" by unfold_locales simp
applicative semigroup_sum
for
pure: Inl
ap: ap_plus
using
ap_sum_id[simplified id_def]
ap_sum_ichng
add.ap_sum_comp[simplified comp_def[abs_def]]
by auto
no_adhoc_overloading Applicative.pure pure_sum
end