{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |
-- Module      : OAlg.Data.Canonical
-- Description : canonical mappings
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- canonical mappings between two types.
module OAlg.Data.Canonical
  ( -- * Canonical Mappings
    Embeddable(..), Projectible(..)
  )
  where

import OAlg.Data.Boolean.Definition

--------------------------------------------------------------------------------
-- Embeddable -

-- | canonical embedding from @__a__@ in to @__b__@.
--
-- __Property__
--
-- (1) 'inj' is injective.
--
-- (2) if the two types  @__a__@ and @__b__@ are also @'Projectible' __a__ __b__@ then
--     @'prj' '.' 'inj'@ is the identical mapping.
class Embeddable a b where
  -- | canonical injetion from @a@ in to @b@.
  inj :: a -> b
  

instance (Embeddable a a', Embeddable b b') => Embeddable (a,b) (a',b') where
  inj :: (a, b) -> (a', b')
inj (a
a,b
b) = (forall a b. Embeddable a b => a -> b
inj a
a,forall a b. Embeddable a b => a -> b
inj b
b)
  
instance (Embeddable a a', Embeddable b b', Embeddable c c')
  => Embeddable (a,b,c) (a',b',c') where
  inj :: (a, b, c) -> (a', b', c')
inj (a
a,b
b,c
c) = (forall a b. Embeddable a b => a -> b
inj a
a,forall a b. Embeddable a b => a -> b
inj b
b,forall a b. Embeddable a b => a -> b
inj c
c)
  
--------------------------------------------------------------------------------
-- Projectible -

-- | canonical projection from @b@ on to @a@.
--
-- __Property__
--
-- (1) 'prj' is surjective.
--
-- (2) if the two types  @__a__@ and @__b__@ are also @'Projectible' __a__ __b__@ then
--     @'prj' '.' 'inj'@ is the identical mapping.
class Projectible a b where
  -- | canonical projection from @b@ on to @a@
  prj :: b -> a

instance (Projectible a a', Projectible b b') => Projectible (a,b) (a',b') where
  prj :: (a', b') -> (a, b)
prj (a'
a',b'
b') = (forall a b. Projectible a b => b -> a
prj a'
a',forall a b. Projectible a b => b -> a
prj b'
b')
  
instance (Projectible a a', Projectible b b', Projectible c c')
  => Projectible (a,b,c) (a',b',c') where
  prj :: (a', b', c') -> (a, b, c)
prj (a'
a',b'
b',c'
c') = (forall a b. Projectible a b => b -> a
prj a'
a',forall a b. Projectible a b => b -> a
prj b'
b',forall a b. Projectible a b => b -> a
prj c'
c')
  
instance Boolean b => Embeddable Bool b where
  inj :: Bool -> b
inj Bool
True  = forall b. Boolean b => b
true
  inj Bool
False = forall b. Boolean b => b
false