{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
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) )
data IsIntersection x y z = IsIntersection
{
IsIntersection x y z -> Sub z x
proj1 :: !(Sub z x),
IsIntersection x y z -> Sub z y
proj2 :: !(Sub z y),
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
}
withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
withIntersection :: 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 =
IsIntersection x y y -> r
forall xy. IsIntersection x y xy -> r
body IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub y x
proj1 = Sub y x
forall k (a :: k) (b :: k). Coercible a b => Sub a b
sub, proj2 :: Sub y y
proj2 = Sub y y
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 = forall s. Sub s x -> Sub s y -> Sub s y
seq }
unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y z
xy IsIntersection x y z'
xy' = Sub z z' -> Sub z' z -> Coercion z z'
forall k (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsIntersection x y z' -> Sub z x -> Sub z y -> Sub z z'
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' (IsIntersection x y z -> Sub z x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xy) (IsIntersection x y z -> Sub z y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xy)) (IsIntersection x y z -> Sub z' x -> Sub z' y -> Sub z' z
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 (IsIntersection x y z' -> Sub z' x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z'
xy') (IsIntersection x y z' -> Sub z' y
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 :: Sub x y -> IsIntersection x y x
lesser Sub x y
l = IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub x x
proj1=Sub x x
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 :: IsIntersection x x x
idemp = Sub x x -> IsIntersection x x x
forall x y. Sub x y -> IsIntersection x y x
lesser Sub x x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative IsIntersection x y z
xyz = IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub z y
proj1 = IsIntersection x y z -> Sub z y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xyz, proj2 :: Sub z x
proj2 = IsIntersection x y z -> Sub z x
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 = (Sub s x -> Sub s y -> Sub s z) -> Sub s y -> Sub s x -> Sub s z
forall a b c. (a -> b -> c) -> b -> a -> c
flip (IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
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 xy'z -> IsIntersection y z yz -> IsIntersection x yz x'yz -> Coercion xy'z x'yz
associative :: IsIntersection x y xy
-> IsIntersection xy z xy'z
-> IsIntersection y z yz
-> IsIntersection x yz x'yz
-> Coercion xy'z x'yz
associative IsIntersection x y xy
xy IsIntersection xy z xy'z
xy'z IsIntersection y z yz
yz IsIntersection x yz x'yz
x'yz =
Sub xy'z x'yz -> Sub x'yz xy'z -> Coercion xy'z x'yz
forall k (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsIntersection x yz x'yz
-> Sub xy'z x -> Sub xy'z yz -> Sub xy'z x'yz
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x yz x'yz
x'yz (IsIntersection x y xy -> Sub xy x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y xy
xy Sub xy x -> Sub xy'z xy -> Sub xy'z x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection xy z xy'z -> Sub xy'z xy
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xy'z
xy'z) (IsIntersection y z yz -> Sub xy'z y -> Sub xy'z z -> Sub xy'z yz
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 (IsIntersection x y xy -> Sub xy y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y xy
xy Sub xy y -> Sub xy'z xy -> Sub xy'z y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection xy z xy'z -> Sub xy'z xy
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xy'z
xy'z) (IsIntersection xy z xy'z -> Sub xy'z z
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection xy z xy'z
xy'z)))
(IsIntersection xy z xy'z
-> Sub x'yz xy -> Sub x'yz z -> Sub x'yz xy'z
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection xy z xy'z
xy'z (IsIntersection x y xy -> Sub x'yz x -> Sub x'yz y -> Sub x'yz xy
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 (IsIntersection x yz x'yz -> Sub x'yz x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x yz x'yz
x'yz) (IsIntersection y z yz -> Sub yz y
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection y z yz
yz Sub yz y -> Sub x'yz yz -> Sub x'yz y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection x yz x'yz -> Sub x'yz yz
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x yz x'yz
x'yz)) (IsIntersection y z yz -> Sub yz z
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection y z yz
yz Sub yz z -> Sub x'yz yz -> Sub x'yz z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection x yz x'yz -> Sub x'yz yz
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x yz x'yz
x'yz))