Parameterised modules and Lambda Lifting

LambdaLifting.agda

module LambdaLifting where

open import Level using (Level)

module Identity (A : Set) where

  identity : A → A
  identity = λ x → x

data _∈_ {ℓ : Level} {A : Set ℓ} (a : A) : (B : Set ℓ) → Set where
  indeed : a ∈ A
  
check : Identity.identity ∈ ∀ A → A → A
check = indeed

open import Algebra
open import Data.Nat
open import Data.Product using ( _,_) renaming (_×_ to _∧_)
open import Data.List using (List; _∷_ ; [] ; foldr ; reverse ; map)
open import Function
open import Relation.Binary.PropositionalEquality

module Reduce {c ℓ : Level} (mon : RawMonoid c ℓ) where

  open RawMonoid mon

  aggregate : List Carrier → Carrier
  aggregate = foldr _∙_ ε

  _⊨reduce_ = aggregate

aggregate′ : {c ℓ : Level} (mon : RawMonoid c ℓ) →
             let open RawMonoid mon in List Carrier → Carrier
aggregate′ mon = let open RawMonoid mon in foldr _∙_ ε

aggregate′′ : {c ℓ : Level} (mon : RawMonoid c ℓ) →
              List (RawMonoid.Carrier mon) → RawMonoid.Carrier mon
aggregate′′ mon = foldr (RawMonoid._∙_ mon) (RawMonoid.ε mon)

open Reduce using (_⊨reduce_)

ℕ+ : RawMonoid _ _
ℕ+ = record { Carrier = ℕ ; _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0 }

ℕ* : RawMonoid _ _
ℕ* = record { Carrier = ℕ ; _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1 }

infix 6 [_⋯_]
[_⋯_] : ℕ → ℕ → List ℕ
[ k ⋯ l ] with compare k l
[ .(suc (k + l)) ⋯ k ] | greater .k l = []
[ k ⋯ .k             ] | equal .k     = k ∷ []
[ k ⋯ .(suc (k + l)) ] | less .k l    = map (k +_) $ reverse $ go (suc l)

  where
  
    go : ℕ → List ℕ
    go 0       = 0 ∷ []
    go (suc k) = suc k ∷ go k

test-aggregate : Reduce.aggregate ℕ+ [ 1 ⋯ 5 ] ≡ 15
               ∧ Reduce.aggregate ℕ* [ 1 ⋯ 5 ] ≡ 120
test-aggregate = refl , refl

test-reduce : ℕ+ ⊨reduce [ 1 ⋯ 5 ] ≡ 15
            ∧ ℕ* ⊨reduce [ 1 ⋯ 5 ] ≡ 120
test-reduce = refl , refl