module Counter where open import Nat open import Identity {- The following is a record type implementing the abstract data type for counters (from 1), cf Pierce chapter 24. It serves the same role as the existential type in Pierce -} record counterADT : Set1 where field Counter : Set new : Counter get : Counter -> Nat inc : Counter -> Counter get-new : get new ≡ 1 get-inc : (c : Counter) → get (inc c) ≡ succ (get c) {- an implementation of an abstract data type is an element of the record implementing it. Again, note the similarity with elements of existential types in Pierce -} natCounter : counterADT natCounter = record { Counter = Nat ; new = 1 ; get = λ n → n ; inc = succ ; get-new = refl ; get-inc = λ c → refl } {- A binary counter, that is, where the Counter type is the type of binary numbers. Show that it implements the counterADT-record. -} data BinNat : Set where I : BinNat _O : BinNat → BinNat _L : BinNat → BinNat bin2nat : BinNat → Nat bin2nat I = 1 bin2nat (b O) = 2 * bin2nat b bin2nat (b L) = succ (2 * bin2nat b) binsucc : BinNat → BinNat binsucc I = I O binsucc (b O) = b L binsucc (b L) = binsucc b O binCounter = record { Counter = BinNat ; new = I ; get = bin2nat ; inc = binsucc ; get-new = refl ; get-inc = {!!} }