Last active
July 20, 2017 07:14
-
-
Save paf31/67400d8fb0e037cf2519 to your computer and use it in GitHub Desktop.
Calculus of types in idris
This file contains 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
| module Deriv | |
| import Control.Isomorphism | |
| -- | |
| -- A type constructor df is the derivative of the type constructor f if for all x and e there exists d such | |
| -- such that | |
| -- | |
| -- f (x + e) ~ f x + e * (df x) + e^2 * d | |
| -- | |
| -- ie. df approximates f up to a second order term at x. | |
| -- | |
| -- DWit is a witness to this isomorphism at x and e. | |
| -- | |
| data DWit : (f : Type -> Type) -> (df : Type -> Type) -> (x : Type) -> (e : Type) -> Type where | |
| dWit : (d : Type) -> (Iso (f (Either x e)) (Either (f x) (Either (e, df x) ((e, e), d)))) -> DWit f df x e | |
| -- | |
| -- d is a witness to the fact that for any choice of x and e there exists an appropriate d | |
| -- | |
| d : (Type -> Type) -> (Type -> Type) -> Type | |
| d f df = (x : Type) -> (e : Type) -> DWit f df x e | |
| -- | |
| -- As a first example, let's show that the derivative of a constant function is the constantly bottom function | |
| -- | |
| data Const : (a : Type) -> (t : Type) -> Type where | |
| MkConst : a -> Const a t | |
| runConst : { a : Type } -> { t : Type } -> Const a t -> a | |
| runConst (MkConst a) = a | |
| runConstInverseToMkConst : (x : Const a b) -> MkConst { t = b } (runConst x) = x | |
| runConstInverseToMkConst (MkConst a) = refl | |
| -- | |
| -- Lemma: Const a b ~ a | |
| -- | |
| constIso : Iso (Const a b) a | |
| constIso = MkIso runConst MkConst (\x => refl) (\x => runConstInverseToMkConst x) | |
| dUnit : d (Const a) (Const _|_) | |
| dUnit = \x => \e => dWit _|_ ?dUnitProof | |
| Deriv.dUnitProof = proof | |
| intros | |
| refine isoTrans | |
| refine constIso | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine constIso | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCong | |
| refine isoTrans | |
| refine pairCongRight | |
| refine constIso | |
| refine pairBotRight | |
| refine pairBotRight | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherBotLeft | |
| refine eitherBotRight | |
| -- | |
| -- The derivative of the identity functor is constantly unit | |
| -- | |
| data Id : (a : Type) -> Type where | |
| MkId : a -> Id a | |
| runId : { a : Type } -> Id a -> a | |
| runId (MkId a) = a | |
| runIdInverseToMkId : (x : Id a) -> MkId (runId x) = x | |
| runIdInverseToMkId (MkId a) = refl | |
| -- | |
| -- Lemma: Id a ~ a | |
| -- | |
| idIso : Iso (Id a) a | |
| idIso = MkIso runId MkId (\x => refl) (\x => runIdInverseToMkId x) | |
| dId : d Id (Const ()) | |
| dId = \x => \e => dWit _|_ ?dIdProof | |
| Deriv.dIdProof = proof | |
| intros | |
| refine isoTrans | |
| refine idIso | |
| refine eitherCong | |
| exact (isoSym idIso) | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCong | |
| refine pairCongRight | |
| refine constIso | |
| refine pairBotRight | |
| refine isoTrans | |
| refine eitherBotRight | |
| refine pairUnitRight | |
| -- | |
| -- Derivative of a sum is the sum of derivatives | |
| -- | |
| data Sum : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where | |
| MkSum : Either (f a) (g a) -> Sum f g a | |
| runSum : Sum f g x -> Either (f x) (g x) | |
| runSum (MkSum x) = x | |
| runSumInverseToMkSum : (x : Sum f g a) -> MkSum (runSum x) = x | |
| runSumInverseToMkSum (MkSum x) = refl | |
| sumIso : Iso (Sum f g x) (Either (f x) (g x)) | |
| sumIso = MkIso runSum MkSum (\x => refl) (\x => runSumInverseToMkSum x) | |
| dEither : d f1 df1 -> d f2 df2 -> d (Sum f1 f2) (Sum df1 df2) | |
| dEither d1 d2 = \x => \e => let (dWit dt1 iso1) = d1 x e in | |
| let (dWit dt2 iso2) = d2 x e in | |
| dWit (Either dt1 dt2) ?dEitherProof | |
| Deriv.dEitherProof = proof | |
| intros | |
| refine isoTrans | |
| refine sumIso | |
| refine isoTrans | |
| refine eitherCong | |
| refine iso1 | |
| refine iso2 | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine sumIso | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongLeft | |
| refine pairCongRight | |
| refine sumIso | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCong | |
| refine distribRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongRight | |
| refine eitherAssoc | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongRight | |
| refine eitherAssoc | |
| refine eitherCongRight | |
| refine eitherCongRight | |
| refine isoSym | |
| refine isoTrans | |
| refine isoSym | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine eitherCongRight | |
| refine isoTrans | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine eitherCongRight | |
| refine isoRefl | |
| -- | |
| -- Derivative of a product by the Leibniz rule | |
| -- | |
| data Prod : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where | |
| MkProd : (f a, g a) -> Prod f g a | |
| runProd : Prod f g x -> (f x, g x) | |
| runProd (MkProd x) = x | |
| runProdInverseToMkProd : (x : Prod f g a) -> MkProd (runProd x) = x | |
| runProdInverseToMkProd (MkProd x) = refl | |
| prodIso : Iso (Prod f g x) (f x, g x) | |
| prodIso = MkIso runProd MkProd (\x => refl) (\x => runProdInverseToMkProd x) | |
| dProd : d f1 df1 -> d f2 df2 -> d (Prod f1 f2) (Sum (Prod f1 df2) (Prod f2 df1)) | |
| dProd d1 d2 = \x => \e => let (dWit dt1 iso1) = d1 x e in | |
| let (dWit dt2 iso2) = d2 x e in | |
| dWit (Either (df1 x, df2 x) | |
| (Either (f1 x, dt2) | |
| (Either (f2 x, dt1) | |
| (Either (e, (df1 x, dt2)) | |
| (Either (e, (df2 x, dt1)) | |
| ((e, e), (dt1, dt2))))))) ?dProdProof | |
| Deriv.dProdProof = proof | |
| intros | |
| refine isoTrans | |
| refine prodIso | |
| refine isoTrans | |
| refine pairCong | |
| refine iso1 | |
| refine iso2 | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCong | |
| refine prodIso | |
| refine eitherCongLeft | |
| refine pairCongRight | |
| refine sumIso | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongLeft | |
| refine pairCongRight | |
| refine eitherCong | |
| refine prodIso | |
| refine prodIso | |
| refine isoSym | |
| refine isoTrans | |
| refine distribLeft | |
| refine isoTrans | |
| refine eitherCong | |
| refine distribRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherCong | |
| refine eitherCongRight | |
| refine distribRight | |
| refine eitherCongRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine eitherCongRight | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCong | |
| refine distribRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine pairAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine pairCongLeft | |
| refine pairComm | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine isoSym | |
| refine pairAssoc | |
| refine eitherCongRight | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongLeft | |
| refine distribLeft | |
| refine isoTrans | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine isoSym | |
| refine pairAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine pairCongRight | |
| refine pairComm | |
| refine eitherCongRight | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongLeft | |
| refine eitherCongLeft | |
| refine distribLeft | |
| refine isoTrans | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine eitherCong | |
| refine isoTrans | |
| refine pairAssoc | |
| refine isoSym | |
| refine isoTrans | |
| refine pairAssoc | |
| refine pairCongLeft | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine isoSym | |
| refine isoTrans | |
| refine pairComm | |
| refine pairCongRight | |
| exact isoRefl | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine eitherCong | |
| refine isoTrans | |
| refine pairComm | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| exact pairComm | |
| refine isoSym | |
| refine isoTrans | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine distribRight | |
| refine isoTrans | |
| refine eitherCongRight | |
| refine eitherCongRight | |
| refine distribRight | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoTrans | |
| refine eitherCongLeft | |
| refine isoSym | |
| refine pairAssoc | |
| refine eitherCong | |
| refine pairCongRight | |
| exact pairComm | |
| refine isoSym | |
| refine isoTrans | |
| refine eitherComm | |
| refine isoTrans | |
| refine eitherAssoc | |
| refine isoSym | |
| refine eitherCong | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| refine isoTrans | |
| refine pairAssoc | |
| refine isoTrans | |
| refine pairCongLeft | |
| refine pairComm | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| exact pairComm | |
| refine isoTrans | |
| refine distribLeft | |
| refine isoTrans | |
| refine eitherComm | |
| refine eitherCong | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| refine isoTrans | |
| refine pairComm | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| exact pairComm | |
| refine isoTrans | |
| refine pairComm | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine pairCongRight | |
| refine isoTrans | |
| refine pairComm | |
| refine isoTrans | |
| refine isoSym | |
| refine pairAssoc | |
| refine isoRefl | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment