coercible-subtypes 0.2.0.0 → 0.3.0.0

raw patch · 4 files changed

+59/−19 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• coercible-subtypes.cabal +2/−2
• src/Newtype/Intersection.hs +24/−8
• src/Newtype/Union.hs +24/−9

@@ -1,5 +1,14 @@ # Revision history for coercible-subtypes +## 0.3.0.0 -- 2023-01-01++* Breaking changes+  +  * Change the `Newtype.Intersection.associative` and `Newtype.Union.associative` to new,+    more succinct type.++* Instance added to `IsIntersection` and `IsUnion`+ ## 0.2.0.0 -- 2021-09-13  * Add `Related`

@@ -1,6 +1,6 @@ cabal-version:       2.2 name:                coercible-subtypes-version:             0.2.0.0+version:             0.3.0.0 stability:           experimental synopsis:            Coercible but only in one direction description: Newtype wrapper 'Data.Type.Coercion.Sub.Sub'@@ -32,7 +32,7 @@                        Data.Type.Coercion.Related.Internal,                        Newtype.Union,                        Newtype.Intersection-  build-depends:       base >=4.12 && <4.17,+  build-depends:       base >=4.12 && <4.18,                        profunctors   hs-source-dirs:      src   default-language:    Haskell2010

@@ -2,7 +2,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE TypeOperators #-} module Newtype.Intersection(   module Data.Type.Coercion.Related,   IsIntersection(..),@@ -17,7 +16,7 @@ import Data.Type.Coercion.Sub.Internal import Data.Type.Coercion.Related import Data.Type.Coercion.Related.Internal-import Data.Type.Coercion ( Coercion(Coercion) )+import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..) )  -- | @IsIntersection x y z@ witnesses the fact: --@@ -34,6 +33,14 @@     conjunct :: forall s. Sub s x -> Sub s y -> Sub s z   } +instance Eq (IsIntersection x y z) where+  _ == _ = True+instance Ord (IsIntersection x y z) where+  compare _ _ = EQ++instance TestCoercion (IsIntersection x y) where+  testCoercion u1 u2 = Just (unique u1 u2)+ -- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified) --   type @xy@ where @xy@ is an intersection type of @x, y@. withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r@@ -52,18 +59,27 @@  -- | Intersection is idempotent. -----   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.+--   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercion x z@ holds. idemp :: IsIntersection x x x idemp = lesser id  -- | Intersection is commutative. -----   Note: combining @commutative@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.+--   Note: combining @commutative@ and 'unique', @IsIntersection x y xy -> IsIntersection y x yx -> Coercion xy yx@ holds. commutative :: IsIntersection x y z -> IsIntersection y x z commutative xyz = IsIntersection{ proj1 = proj2 xyz, proj2 = proj1 xyz, conjunct = flip (conjunct xyz)}  -- | Intersection is associative.-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 xy xy'z yz x'yz =-    equiv (conjunct x'yz (proj1 xy . proj1 xy'z) (conjunct yz (proj2 xy . proj1 xy'z) (proj2 xy'z)))-          (conjunct xy'z (conjunct xy (proj1 x'yz) (proj1 yz . proj2 x'yz)) (proj2 yz . proj2 x'yz))+--+--   Note: combining @associative@ and 'unique', the following holds.+--   +--   >    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 xyz -> IsIntersection y z yz -> IsIntersection x yz xyz+associative xy xy'z yz =+    IsIntersection {+       proj1 = proj1 xy . proj1 xy'z+     , proj2 = conjunct yz (proj2 xy . proj1 xy'z) (proj2 xy'z)+     , conjunct = \s_x s_yz -> conjunct xy'z (conjunct xy s_x (proj1 yz . s_yz)) (proj2 yz . s_yz)+    }

@@ -1,8 +1,6 @@-{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE TypeOperators #-} module Newtype.Union(   module Data.Type.Coercion.Related,   IsUnion(..),@@ -18,7 +16,7 @@ import Data.Type.Coercion.Sub.Internal import Data.Type.Coercion.Related import Data.Type.Coercion.Related.Internal-import Data.Type.Coercion ( Coercion(Coercion))+import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..))  -- | @IsUnion x y z@ witnesses the fact: --@@ -36,6 +34,14 @@       -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.   } +instance Eq (IsUnion x y z) where+  _ == _ = True+instance Ord (IsUnion x y z) where+  compare _ _ = EQ++instance TestCoercion (IsUnion x y) where+  testCoercion u1 u2 = Just (unique u1 u2)+ -- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified) --   type @xy@ where @xy@ is a union type of @x, y@. withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r@@ -53,18 +59,27 @@  -- | Union is idempotent. -----   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercible x z@ holds.+--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercion x z@ holds. idemp :: IsUnion x x x idemp = greater id  -- | Union is commutative. -----   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercible xy yx@ holds.+--   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercion xy yx@ holds. commutative :: IsUnion x y z -> IsUnion y x z commutative xyz = IsUnion{ inl = inr xyz, inr = inl xyz, elim = flip (elim xyz) }  -- | Union is associative.-associative :: IsUnion x y xy -> IsUnion xy z xy'z -> IsUnion y z yz -> IsUnion x yz x'yz -> Coercion xy'z x'yz-associative xy xy'z yz x'yz =-    equiv (elim xy'z (elim xy (inl x'yz) (inr x'yz . inl yz)) (inr x'yz . inr yz))-          (elim x'yz (inl xy'z . inl xy) (elim yz (inl xy'z . inr xy) (inr xy'z)))+--+--   Note: combining @associative@ and 'unique', the following holds.+--   +--   >    IsUnion x y xy -> IsUnion xy z xy'z+--   > -> IsUnion y z yz -> IsUnion x yz x'yz+--   > -> Coercion xy'z x'yz +associative :: IsUnion x y xy -> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz+associative xy xy'z yz =+    IsUnion {+       inl = inl xy'z . inl xy +     , inr = elim yz (inl xy'z . inr xy) (inr xy'z)+     , elim = \x_r yz_r -> elim xy'z (elim xy x_r (yz_r . inl yz)) (yz_r . inr yz)+    }