From ea18c145c14b7534b9c58778879838dd5d8b5429 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Sat, 27 Oct 2012 22:20:12 +0200
Subject: [PATCH] another example

---
 Automata.hs  |  6 +++---
 Coalgebra.hs |  9 +++++----
 Natinfi.hs   | 35 +++++++++++++++++++++++++++++++++++
 Streams.hs   |  4 ++--
 4 files changed, 45 insertions(+), 9 deletions(-)
 create mode 100644 Natinfi.hs

diff --git a/Automata.hs b/Automata.hs
index e684a58..b8c2d4e 100644
--- a/Automata.hs
+++ b/Automata.hs
@@ -8,15 +8,15 @@ import Coalgebra
 type F a = (,) Bool `O` ((->) a)
 
 -- Fixpoint, ie languages
-type Language a = Mu (F a)
+type Language a = Nu (F a)
 
--- auciliry function
+-- auxiliary function
+-- recall that the first component of psi l is true if the language accepts the empty word
 is_member :: [a] -> Language a -> Bool
 is_member [] l = b where O (b, _) = psi l
 is_member (a:r) l = is_member r (trans a) where O (_, trans) = psi l
 
 
-
 -- Our alphabet
 data A = A | B
 	deriving Show
diff --git a/Coalgebra.hs b/Coalgebra.hs
index baee4da..016354f 100644
--- a/Coalgebra.hs
+++ b/Coalgebra.hs
@@ -12,15 +12,16 @@ class Functor f => Coalgebra f m | m -> f where
 
 -- Fixpoint, ie f (Mu f) = Mu f
 -- unfortunatly we need a data constructor
-data Mu f = In (f (Mu f))
+data Nu f = In (f (Nu f))
 
 -- The fixpoint is both a algebra and coalgebra,
 -- because there is an arrow id: X -> X = FX, if X is a fixpoint
-instance Functor f => Algebra f (Mu f) where
+instance Functor f => Algebra f (Nu f) where
     phi = In
  
-instance Functor f => Coalgebra f (Mu f) where
+instance Functor f => Coalgebra f (Nu f) where
     psi (In x) = x
 
-semantics :: (Functor f, Coalgebra f x) => x -> (Mu f)
+-- It feels weird that this always works...
+semantics :: (Functor f, Coalgebra f x) => x -> (Nu f)
 semantics x = phi (fmap semantics (psi x))
diff --git a/Natinfi.hs b/Natinfi.hs
new file mode 100644
index 0000000..aab8aeb
--- /dev/null
+++ b/Natinfi.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
+
+import Control.Monad.Instances
+import Coalgebra
+
+-- F X = 1 + X
+type F = Maybe
+
+-- This will give the fixpoint, ie a coalgebra, because F is a functor
+type Natinfi = Nu F
+
+-- The semantics from the following coalgebra to Natinfi is "the selection function" (I hope)
+-- In some sense this behaviour searches through all natural numbers
+instance Coalgebra F (Natinfi -> Bool) where
+	psi p
+		| p (phi Nothing) == False = Nothing
+		| otherwise = Just (\x -> p $ phi $ Just x)
+
+-- On "numbers" bigger that one, return True
+test :: Natinfi -> Bool
+test p = case q of
+		Nothing -> True
+		Just y -> False
+	where q = psi p
+
+-- Of course this will not always terminate!
+toInt :: Natinfi -> Int
+toInt s = case q of
+		Nothing -> 0
+		Just y -> 1 + toInt y
+	where q = psi s
+
+main :: IO ()
+main = do
+	putStrLn $ show $ toInt $ (semantics test :: Natinfi)
\ No newline at end of file
diff --git a/Streams.hs b/Streams.hs
index 1ff3cf2..8926716 100644
--- a/Streams.hs
+++ b/Streams.hs
@@ -7,9 +7,9 @@ import Coalgebra
 type F a = (,) a
 
 -- This will give the fixpoint, ie a coalgebra, because F is a functor
-type Stream a = Mu (F a)
+type Stream a = Nu (F a)
 
--- auxilary functions
+-- auxiliary functions
 toList :: Stream a -> [a]
 toList s = a0 : toList a' where (a0, a') = psi s