Last active
April 29, 2025 09:05
-
-
Save kory33/40740cfca68e9a255768b264843afb1c to your computer and use it in GitHub Desktop.
ap による Applicative と product による Applicative
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| structure ApApplicative (F : Type u → Type v) where | |
| ---- 型クラスが提供する演算 | |
| pure : a → F a | |
| ap : F (a → b) → F a → F b | |
| ---- 拡張関数 | |
| map : (a → b) → F a → F b | |
| mapDefn : map f fa = ap (pure f) fa | |
| ---- 則 | |
| -- 関手則 | |
| covariantIdentity {fa : F a} : map id fa = fa | |
| covariantComposition {g : b → c} {f : a → b} {fa : F a} : map g (map f fa) = map (g ∘ f) fa | |
| -- ap と pure の相互作用則 | |
| applicativeHomomorphism {f : a → b} {x : a} : ap (pure f) (pure x) = pure (f x) | |
| applicativeInterchange {ff : F (a → b)} {x : a} : ap ff (pure x) = ap (pure (fun f => f x)) ff | |
| -- ap の一種の結合性 | |
| applyComposition {fab : F (a → b)} {fa : F a} {fbc : F (b → c)} : ap fbc (ap fab fa) = ap (ap (map (fun bc => fun ab => bc ∘ ab) fbc) fab) fa | |
| structure ProductApplicative (F : Type u → Type v) where | |
| ---- 型クラスが提供する演算 | |
| map : (a → b) → F a → F b | |
| pure : a → F a | |
| product : F a → F b → F (a × b) | |
| ---- 拡張関数 | |
| ev : (faba : F ((a → b) × a)) -> F b | |
| evDefn { faba : F ((a → b) × a) } : ev faba = map (fun ((ab, a)) => ab a) faba | |
| ---- 則 | |
| -- 関手則 | |
| covariantIdentity {fa : F a} : map id fa = fa | |
| covariantComposition {g : b → c} {f : a → b} {fa : F a} : map g (map f fa) = map (g ∘ f) fa | |
| -- product の片方が pure だったときの計算規則 | |
| pureProductEv {f : a → b} {fa : F a} : ev (product (pure f) fa) = map f fa | |
| productPureEv {ff : F (a → b)} {x : a} : ev (product ff (pure x)) = map (fun f => f x) ff | |
| -- product の結合則 | |
| productAssociative {fa : F a} {fb : F b} {fc : F c} : map (fun (a, (b, c)) => (a, b, c)) (product fa (product fb fc)) | |
| = map (fun ((a, b), c) => (a, b, c)) (product (product fa fb) fc) | |
| -- product の自然性（一般に、双関手間の変換（今回は product : (F-)×(F-) ⇒ F(-×-)）の自然性は引数ごとの自然性と同値） | |
| productLeftNaturality {fa : F a} {fb : F b} {ac : a → c} : product (map ac fa) fb = map (fun (a, b) => (ac a, b)) (product fa fb) | |
| productRightNaturality {fa : F a} {fb : F b} {bc : b → c} : product fa (map bc fb) = map (fun (a, b) => (a, bc b)) (product fa fb) | |
| -- pure の自然性 | |
| pureNaturality {f : a → b} {x : a} : pure (f x) = map f (pure x) | |
| -- ApApplicative についての補題 | |
| def ApApplicative.mapPure (inst : ApApplicative F) {f : a → b} {x : a} : | |
| inst.map f (inst.pure x) = inst.pure (f x) := by | |
| rw [inst.mapDefn, applicativeHomomorphism] | |
| def ApApplicative.mapAp (inst : ApApplicative F) {fab : F (a → b)} {fa : F a} {bc : b → c} : | |
| inst.map bc (inst.ap fab fa) = inst.ap (inst.map (fun ab => bc ∘ ab) fab) fa := by | |
| rw [inst.mapDefn, inst.mapDefn, applyComposition, mapPure] | |
| def ApApplicative.apMap (inst : ApApplicative F) {fa : F a} {ab : a → b} {fbc : F (b → c)} : | |
| inst.ap fbc (inst.map ab fa) = inst.ap (inst.map (fun bc => bc ∘ ab) fbc) fa := by | |
| rw [inst.mapDefn, applyComposition, inst.applicativeInterchange, ←inst.mapDefn, inst.covariantComposition] | |
| unfold Function.comp; dsimp only | |
| -- ApApplicative → ProductApplicative | |
| def ApApplicative.toProductApplicative {F : Type u → Type v} (inst : ApApplicative F) : ProductApplicative F := | |
| { | |
| ---- 実装 | |
| map := inst.map, | |
| pure := inst.pure, | |
| product fa fb := inst.ap (inst.map (fun a => fun b => (a, b)) fa) fb, | |
| ---- 拡張関数 | |
| ev {a b} (faba : F ((a → b) × a)) := inst.map (fun (ab, a) => ab a) faba, | |
| evDefn := by simp, | |
| ---- 則 | |
| covariantIdentity := inst.covariantIdentity, | |
| covariantComposition := inst.covariantComposition, | |
| pureProductEv := by | |
| intros _ _ f fa | |
| simp only [inst.mapDefn] | |
| rw [inst.applicativeHomomorphism] | |
| repeat rw [←inst.mapDefn] | |
| rw [inst.covariantComposition] | |
| congr | |
| productPureEv := by | |
| intros _ _ ff x | |
| simp only [inst.mapDefn] | |
| rw [inst.applicativeInterchange] | |
| repeat rw [←inst.mapDefn] | |
| repeat rw [inst.covariantComposition] | |
| congr | |
| productAssociative := by | |
| intros a b c fa fb fc | |
| dsimp only | |
| simp only [inst.applyComposition, inst.covariantComposition, inst.apMap, inst.mapAp] | |
| unfold Function.comp; dsimp only, | |
| productLeftNaturality := by | |
| intros _ _ _ fa fb ac | |
| dsimp only | |
| simp only [inst.covariantComposition, inst.mapAp] | |
| unfold Function.comp; dsimp only | |
| productRightNaturality := by | |
| intros _ _ _ fa fb bc | |
| dsimp only | |
| simp only [inst.apMap, inst.covariantComposition, inst.mapAp] | |
| unfold Function.comp; dsimp only | |
| pureNaturality := by | |
| intros _ _ f x | |
| dsimp only | |
| simp only [inst.mapDefn] | |
| rw [inst.applicativeHomomorphism] | |
| } | |
| -- ProductApplicative → ApApplicative | |
| def ProductApplicative.toApApplicative {F : Type u → Type v} (inst : ProductApplicative F) : ApApplicative F := | |
| let ap {a b : Type u} (fab : F (a → b)) (fa : F a) := inst.ev (inst.product fab fa) | |
| { | |
| ---- 実装 | |
| pure := inst.pure, | |
| ap := ap, | |
| ---- 拡張関数 | |
| map := inst.map, | |
| mapDefn := by | |
| -- inst.map でも ap (pure f) fa でも一致する | |
| -- ことの証明になっている | |
| intros _ _ f fa | |
| dsimp only; unfold ap | |
| rw [inst.pureProductEv] | |
| ---- 則 | |
| covariantIdentity := inst.covariantIdentity, | |
| covariantComposition := inst.covariantComposition, | |
| applicativeHomomorphism := by | |
| intros _ _ f x | |
| dsimp only; unfold ap | |
| rw [inst.pureProductEv, inst.pureNaturality] | |
| applicativeInterchange := by | |
| intros _ _ ff x | |
| dsimp only; unfold ap | |
| rw [inst.productPureEv, inst.pureProductEv] | |
| applyComposition := by | |
| intros _ _ _ fab fa fbc; dsimp only | |
| simp only [ap, inst.evDefn, inst.productLeftNaturality, inst.productRightNaturality, inst.covariantComposition] | |
| unfold Function.comp; dsimp only | |
| have lhs_with_intermediate_map : | |
| inst.map (fun (bc, (ab, a)) => bc (ab a)) (inst.product fbc (inst.product fab fa)) | |
| = inst.map (fun (bc, ab, a) => bc (ab a)) (inst.map (fun (bc, (ab, a)) => (bc, ab, a)) (inst.product fbc (inst.product fab fa))) := by | |
| simp only [inst.covariantComposition]; congr | |
| rw [lhs_with_intermediate_map, inst.productAssociative, inst.covariantComposition] | |
| dsimp only; congr | |
| } | |
| ---- toProductApplicative と toApApplicative は互いに逆 | |
| theorem apToProdToAp {F : Type u → Type v} : ProductApplicative.toApApplicative ∘ ApApplicative.toProductApplicative (F := F) = id := by | |
| ext inst | |
| unfold ProductApplicative.toApApplicative ApApplicative.toProductApplicative; simp | |
| -- （Lean は proof-irrelevant なので）等価性が非自明なのは ap と product だけ (他の関数は definitional に等しい)。 | |
| -- 今回は ProductApplicative.toApApplicative(ApApplicative.toProductApplicative(inst)).ap = inst.ap を示す | |
| congr | |
| ext a b fab fa | |
| simp [ApApplicative.mapAp, inst.covariantComposition] | |
| unfold Function.comp; dsimp only | |
| congr | |
| conv => rhs; rw [←inst.covariantIdentity (fa := fab)] | |
| congr | |
| theorem prodToApToProd {F : Type u → Type v} : ApApplicative.toProductApplicative ∘ ProductApplicative.toApApplicative (F := F) = id := by | |
| ext inst | |
| unfold ApApplicative.toProductApplicative ProductApplicative.toApApplicative; simp | |
| -- 今回は | |
| -- - ApApplicative.toProductApplicative(ProductApplicative.toApApplicative(inst)).product = inst.product | |
| -- - ApApplicative.toProductApplicative(ProductApplicative.toApApplicative(inst)).ev = inst.ev (こちらは展開すると自明) | |
| -- を示す | |
| congr | |
| · ext a b fa fb | |
| simp [inst.evDefn, inst.productLeftNaturality, inst.covariantComposition] | |
| unfold Function.comp; dsimp only | |
| conv => rhs; rw [←inst.covariantIdentity (fa := inst.product fa fb)] | |
| congr | |
| · ext a b faba; simp only [inst.evDefn] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment