diff --git a/src/Strongweak.hs b/src/Strongweak.hs index 57899aa..3ed1ce9 100644 --- a/src/Strongweak.hs +++ b/src/Strongweak.hs @@ -23,6 +23,7 @@ module Strongweak import Strongweak.Weaken import Strongweak.Strengthen +import Strongweak.Strength {- $strongweak-instance-design diff --git a/src/Strongweak/Chain.hs b/src/Strongweak/Chain.hs index 31290cb..d8e6b88 100644 --- a/src/Strongweak/Chain.hs +++ b/src/Strongweak/Chain.hs @@ -1,13 +1,12 @@ {-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints -{-# LANGUAGE AllowAmbiguousTypes #-} -- TODO +{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes module Strongweak.Chain where -import Strongweak.Weaken +import Strongweak.Weaken ( Weaken(weaken), type WeakenedN ) import Strongweak.Strengthen import GHC.TypeNats - -import Unsafe.Coerce +import Unsafe.Coerce ( unsafeCoerce ) {- | When weakening (or strengthening), chain the operation @n@ times. diff --git a/src/Strongweak/Example.hs b/src/Strongweak/Example.hs deleted file mode 100644 index cab6d71..0000000 --- a/src/Strongweak/Example.hs +++ /dev/null @@ -1,16 +0,0 @@ -module Strongweak.Example where -import Strongweak -import Strongweak.Generic -import GHC.Generics ( Generic ) -import Data.List.NonEmpty as NE -import Data.Word - -data A (s :: Strength) = A - { a1 :: SW s (NE.NonEmpty (SW s Word8)) - } deriving stock Generic -deriving instance Show (A Weak) -deriving instance Show (A Strong) - -instance Weaken (A Strong) where - type Weakened (A Strong) = A Weak - weaken = undefined -- weakenGeneric diff --git a/src/Strongweak/Strength.hs b/src/Strongweak/Strength.hs new file mode 100644 index 0000000..77dd7df --- /dev/null +++ b/src/Strongweak/Strength.hs @@ -0,0 +1,26 @@ +module Strongweak.Strength where + +import Strongweak.Weaken ( type Weakened ) +import Data.Kind ( type Type ) + +-- | Strength enumeration: is it strong, or weak? +-- +-- Primarily interesting at the type level (using DataKinds). +data Strength = Strong | Weak + +{- | Get either the strong or weak representation of a type, depending on the + type-level "switch" provided. + +This is intended to be used in data types that take a 'Strength' type. Define +your type using strong fields wrapped in @SW s@. You then get the weak +representation for free, using the same definition. + +@ +data A (s :: Strength) = A + { a1 :: SW s Word8 + , a2 :: String } +@ +-} +type family SW (s :: Strength) a :: Type where + SW Strong a = a + SW Weak a = Weakened a diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs index ea107c2..54f807e 100644 --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -20,8 +20,13 @@ module Strongweak.Strengthen , Strongweak.Weaken.Weakened ) where +import Strongweak.Weaken ( Weaken(Weakened) ) + +import Strongweak.Weaken ( Weaken(weaken) ) + +import Strongweak.Weaken ( SWCoercibly(..) ) + import Strongweak.Util.TypeNats ( natVal'' ) -import Strongweak.Weaken ( Weaken(Weakened, weaken) ) import GHC.TypeNats ( KnownNat ) import Data.Word @@ -101,6 +106,15 @@ failStrengthen t fs = Left $ StrengthenFailure t fs failStrengthen1 :: [text] -> Either (StrengthenFailure text) a failStrengthen1 t = failStrengthen t [] +-- TODO add a via type for obtaining strengthen via unsafestrengthen :) +-- should be permitted only for non-failing, zero invariant strengthens + +instance Strengthen (SWCoercibly a) where + strengthen = Right . SWCoercibly + +deriving via SWCoercibly a instance Strengthen (Identity a) +deriving via SWCoercibly a instance Strengthen (Const a b) + -- | Strengthen a type by refining it with a predicate. instance Refine p a => Strengthen (Refined p a) where strengthen = refine .> \case @@ -236,6 +250,3 @@ f .> g = g . f typeRep' :: forall a. Typeable a => TypeRep typeRep' = typeRep (Proxy @a) - -instance Strengthen (Identity a) where - strengthen = Right . Identity diff --git a/src/Strongweak/Strengthen/Unsafe.hs b/src/Strongweak/Strengthen/Unsafe.hs index 4d328a7..68747cb 100644 --- a/src/Strongweak/Strengthen/Unsafe.hs +++ b/src/Strongweak/Strengthen/Unsafe.hs @@ -7,11 +7,13 @@ import Rerefined.Refine import Data.Vector.Generic.Sized qualified as VGS -- Shazbot! import Data.Vector.Generic qualified as VG import Data.Vector.Generic.Sized.Internal qualified -import Data.Functor.Identity -import Data.Functor.Const import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) +import Strongweak.Weaken ( SWCoercibly(..) ) +import Data.Functor.Identity +import Data.Functor.Const + {- | Unsafely transform a @'Weakened' a@ to an @a@, without asserting invariants. Naturally, you must only even /consider/ using this if you have a guarantee that @@ -34,6 +36,12 @@ class Weaken a => UnsafeStrengthen a where -- | Unsafely transform a @'Weakened' a@ to its associated strong type @a@. unsafeStrengthen :: Weakened a -> a +instance UnsafeStrengthen (SWCoercibly a) where + unsafeStrengthen = SWCoercibly + +deriving via SWCoercibly a instance UnsafeStrengthen (Identity a) +deriving via SWCoercibly a instance UnsafeStrengthen (Const a b) + -- | Add a refinement to a type without checking the associated predicate. instance UnsafeStrengthen (Refined p a) where unsafeStrengthen = unsafeRefine diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs index cc6d96d..b86f3ea 100644 --- a/src/Strongweak/Weaken.hs +++ b/src/Strongweak/Weaken.hs @@ -2,16 +2,10 @@ module Strongweak.Weaken ( - -- * 'Weaken' class - Weaken(..) + Weaken(Weakened, weaken) , type WeakenedN , liftWeakF - - -- * Strength switch helper - , Strength(..) - , type SW - - , ErrZeroInvariantNewtype' + , SWCoercibly(..) ) where import Rerefined @@ -26,10 +20,6 @@ import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) import GHC.TypeNats -import GHC.TypeError -import Strongweak.Util.TypeErrors -import GHC.TypeLits ( type Symbol ) - {- | Weaken some @a@, relaxing certain invariants. See "Strongweak" for class design notes and laws. @@ -41,38 +31,32 @@ class Weaken a where -- | Weaken some @a@ to its associated weak type @'Weakened' a@. weaken :: a -> Weakened a --- | Strength enumeration: is it strong, or weak? --- --- Primarily interesting at the type level (using DataKinds). -data Strength = Strong | Weak - -- | Lift a function on a weak type to the associated strong type by weakening -- first. liftWeakF :: Weaken a => (Weakened a -> b) -> a -> b liftWeakF f = f . weaken -{- | Get either the strong or weak representation of a type, depending on the - type-level "switch" provided. - -This is intended to be used in data types that take a 'Strength' type. Define -your type using strong fields wrapped in @SW s@. You then get the weak -representation for free, using the same definition. - -@ -data A (s :: Strength) = A - { a1 :: SW s Word8 - , a2 :: String } -@ --} -type family SW (s :: Strength) a :: Type where - SW Strong a = a - SW Weak a = Weakened a - -- | The type of @a@ after weakening @n@ times. type family WeakenedN (n :: Natural) a :: Type where WeakenedN 0 a = a WeakenedN n a = Weakened (WeakenedN (n-1) a) +-- | A "via type" newtype for defining strongweak instances for zero-invariant, +-- coercible newtypes. +-- +-- Use like so: +-- +-- @ +-- deriving via 'SWCoercibly' a instance 'Weaken' ('Identity' a) +-- @ +newtype SWCoercibly a = SWCoercibly { unSWCoercibly :: a } +instance Weaken (SWCoercibly a) where + type Weakened (SWCoercibly a) = a + weaken = unSWCoercibly + +deriving via SWCoercibly a instance Weaken (Identity a) +deriving via SWCoercibly a instance Weaken (Const a b) + -- | Strip refined type refinement. instance Weaken (Refined p a) where type Weakened (Refined p a) = a @@ -144,37 +128,3 @@ instance (Weaken a, Weaken b) => Weaken (Either a b) where type Weakened (Either a b) = Either (Weakened a) (Weakened b) weaken = \case Left a -> Left $ weaken a Right b -> Right $ weaken b - ---- - -newtype ErrZeroInvariantNewtype' (typeName :: Symbol) a - = ErrZeroInvariantNewtype' a -instance Unsatisfiable (ErrZeroInvariantNewtype typeName) - => Weaken (ErrZeroInvariantNewtype' typeName a) where - type Weakened (ErrZeroInvariantNewtype' typeName a) = - TypeError (ErrZeroInvariantNewtype typeName) - weaken = unsatisfiable - ---deriving via ErrZeroInvariantNewtype' "Identity" a --- instance Weaken (Identity a) - -{- TODO 2024-10-16T04:21:22+0100 -aww this doesn't work haha. ok fine just gotta make some utils for filling out -the context and Weakened associated type family for custom erroring instances --} - -{- -instance Unsatisfiable (ErrZeroInvariantNewtype "Identity") - => Weaken (Identity a) where - type Weakened (Identity a) = a - weaken = unsatisfiable --} - --- TODO define custom errors using Unsatisfiable to point users to Coercibly --- Unsatisfiable is base-4.19 -> GHC 9.8 ---deriving via Coercibly1 Shallow Identity a instance Weaken (Identity a) ---deriving via Coercibly Shallow (Const a b) a instance Weaken (Const a b) - -instance Weaken (Identity a) where - type Weakened (Identity a) = a - weaken (Identity a) = a diff --git a/strongweak.cabal b/strongweak.cabal index a53e4f6..99f2f6b 100644 --- a/strongweak.cabal +++ b/strongweak.cabal @@ -32,8 +32,8 @@ library Strongweak Strongweak.Chain Strongweak.Coercibly - Strongweak.Example Strongweak.Generic + Strongweak.Strength Strongweak.Strengthen Strongweak.Strengthen.Generic Strongweak.Strengthen.Unsafe