GetTypes.agda

   1 module GetTypes where
   2
   3 open import Level using () renaming (zero to ℓ₀)
   4 open import Data.Nat using (ℕ)
   5 open import Data.List using (List ; map)
   6 open import Data.Vec using (Vec) renaming (map to mapV)
   7 open import Function using (_∘_)
   8 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
   9 open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
  10 open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
  11 open import Relation.Binary using (Setoid)
  12 open Injection using (to)
  13
  14 open import Generic using (≡-to-Π)
  15
  16 module ListList where
  17   record Get : Set₁ where
  18     field
  19       get : {A : Set} → List A → List A
  20       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
  21
  22 module VecVec where
  23   record Get : Set₁ where
  24     field
  25       getlen : ℕ → ℕ
  26       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
  27       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
  28
  29 module PartialVecVec where
  30   record Get : Set₁ where
  31     field
  32       I : Setoid ℓ₀ ℓ₀
  33       gl₁ : I ↪ EqSetoid ℕ
  34       gl₂ : I ⟶ EqSetoid ℕ
  35
  36     |I|   = Setoid.Carrier I
  37     |gl₁| = _⟨$⟩_ (to gl₁)
  38     |gl₂| = _⟨$⟩_ gl₂
  39
  40     field
  41       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
  42       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
  43
  44 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
  45 VecVec-to-PartialVecVec G = record
  46   { I = EqSetoid ℕ
  47   ; gl₁ = id↪
  48   ; gl₂ = ≡-to-Π getlen
  49   ; get = get
  50   ; free-theorem = free-theorem
  51   } where open VecVec.Get G