N-ary Products à la Andres Löh but in Agda

NP.agda

module NP where

open import Level as L using (Level)
open import Data.Nat
open import Data.List
open import Data.String as String hiding (show)
open import Function

data NP {ℓ ℓ′ : Level} (f : Set ℓ → Set ℓ′) :
        (xs : List (Set ℓ)) → Set (L.suc ℓ L.⊔ ℓ′) where
  []  : NP f []
  _∷_ : ∀ {x xs} (hd : f x) (tl : NP f xs) → NP f (x ∷ xs)

hpure : ∀ {ℓ ℓ′} {f : Set ℓ → Set ℓ′} {xs} (p : ∀ {a} → f a) → NP f xs
hpure {xs = []}     p = [] 
hpure {xs = x ∷ xs} p = p ∷ hpure p 

record Top {ℓ} : Set ℓ where

record Both {ℓ ℓ′} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ L.⊔ ℓ′) where
  constructor _,_
  field
    fst : A
    snd : B
open Both

All : {ℓ ℓ′ : Level} (c : Set ℓ → Set ℓ′) (xs : List (Set ℓ)) → Set ℓ′
All c []       = Top
All c (x ∷ xs) = Both (c x) (All c xs) 

hcpure : ∀ {ℓ ℓ′ ℓᶜ} {f : Set ℓ → Set ℓ′} {c : Set ℓ → Set ℓᶜ} {xs} {{_ : All c xs}} (p : ∀ {a} {{_ : c a}} → f a) → NP f xs
hcpure {xs = []}            p = [] 
hcpure {xs = x ∷ xs} {{cs}} p = p {{fst cs}} ∷ hcpure {{snd cs}} p

hcmap : ∀ {ℓ ℓ′ ℓ′′ ℓᶜ} {f : Set ℓ → Set ℓ′} {g : Set ℓ → Set ℓ′′} {c : Set ℓ → Set ℓᶜ} {xs}
        {{_ : All c xs}} (p : ∀ {a} {{_ : c a}} → f a → g a) → NP f xs → NP g xs
hcmap        p []       = [] 
hcmap {{cs}} p (v ∷ vs) = p {{fst cs}} v ∷ hcmap {{snd cs}} p vs

instance

  top : {ℓ : Level} → Top {ℓ}
  top = record {}

  pair : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} {{pA : A}} {{pB : B}} → Both A B
  pair {{pA}} {{pB}} = pA , pB

record Show {ℓ : Level} (A : Set ℓ) : Set ℓ where
  constructor mkShow
  field
    show : A → String

record Default {ℓ : Level} (A : Set ℓ) : Set ℓ where
  constructor mkDefault
  field
    default : A

instance

  showString : Show String
  showString = mkShow show
    where open import Data.String

  showNat : Show ℕ
  showNat = mkShow show
    where open import Data.Nat.Show

  defaultString : Default String
  defaultString = mkDefault ""

  defaultNat : Default ℕ
  defaultNat = mkDefault 0

show : {ℓ : Level} {A : Set ℓ} {{_ : Show A}} → A → String
show {{sA}} = Show.show sA

default : {ℓ : Level} {A : Set ℓ} {{_ : Default A}} → A
default {{dA}} = Default.default dA

example : NP {L.zero} {L.zero} (λ _ → String) (ℕ ∷ String ∷ [])
example = hcmap show (hcpure {f = id} default)