Skip to content

Instantly share code, notes, and snippets.

@paf31
Last active July 20, 2017 07:14
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 2 You must be signed in to fork a gist
  • Save paf31/67400d8fb0e037cf2519 to your computer and use it in GitHub Desktop.
Save paf31/67400d8fb0e037cf2519 to your computer and use it in GitHub Desktop.
Calculus of types in idris
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