Joshua Moerman
12 years ago
commit
b26e5d4b5b
2 changed files with 57 additions and 0 deletions
@ -0,0 +1,23 @@ |
|||||
|
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} |
||||
|
module Coalgebra where |
||||
|
|
||||
|
import Control.Monad |
||||
|
|
||||
|
-- Definitions for (co)algebras |
||||
|
class Functor f => Algebra f m where |
||||
|
phi :: f m -> m |
||||
|
|
||||
|
class Functor f => Coalgebra f m where |
||||
|
psi :: m -> f m |
||||
|
|
||||
|
-- Fixpoint, ie f (Mu f) = Mu f |
||||
|
-- unfortunatly we need a data constructor |
||||
|
data Mu f = In (f (Mu 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 |
||||
|
phi = In |
||||
|
|
||||
|
instance Functor f => Coalgebra f (Mu f) where |
||||
|
psi (In x) = x |
@ -0,0 +1,34 @@ |
|||||
|
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} |
||||
|
|
||||
|
import Control.Monad.Instances |
||||
|
import Coalgebra |
||||
|
|
||||
|
-- F X = A x X, for a fixed A, The prelude already provides the functor instance :) |
||||
|
type F a = (,) a |
||||
|
|
||||
|
-- This will give the fixpoint, ie a coalgebra. |
||||
|
type Stream a = Mu (F a) |
||||
|
|
||||
|
(+:+) :: a -> Stream a -> Stream a |
||||
|
(+:+) a s = In (a, s) |
||||
|
|
||||
|
-- For every other (F a)-coalgebra x, there is a arrow x -> Stream a |
||||
|
-- and it is unique, so `Stream a` is the final (F a)-coalgebra! |
||||
|
sem :: (Coalgebra (F a) x) => x -> Stream a |
||||
|
sem x = x0 +:+ sem x' where (x0, x') = psi x |
||||
|
|
||||
|
-- auxilary functions |
||||
|
toList :: Stream a -> [a] |
||||
|
toList s = a0 : toList a' where (a0, a') = psi s |
||||
|
|
||||
|
|
||||
|
-- example, with a very simple (F Int)-coalgebra, 1 -> 2, 2 -> 3, 3 -> 2 |
||||
|
data X = One | Two | Three |
||||
|
instance Coalgebra (F Int) X where |
||||
|
psi One = (1, Two) |
||||
|
psi Two = (2, Three) |
||||
|
psi Three = (3, Two) |
||||
|
|
||||
|
main :: IO () |
||||
|
main = do |
||||
|
putStrLn $ show $ take 20 $ toList $ (sem One :: Stream Int) |
Reference in new issue