{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
module Data.Embedding where
import qualified Prelude as Hask hiding(foldl)
import qualified Control.Applicative as Hask
import qualified Control.Monad as Hask
import qualified Data.Foldable as Hask
import Control.Category.Constrained.Prelude hiding ((^))
import Control.Arrow.Constrained
data Isomorphism c a b = Isomorphism { forwardIso :: c a b
, backwardIso :: c b a }
infixr 0 $->$, $<-$
($->$) :: (Function c, Object c a, Object c b) => Isomorphism c a b -> a -> b
Isomorphism f _ $->$ x = f $ x
($<-$) :: (Function c, Object c b, Object c a) => Isomorphism c a b -> b -> a
Isomorphism _ p $<-$ y = p $ y
fromInversePair :: c a b -> c b a -> Isomorphism c a b
fromInversePair = Isomorphism
perfectInvert :: Isomorphism c a b -> Isomorphism c b a
perfectInvert (Isomorphism f b) = Isomorphism b f
instance (Category c) => Category (Isomorphism c) where
type Object (Isomorphism c) a = Object c a
id = Isomorphism id id
Isomorphism e p . Isomorphism f q = Isomorphism (e.f) (q.p)
instance (Cartesian c) => Cartesian (Isomorphism c) where
type UnitObject (Isomorphism c) = UnitObject c
type PairObjects (Isomorphism c) a b = PairObjects c a b
swap = Isomorphism swap swap
attachUnit = Isomorphism attachUnit detachUnit
detachUnit = Isomorphism detachUnit attachUnit
regroup = Isomorphism regroup regroup'
regroup' = Isomorphism regroup' regroup
instance (CoCartesian c) => CoCartesian (Isomorphism c) where
type ZeroObject (Isomorphism c) = ZeroObject c
type SumObjects (Isomorphism c) a b = SumObjects c a b
coSwap = Isomorphism coSwap coSwap
attachZero = Isomorphism attachZero detachZero
detachZero = Isomorphism detachZero attachZero
coRegroup = Isomorphism coRegroup coRegroup'
coRegroup' = Isomorphism coRegroup' coRegroup
maybeAsSum = Isomorphism maybeAsSum maybeFromSum
maybeFromSum = Isomorphism maybeFromSum maybeAsSum
boolAsSum = Isomorphism boolAsSum boolFromSum
boolFromSum = Isomorphism boolFromSum boolAsSum
instance (Morphism c) => Morphism (Isomorphism c) where
Isomorphism e p *** Isomorphism f q = Isomorphism (e***f) (p***q)
instance (MorphChoice c) => MorphChoice (Isomorphism c) where
Isomorphism e p +++ Isomorphism f q = Isomorphism (e+++f) (p+++q)
instance (Category c) => EnhancedCat c (Isomorphism c) where
arr = forwardIso
instance (Category c) => EnhancedCat (Embedding c) (Isomorphism c) where
arr (Isomorphism f b) = Embedding f b
data Embedding c a b = Embedding { embedding :: c a b
, projection :: c b a
}
fromEmbedProject :: c a b
-> c b a
-> Embedding c a b
fromEmbedProject = Embedding
infixr 0 $->, >-$
($->) :: (Function c, Object c a, Object c b) => Embedding c a b -> a -> b
Embedding f _ $-> x = f $ x
(>-$) :: (Function c, Object c b, Object c a) => Embedding c a b -> b -> a
Embedding _ p >-$ y = p $ y
instance (Category c) => Category (Embedding c) where
type Object (Embedding c) a = Object c a
id = Embedding id id
Embedding e p . Embedding f q = Embedding (e.f) (q.p)
instance (Cartesian c) => Cartesian (Embedding c) where
type UnitObject (Embedding c) = UnitObject c
type PairObjects (Embedding c) a b = PairObjects c a b
swap = Embedding swap swap
attachUnit = Embedding attachUnit detachUnit
detachUnit = Embedding detachUnit attachUnit
regroup = Embedding regroup regroup'
regroup' = Embedding regroup' regroup
instance (CoCartesian c) => CoCartesian (Embedding c) where
type ZeroObject (Embedding c) = ZeroObject c
type SumObjects (Embedding c) a b = SumObjects c a b
coSwap = Embedding coSwap coSwap
attachZero = Embedding attachZero detachZero
detachZero = Embedding detachZero attachZero
coRegroup = Embedding coRegroup coRegroup'
coRegroup' = Embedding coRegroup' coRegroup
maybeAsSum = Embedding maybeAsSum maybeFromSum
maybeFromSum = Embedding maybeFromSum maybeAsSum
boolAsSum = Embedding boolAsSum boolFromSum
boolFromSum = Embedding boolFromSum boolAsSum
instance (Morphism c) => Morphism (Embedding c) where
Embedding e p *** Embedding f q = Embedding (e***f) (p***q)
instance (MorphChoice c) => MorphChoice (Embedding c) where
Embedding e p +++ Embedding f q = Embedding (e+++f) (p+++q)
instance (Category c) => EnhancedCat c (Embedding c) where
arr = embedding