← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/Container/FreeMonad.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Container/FreeMonad.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- The free monad construction on containers
 
5
------------------------------------------------------------------------
 
6
 
 
7
module Data.Container.FreeMonad where
 
8
 
 
9
open import Level
 
10
open import Function using (_∘_)
 
11
open import Data.Empty using (⊥-elim)
 
12
open import Data.Sum using (inj₁; inj₂)
 
13
open import Data.Product
 
14
open import Data.Container
 
15
open import Data.Container.Combinator using (const; _⊎_)
 
16
open import Data.W
 
17
open import Category.Monad
 
18
 
 
19
infixl 1 _⋆C_
 
20
infix  1 _⋆_
 
21
 
 
22
------------------------------------------------------------------------
 
23
 
 
24
-- The free monad construction over a container and a set is, in
 
25
-- universal algebra terminology, also known as the term algebra over a
 
26
-- signature (a container) and a set (of variable symbols). The return
 
27
-- of the free monad corresponds to variables and the bind operator
 
28
-- corresponds to (parallel) substitution.
 
29
 
 
30
-- A useful intuition is to think of containers describing single
 
31
-- operations and the free monad construction over a container and a set
 
32
-- describing a tree of operations as nodes and elements of the set as
 
33
-- leafs. If one starts at the root, then any path will pass finitely
 
34
-- many nodes (operations described by the container) and eventually end
 
35
-- up in a leaf (element of the set) -- hence the Kleene star notation
 
36
-- (the type can be read as a regular expression).
 
37
 
 
38
_⋆C_ : ∀ {c} → Container c → Set c → Container c
 
39
C ⋆C X = const X ⊎ C
 
40
 
 
41
_⋆_ : ∀ {c} → Container c → Set c → Set c
 
42
C ⋆ X = μ (C ⋆C X)
 
43
 
 
44
do : ∀ {c} {C : Container c} {X} → ⟦ C ⟧ (C ⋆ X) → C ⋆ X
 
45
do (s , k) = sup (inj₂ s) k
 
46
 
 
47
rawMonad : ∀ {c} {C : Container c} → RawMonad (_⋆_ C)
 
48
rawMonad = record { return = return; _>>=_ = _>>=_ }
 
49
  where
 
50
  return : ∀ {c} {C : Container c} {X} → X → C ⋆ X
 
51
  return x = sup (inj₁ x) (⊥-elim ∘ lower)
 
52
 
 
53
  _>>=_ : ∀ {c} {C : Container c} {X Y} → C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
 
54
  sup (inj₁ x) _ >>= k = k x
 
55
  sup (inj₂ s) f >>= k = do (s , λ p → f p >>= k)