{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
module Newtype.Intersection(
module Data.Type.Coercion.Related,
IsIntersection(..),
withIntersection,
unique, lesser, idemp, commutative, associative
) where
import Prelude hiding (id, (.))
import Control.Category
import Data.Type.Coercion.Sub (equiv, sub)
import Data.Type.Coercion.Sub.Internal
import Data.Type.Coercion.Related
import Data.Type.Coercion.Related.Internal
import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..) )
data IsIntersection x y z = IsIntersection
{
forall x y z. IsIntersection x y z -> Sub z x
proj1 :: !(Sub z x),
forall x y z. IsIntersection x y z -> Sub z y
proj2 :: !(Sub z y),
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct :: forall s. Sub s x -> Sub s y -> Sub s z
}
instance Eq (IsIntersection x y z) where
IsIntersection x y z
_ == :: IsIntersection x y z -> IsIntersection x y z -> Bool
== IsIntersection x y z
_ = Bool
True
instance Ord (IsIntersection x y z) where
compare :: IsIntersection x y z -> IsIntersection x y z -> Ordering
compare IsIntersection x y z
_ IsIntersection x y z
_ = Ordering
EQ
instance TestCoercion (IsIntersection x y) where
testCoercion :: forall a b.
IsIntersection x y a
-> IsIntersection x y b -> Maybe (Coercion a b)
testCoercion IsIntersection x y a
u1 IsIntersection x y b
u2 = forall a. a -> Maybe a
Just (forall x y z z'.
IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y a
u1 IsIntersection x y b
u2)
withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
withIntersection :: forall x y r.
Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
withIntersection (Related Coercion x y
Coercion) forall xy. IsIntersection x y xy -> r
body =
forall xy. IsIntersection x y xy -> r
body IsIntersection{ proj1 :: Sub y x
proj1 = forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub, proj2 :: Sub y y
proj2 = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, conjunct :: forall s. Sub s x -> Sub s y -> Sub s y
conjunct = seq :: forall a b. a -> b -> b
seq }
unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique :: forall x y z z'.
IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y z
xy IsIntersection x y z'
xy' = forall {k} (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z'
xy' (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xy) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xy)) (forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z
xy (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z'
xy') (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z'
xy'))
lesser :: Sub x y -> IsIntersection x y x
lesser :: forall x y. Sub x y -> IsIntersection x y x
lesser Sub x y
l = IsIntersection{ proj1 :: Sub x x
proj1=forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, proj2 :: Sub x y
proj2=Sub x y
l, conjunct :: forall s. Sub s x -> Sub s y -> Sub s x
conjunct= \Sub s x
sx !Sub s y
_ -> Sub s x
sx }
idemp :: IsIntersection x x x
idemp :: forall x. IsIntersection x x x
idemp = forall x y. Sub x y -> IsIntersection x y x
lesser forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative :: forall x y z. IsIntersection x y z -> IsIntersection y x z
commutative IsIntersection x y z
xyz = IsIntersection{ proj1 :: Sub z y
proj1 = forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xyz, proj2 :: Sub z x
proj2 = forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xyz, conjunct :: forall s. Sub s y -> Sub s x -> Sub s z
conjunct = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z
xyz)}
associative :: IsIntersection x y xy -> IsIntersection xy z xyz -> IsIntersection y z yz -> IsIntersection x yz xyz
associative :: forall x y xy z xyz yz.
IsIntersection x y xy
-> IsIntersection xy z xyz
-> IsIntersection y z yz
-> IsIntersection x yz xyz
associative IsIntersection x y xy
xy IsIntersection xy z xyz
xy'z IsIntersection y z yz
yz =
IsIntersection {
proj1 :: Sub xyz x
proj1 = forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y xy
xy forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xyz
xy'z
, proj2 :: Sub xyz yz
proj2 = forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection y z yz
yz (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y xy
xy forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xyz
xy'z) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection xy z xyz
xy'z)
, conjunct :: forall s. Sub s x -> Sub s yz -> Sub s xyz
conjunct = \Sub s x
s_x Sub s yz
s_yz -> forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection xy z xyz
xy'z (forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y xy
xy Sub s x
s_x (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection y z yz
yz forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Sub s yz
s_yz)) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection y z yz
yz forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Sub s yz
s_yz)
}