{-# LANGUAGE GADTs #-}
-------------------------------------------------------------------------------------------
-- |
-- Module	: Control.Category.Discrete
  Copyright 	 : 2008  
-- License	: BSD
--
  Maintainer 	 :   <  >
-- Stability	: experimental
-- Portability	: portable
--
-------------------------------------------------------------------------------------------
module Control.Category.Discrete
	( Discrete(Refl)
	, mapDiscrete
	, cast
	, invDiscrete
	) where

import Prelude hiding (id,(.))
import Control.Category
import Unsafe.Coerce (unsafeCoerce)
  import Control . Functor . Categorical

data Discrete a b where 
	Refl :: Discrete a a

instance Category Discrete where
	id = Refl
	Refl . Refl = Refl

  instance CFunctor f Discrete Discrete where cmap = mapDiscrete

mapDiscrete :: Discrete a b -> Discrete (f a) (f b)
mapDiscrete Refl = Refl

cast :: Discrete a b -> a -> b
cast Refl = unsafeCoerce

invDiscrete :: Discrete a b -> Discrete b a
invDiscrete Refl = Refl

# LANGUAGE GADTs #
-----------------------------------------------------------------------------------------
 |
 Module	: Control.Category.Discrete
 License	: BSD

 Stability	: experimental
 Portability	: portable

-----------------------------------------------------------------------------------------
  Copyright 	 : 2008  
  Maintainer 	 :   <  >
module Control.Category.Discrete
	( Discrete(Refl)
	, mapDiscrete
	, cast
	, invDiscrete
	) where

import Prelude hiding (id,(.))
import Control.Category
import Unsafe.Coerce (unsafeCoerce)
  import Control . Functor . Categorical

data Discrete a b where 
	Refl :: Discrete a a

instance Category Discrete where
	id = Refl
	Refl . Refl = Refl

  instance CFunctor f Discrete Discrete where cmap = mapDiscrete

mapDiscrete :: Discrete a b -> Discrete (f a) (f b)
mapDiscrete Refl = Refl

cast :: Discrete a b -> a -> b
cast Refl = unsafeCoerce

invDiscrete :: Discrete a b -> Discrete b a
invDiscrete Refl = Refl
