another example

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

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))

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)

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