coercible-subtypes 0.1.1.0 → 0.2.0.0

raw patch · 8 files changed

+278/−29 lines, 8 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• coercible-subtypes.cabal +6/−2
• src/Data/Type/Coercion/Related.hs +50/−0
• src/Data/Type/Coercion/Related/Internal.hs +44/−0
• src/Data/Type/Coercion/Sub.hs +25/−27
• src/Data/Type/Coercion/Sub/Internal.hs +9/−0
• src/Newtype/Intersection.hs +69/−0
• src/Newtype/Union.hs +70/−0

@@ -1,5 +1,10 @@ # Revision history for coercible-subtypes +## 0.2.0.0 -- 2021-09-13++* Add `Related`+* Add `IsIntersection` and `IsUnion` facilities+ ## 0.1.1.0 -- 2021-08-24  * Add instances `Coercible a b => (Read (Sub a b), Enum (Sub a b), Bounded (Sub a b))`

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

@@ -0,0 +1,50 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE RankNTypes            #-}+{- |+  'Related' type to witness that two types @a@ and @b@ shares the same runtime representation,+  but nothing about whether @a@ can be safely coerced to or from @b@.++  Unlike 'Coercion' or 'Sub', having a value of @Related a b@ does not allow to+  touch values of @a@ or @b@.++  This module is used alonside "Newtype.Union" and "Newtype.Intersection"+  to define union and intersection types of two 'Related' types.+-}+module Data.Type.Coercion.Related(+    Related(),+    related,+    subIsRelated, coercionIsRelated,+    symRelated, undirected, informRelation+) where++import Data.Coerce+import Data.Type.Coercion+import Data.Type.Coercion.Sub+import Data.Type.Coercion.Sub.Internal+import Data.Type.Coercion.Related.Internal++-- | @'Coercible' a b@ implies @Related a b@.+related :: Coercible a b => Related a b+related = Related Coercion++-- | @'Sub' a b@ implies @Related a b@.+subIsRelated :: Sub (Sub a b) (Related a b)+subIsRelated = sub++-- | @'Coercion' a b@ implies @'Sub' a b@, which implies @Related a b@.+coercionIsRelated :: Sub (Coercion a b) (Related a b)+coercionIsRelated = sub++-- | @Related@ is a symmetric relation.+symRelated :: Related a b -> Related b a+symRelated ab = informRelation ab related++-- | A direct consequence of 'informRelation' and 'subIsRelated'.+undirected :: Sub a b -> (Coercible a b => Related x y) -> Related x y+undirected ab = informRelation (upcastWith subIsRelated ab)++-- | Given @Related a b@, you can assume @Coercible a b@ for the purpose of proving+--   another @Related@ relation.+informRelation :: Related a b -> (Coercible a b => Related x y) -> Related x y+informRelation (Related Coercion) body = body

@@ -0,0 +1,44 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE StandaloneDeriving #-}+{- |++This module exposes internals of "Data.Type.Coercion.Related".++Using this module allows to violate the premises 'Related' type provides.+It is advisable not to import this module if there is another way,+and to limit the amount of code accesible to this module.++-}+module Data.Type.Coercion.Related.Internal where++import           Control.Category+import           Prelude                    hiding (id, (.))++import           Data.Coerce+import           Data.Type.Coercion++-- | @Related a b@ witnesses @a@ and @b@ shares the same runtime representation,+--   but nothing about whether @a@ can be safely coerced to or from @b@.+-- +-- You can make 'Related' witnesses by using combinators in this module, or the methods of+-- the @'Category' Related@ instance: 'id' and @('.')@.+newtype Related (a :: k) (b :: k) = Related { getRelated :: Coercion a b }+  deriving stock (Eq, Ord, Show)+-- It is intentional to omit the 'TestCoercion' instance, existing for @Coercion@.+-- Knowing @Related a b@ and @Related a c@ should not conclude+-- @Coercible b c@.++deriving stock instance Coercible a b => Read (Related a b)+deriving newtype instance Coercible a b => Enum (Related a b)+deriving newtype instance Coercible a b => Bounded (Related a b)++instance Category Related where+  id :: Related a a+  id = Related Coercion++  (.) :: Related b c -> Related a b -> Related a c+  Related Coercion . Related Coercion = Related Coercion

@@ -2,38 +2,35 @@ {-# LANGUAGE PolyKinds             #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes            #-}-module Data.Type.Coercion.Sub(-  {- | @Sub a b@ witnesses a zero-cost conversion @a -> b@.+{- | @'Sub' a b@ witnesses a zero-cost conversion @a -> b@. -  @Sub@ is a newtype wrapper around 'Coercion', but made opaque to hide-  the ability to 'Data.Coerce.coerce' into other direction.+=== Example -  This is convenient for newtype wrappers which give additional guarantees.+Think about the following code: -  As an example, think about the following code:+> -- | A pair @(x::a, y::a)@, but guaranteed @x <= y@+> newtype Range a = MkRange (a,a)+>+> getRange :: Range a -> (a,a)+> getRange = coerce+> mkRange :: Ord a => a -> a -> Range a+> mkRange x y = if x <= y then MkRange (x,y) else MkRange (y,x) -  > -- | A pair @(x::a, y::a)@, but guaranteed @x <= y@-  > newtype Range a = MkRange (a,a)-  >-  > getRange :: Range a -> (a,a)-  > getRange = coerce-  > mkRange :: Ord a => a -> a -> Range a-  > mkRange x y = if x <= y then MkRange (x,y) else MkRange (y,x)+If you want to provide this type from a library you maintain,+you would want to keep @Range@ abstract from outside of the module. -  If you want to provide this type from a library you maintain,-  you would want to keep @Range@ abstract from outside of the module.+A user may want to convert @[Range a]@ to @[(a,a)]@ without actually+traversing the list. This is possible if the user have access to the+internals, or you export a @Coercion (Range a) (a,a)@ value. But doing so+breaks the guarantee, because it also allows to use @Coercible@ in the other+direction, as in @coerce (10,5) :: Range Int@. -  An user may want to convert @[Range a]@ to @[(a,a)]@ without actually-  traversing the list. This is possible if the user have access to the-  internals, or you export a @Coercion (Range a) (a,a)@ value. But doing so-  breaks the guarantee, because it also allows to use @Coercible@ in the other-  direction, as in @coerce (10,5) :: Range Int@.+By exporting only @Sub (Range a) (a,a)@ value from your module,+this user can get @Sub [Range a] [(a,a)]@ using 'mapR',+without being able to make an invalid value. -  By exporting only @Sub (Range a) (a,a)@ value from your module,-  this user can get @Sub [Range a] [(a,a)]@ using 'mapR',-  without being able to make an invalid value.-  -  -}+-}+module Data.Type.Coercion.Sub(   Sub(),   sub, toSub, upcastWith, equiv, gequiv, @@ -53,10 +50,11 @@  import           Data.Type.Coercion.Sub.Internal --- | Make a witness for type-safe casting which respects direction.+-- | Make a directed witness of @'coerce' :: a -> b@. sub :: Coercible a b => Sub a b sub = Sub Coercion +-- | Make a directed witness of @'coerce' :: a -> b@, from a 'Coercion' value. toSub :: Coercion a b -> Sub a b toSub = Sub @@ -146,7 +144,7 @@        => Sub a a' -> Sub b b' -> Sub (t a' b) (t a b') dimapR (Sub Coercion) (Sub Coercion) = Sub Coercion --- | 'dimapR' specialized for '(->)'+-- | 'dimapR' specialized for functions @(->)@ arrR :: Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b') arrR = dimapR 

@@ -23,6 +23,15 @@ import           Data.Coerce import           Data.Type.Coercion +{- |+  @Sub@ is a newtype wrapper around 'Coercion', but made opaque to hide+  the ability to 'Data.Coerce.coerce' into other direction.++  This is convenient for newtype wrappers which give additional guarantees.++  You can make @Sub@ witnesses by using combinators in this module, or the methods of+  the @'Category' Sub@ instance: 'id' and @('.')@.+-} newtype Sub (a :: k) (b :: k) = Sub { getSub :: Coercion a b }   deriving stock (Eq, Ord, Show) -- It is intentional to omit the 'TestCoercion' instance, existing for @Coercion@.

@@ -0,0 +1,69 @@+{-# 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) )++-- | @IsIntersection x y z@ witnesses the fact:+--+--   * All @x, y, z@ share the same runtime representation+--   * @z@ is an intersection type of @x@ and @y@. In other words, the following three holds:+--+--       * @'Sub' z x@+--       * @Sub z y@+--       * For any type @s@ satisfying both of @(Sub s x, Sub s y)@, @Sub s z@.+data IsIntersection x y z = IsIntersection+  {+    proj1 :: !(Sub z x),+    proj2 :: !(Sub z y),+    conjunct :: forall s. Sub s x -> Sub s y -> Sub s z+  }++-- | 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+withIntersection (Related Coercion) body =+    body IsIntersection{ proj1 = sub, proj2 = id, conjunct = seq }++-- | Two intersection types @z,z'@ of the same pair of types @x,y@ may be different,+--   but they are equivalent in terms of coercibility.+unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'+unique xy xy' = equiv (conjunct xy' (proj1 xy) (proj2 xy)) (conjunct xy (proj1 xy') (proj2 xy'))++-- | When @Sub x y@, @x@ itself is an intersection type of @x, y@.+lesser :: Sub x y -> IsIntersection x y x+lesser l = IsIntersection{ proj1=id, proj2=l, conjunct= \sx !_ -> sx }+++-- | Intersection is idempotent.+--+--   Note: combining @idemp@ and 'unique', @IsIntersection x x z -> Coercible 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.+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))

@@ -0,0 +1,70 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE TypeOperators #-}+module Newtype.Union(+  module Data.Type.Coercion.Related,+  IsUnion(..),++  withUnion,+  +  unique, greater, idemp, commutative, associative+) where++import Prelude hiding (id, (.))+import Control.Category+import Data.Type.Coercion.Sub (sub, equiv)+import Data.Type.Coercion.Sub.Internal+import Data.Type.Coercion.Related+import Data.Type.Coercion.Related.Internal+import Data.Type.Coercion ( Coercion(Coercion))++-- | @IsUnion x y z@ witnesses the fact:+--+--   * All @x, y, z@ share the same runtime representation+--   * @z@ is a union type of @x@ and @y@. In other words, the following three holds:+--+--     * @'Sub' x z@+--     * @Sub y z@+--     * For any type @r@ satisfying both of @(Sub x r, Sub y r)@, @Sub z r@.+data IsUnion x y z = IsUnion+  {+    inl :: !(Sub x z), -- ^ @x@ can be safely coerced to @z@+    inr :: !(Sub y z), -- ^ @y@ can be safely coerced to @z@+    elim :: forall r. Sub x r -> Sub y r -> Sub z r+      -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.+  }++-- | 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+withUnion (Related Coercion) body =+    body IsUnion{ inl = sub, inr = id, elim = seq }++-- | Two union types @z,z'@ of the same pair of types @x,y@ may be different,+--   but they are equivalent in terms of coercibility.+unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'+unique xy xy' = equiv (elim xy (inl xy') (inr xy')) (elim xy' (inl xy) (inr xy))++-- | When @Sub x y@, @y@ itself is a union type of @x, y@.+greater :: Sub x y -> IsUnion x y y+greater l = IsUnion{ inl = l, inr = id, elim=seq }++-- | Union is idempotent.+--+--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercible 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.+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)))