naryapplicative.agda

module naryapplicative where

open import Agda.Primitive

module Functor
  where

  record functor { ℓ } (f : Set ℓ → Set ℓ) : Set (lsuc ℓ)
    where
    field
      _<$>_ : ∀ { a b } → (a → b) → f a → f b

open Functor
open functor ⦃ ... ⦄

module Applicative
  where

  record applicative { ℓ } (f : Set ℓ → Set ℓ) : Set (lsuc ℓ)
    where
    field
      ⦃ functorF ⦄ : functor { ℓ } f
      pure : ∀ { a } → a → f a
      _<*>_ : ∀ { a b } → f (a → b) → f a → f b

open Applicative
open applicative ⦃ ... ⦄

module Nat
  where

  data nat : Set
    where
    zero : nat
    succ : nat → nat

  {-# BUILTIN NATURAL nat #-}

  _+_ : nat → nat → nat
  0 + x = x
  succ x + y = succ (x + y)

open Nat

module Bool
  where

  data bool : Set
    where
    true : bool
    false : bool

open Bool

module Vec
  where

  data vec { ℓ } : nat → Set ℓ → Set ℓ
    where
    [] : ∀ { a } → vec 0 a
    _∷_ : ∀ { n } { a } → a → vec n a → vec (succ n) a

  infixr 5 _∷_

  replicate : ∀ { ℓ } { a : Set ℓ } → (n : nat) → a → vec n a
  replicate zero _ = []
  replicate (succ n) a = a ∷ replicate n a

  lift2 : ∀ { ℓ } { n } { a b c : Set ℓ } → (a → b → c) → vec n a → vec n b → vec n c
  lift2 _ [] [] = []
  lift2 f (x ∷ xs) (y ∷ ys) = f x y ∷ lift2 f xs ys

  instance
    vf : ∀ { ℓ } { n } → functor { ℓ } (vec n)
    vf = record
      { _<$>_ = λ
          { f [] → []
          ; f (x ∷ xs) → f x ∷ f <$> xs
          }
      }

    va : ∀ { ℓ } { n } → applicative { ℓ } (vec n)
    va { ℓ } { n } = record
      { pure = replicate n
      ; _<*>_ = lift2 (λ f → f)
      }

open Vec

module Function
  where
  nary : ∀ { ℓ } { n } → vec n (Set ℓ) → Set ℓ → Set ℓ
  nary [] r = r
  nary (x ∷ xs) r = x → nary xs r

open Function

module Exists
  where

  data Σ { κ ℓ } { a : Set κ } (f : a → Set ℓ) : Set (κ ⊔ ℓ)
    where
    ∃ : ∀ { x } → f x → Σ f

open Exists

module HList
  where

  data hlist { ℓ } : ∀ { n } → vec n (Set ℓ) → Set ℓ
    where
    ∎ : hlist []
    _,_ : ∀ { n } { x : Set ℓ } { xs : vec n (Set ℓ) } → x → hlist xs → hlist (x ∷ xs)

  infixr 2 _,_

open HList

module List
  where

  list : ∀ { ℓ } → Set ℓ → Set ℓ
  list a = Σ (λ n → vec n a)

module FreeApplicative
  where

  data freeF { n } (fs : vec n (Set → Set)) (a : Set) : Set₁
    where
    _<‥*‥>_ : ∀ { xs } → nary xs a → hlist (fs <*> xs) → freeF fs a

  free : (Set → Set) → Set → Set₁
  free f a = Σ (λ n → freeF (replicate n f) a)

  test : free (vec 3) bool
  test = ∃ (and <‥*‥> (v1 , v2 , ∎))
    where
    and : bool → bool → bool
    and true x = x
    and _    _ = false

    v1 : vec 3 bool
    v1 = true ∷ false ∷ true ∷ []

    v2 : vec 3 bool
    v2 = false ∷ true ∷ true ∷ []

  interpret : ∀ { f } { a } ⦃ _ : applicative f ⦄ → free f a → f a
  interpret (∃ {zero}   (v <‥*‥> _)) = ?
  interpret (∃ {succ n} (v <‥*‥> xs)) = ?

open Applicative