ncfavier

{-# LANGUAGE BlockArguments #-}

import Control.Monad
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Sequence qualified as Seq
import Data.PriorityQueue.FingerTree qualified as PQ

ncfavier

open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Relation.Binary.PropositionalEquality

Futamura projections

Let us represent programs from inputs I to outputs O as simple functions I → O, and assume we have a specialiser: a program that partially evaluates another program applied to the "static" part of its input.

ncfavier

open import 1Lab.Prelude
open import Data.Dec
open import Data.Nat

module Goat where

holds : ∀ {ℓ} (A : Type ℓ) ⦃ _ : Dec A ⦄ → Type
holds _ ⦃ yes _ ⦄ = ⊤
holds _ ⦃ no _ ⦄ = ⊥

ncfavier

open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Functor.Coherence
open import Cat.Instances.Product
open import Cat.Functor.Compose
open import Cat.Diagram.Monad
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

ncfavier

L ⊣ R

adjunct : (L a → b) → (a → R b)
coadjunct : (a → R b) → (L a → b)
unit : a → RL a
counit : LR b → b
Lmap : (a → b) → (L a → L b)
Rmap : (a → b) → (R a → R b)

adjunct f = unit; Rmap f

ncfavier

instance Monoid a => MonadFix ((,) a) where
  mfix :: (b -> (a, b)) -> (a, b)
  mfix f = let (a, b) = f b in (a, b)
  -- or
  mfix f = fix (f . snd)

The laws are proved in section 4.5 of Value Recursion in Monadic Computations

ncfavier

-- Moved to https://agda.monade.li/NatChurchMonoid.html

ncfavier

-- Moved to https://agda.monade.li/Applicative.html

ncfavier

-- Moved to https://agda.monade.li/MonoidalFibres.html

ncfavier

-- Moved to https://agda.monade.li/FirstGroupCohomology.html