--------------------------------------------------------------------------------
--
---- Logic IV: Datatype-generic theories for dependently typed programming
--
---- Josh Ko (Institute of Information Science, Academia Sinica, Taiwan)
--
--------------------------------------------------------------------------------
-- This file imports the ‘Native Datatype-Generic Programming’ library
-- hosted at https://github.com/josh-hs-ko/NDGP.
open import Prelude
open import Data.Vec hiding (length)
open import Generics.Description
open import Generics.Recursion
open import Generics.Reflection
open import Generics.RecursionScheme
open import Generics.Ornament
open import Generics.Ornament.Description
open import Generics.Ornament.Algebraic
open import Generics.Ornament.Algebraic.Isomorphism
-- Since dependently typed programming depends heavily on designing various
-- indexed datatypes, we need to develop powerful theories of datatypes to
-- make sense of what we’re doing, as well as identify and provide reusable
-- constructions.
-- A simplest example is the theorem
--
-- ‘There is an induction principle for any datatype.’
--
-- This theorem can be formalised datatype-generically, and used to generate
-- the induction principle of (roughly speaking) any datatype with the help of
-- Agda’s metaprogramming mechanism. The generated induction principle, which
-- is a type, comes with a proof/program, and the generation is (intrinsically)
-- proved to produce correct types and programs.
-- For example, we can generate induction principles for natural numbers and
-- lists,
instance
NatC : Named (quote ℕ) _
unNamed NatC = genDataC NatD (genDataT NatD ℕ)
where NatD = genDataD ℕ
ListC : Named (quote List) _
unNamed ListC = genDataC ListD (genDataT ListD List)
where ListD = genDataD List
ListFin : Finitary (findDataD (quote List))
ListFin = [] ∷ (tt ∷ refl ∷ []) ∷ []
unquoteDecl indℕ = defineInd (ind-operator (quote ℕ)) indℕ
unquoteDecl indList = defineInd (ind-operator (quote List)) indList
-- and even for a rather sophisticated datatype (‘BT’ below) that can be used
-- to quantify over all sublists of a particular length:
variable
n k : ℕ
A : Set
P : A → Set
x : A
xs : Vec _ _
data BT : (n k : ℕ) → (Vec A k → Set) → Vec A n → Set₁ where
tipZ : P [] → BT n zero P xs
tipS : P xs → BT (suc k) (suc k) P xs
bin : BT n (suc k) P xs
→ BT n k (λ zs → P (x ∷ zs)) xs → BT (suc n) (suc k) P (x ∷ xs)
-- testBT : BT 4 2 P ('a' ∷ 'b' ∷ 'c' ∷ 'd' ∷ [])
-- testBT = bin (bin (tipS {! !})
-- (bin (tipS {! !})
-- (tipZ {! !})))
-- (bin (bin (tipS {! !})
-- (tipZ {! !}))
-- (tipZ {! !}))
instance
BTC : Named (quote BT) _
unNamed BTC = genDataC BTD (genDataT BTD BT)
where BTD = genDataD BT
unquoteDecl indBT = defineInd (ind-operator (quote BT)) indBT
-- There’s a common pattern shared by BT and the double negation monad (!)
-- called the continuation-passing style (CPS). CPS has been extensively
-- studied in functional programming, but never discussed in the context of
-- indexed datatypes. More generally, there’s probably a close relationship
-- between certain indexed datatypes and programs (such as BT and the program
-- that nondeterministically chooses a sublist from a list) — I’m thinking
-- about formalising this relationship and exploring its consequences.
-- Another example of datatype-generic theories is the theory of ‘ornaments’.
-- An ornament is a ‘diff’ between datatypes — for example, the difference
-- between the datatypes of lists and natural numbers is that lists take an
-- element in the inductive case.
instance
ListO : DataO (findDataD (quote List)) (findDataD (quote ℕ))
ListO = record
{ level = λ _ → tt
; applyL = λ (ℓ , _) → record
{ param = λ _ → tt
; index = λ _ _ → tt
; applyP = λ _ → ι ∷ ∺ (Δ[ _ ] ρ ι ι) ∷ ∺ [] } }
-- From the ornament, first we can generate the length function.
private
lengthP : FoldP
lengthP = forget (quote List) (quote ℕ)
instance
lengthC = genFoldC lengthP length
-- Then, from the datatype of lists and the length function, we can generate
-- the datatype of vectors, because the indices in the definition of vectors
-- are exactly computed by length.
--
-- In general, the theory allows us to fuse a fold function on a datatype into
-- that datatype and get an indexed variant of the datatype.
private
VectOD : DataOD (findDataD (quote List))
VectOD = AlgOD lengthP
instance
VectO = ⌈ VectOD ⌉ᵈ
unquoteDecl data Vect constructor [] _∷_ =
defineByDataD ⌊ VectOD ⌋ᵈ Vect (Vect.[] List.∷ Vect._∷_ List.∷ List.[])
-- And then the theory proves in general that there are isomorphisms such as
--
-- Vect A n ≅ Σ[ xs ∶ List A ] length xs ≡ n
--
-- formalising the idea that vectors are lists fused with length proofs. (We
-- could go on and think about how to fuse other forms of proof and manufacture
-- more sophisticated indexed datatypes systematically.)
instance
VectC : Named (quote Vect) _
unNamed VectC = genDataC ⌊ VectOD ⌋ᵈ (genDataT ⌊ VectOD ⌋ᵈ Vect)
private
fromVectP : FoldP
fromVectP = forget (quote Vect) (quote List)
unquoteDecl fromVect = defineFold fromVectP fromVect
instance
fromVectC = genFoldC fromVectP fromVect
private
toVectP : IndP
toVectP = remember (quote Vect)
unquoteDecl toVect = defineInd toVectP toVect
instance
toVectC = genIndC toVectP toVect
private
from-toVectP : IndP
from-toVectP = forget-remember-inv (quote Vect) (quote List) (inl it)
unquoteDecl from-toVect = defineInd from-toVectP from-toVect
private
to-fromVectP : IndP
to-fromVectP = remember-forget-inv (quote Vect) (quote List) (inl it)
unquoteDecl to-fromVect = defineInd to-fromVectP to-fromVect
--------------------------------------------------------------------------------
--
---- Conclusions
--
-- Like in logic, we not only use a language (or deduction system) but also
-- prove theorems (that is, formulate general constructions) about it.
--
-- We like programming, and we want to study it using mathematical methods
-- to figure out how to write better programs.
--
--------------------------------------------------------------------------------