diff --git a/CHANGELOG.md b/CHANGELOG.md index 983059d..bedfdb0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,9 @@ +## 0.12.0 (unreleased) +* rename `WeakenN` to `SWChain` +* export previous `SWChain` internals `weakenN` and `strengthenN` for magical + strongweak chaining (!) + * no need to write `weaken . weaken . weaken` when `weakenN @3` will do! + ## 0.11.0 (2024-10-17) * add `WeakenN` and `SWN` for chaining weakenings * clarify instance design: even zero-invariant coercible newtypes aren't allowed diff --git a/src/Strongweak.hs b/src/Strongweak.hs index 3033de4..1f1ef61 100644 --- a/src/Strongweak.hs +++ b/src/Strongweak.hs @@ -10,10 +10,12 @@ module Strongweak -- * Classes Weaken(..) + , weakenN , Strengthen(..) + , strengthenN -- * Other definitions - , WeakenN(..) + , SWChain(..) , SWCoercibly(..) , liftWeakF @@ -27,7 +29,7 @@ module Strongweak import Strongweak.Weaken import Strongweak.Strengthen import Strongweak.Strength -import Strongweak.WeakenN +import Strongweak.Chain {- $strongweak-instance-design diff --git a/src/Strongweak/Chain.hs b/src/Strongweak/Chain.hs new file mode 100644 index 0000000..9e0102d --- /dev/null +++ b/src/Strongweak/Chain.hs @@ -0,0 +1,45 @@ +module Strongweak.Chain ( SWChain(..), strengthenN ) where + +import Strongweak.Weaken ( Weaken(..), WeakenN(weakenN), type WeakenedN ) +import Strongweak.Strengthen ( Strengthen(..), StrengthenN(strengthenN) ) +import GHC.TypeNats ( type Natural ) + +{- | When weakening (or strengthening), chain the operation @n@ times. + +You may achieve this without extra newtypes by nesting uses of +'Strongweak.Strength.SW'. However, strongweak generics can't handle this, +forcing you to write manual instances. + +'SWChain' provides this nesting behaviour in a type. In return for adding a +boring newtype layer to the strong representation, you can chain weakening and +strengthenings without having to write them manually. + +The type works as follows: + +@ +'Weakened' ('SWChain' 0 a) = a +'Weakened' ('SWChain' 1 a) = 'Weakened' a +'Weakened' ('SWChain' 2 a) = 'Weakened' ('Weakened' a) +'Weakened' ('SWChain' n a) = 'WeakenedN' n a +@ + +And so on. (This type is only much use from @n = 2@ onwards.) + +You may also use this as a "via" type: + +@ +newtype A (s :: 'Strength') = A { a1 :: 'SW' s (Identity ('SW' s Word8)) } +deriving via 'SWChain' 2 (Identity Word8) instance 'Weaken' (A 'Strong') +deriving via 'SWChain' 2 (Identity Word8) instance 'Strengthen' (A 'Strong') +@ +-} +newtype SWChain (n :: Natural) a = SWChain { unSWChain :: a } + deriving stock Show + deriving (Ord, Eq) via a + +instance WeakenN n a => Weaken (SWChain n a) where + type Weakened (SWChain n a) = WeakenedN n a + weaken = weakenN @n . unSWChain + +instance StrengthenN n a => Strengthen (SWChain n a) where + strengthen = fmap SWChain . strengthenN @n diff --git a/src/Strongweak/Strength.hs b/src/Strongweak/Strength.hs index 940d9ac..e7e03b6 100644 --- a/src/Strongweak/Strength.hs +++ b/src/Strongweak/Strength.hs @@ -5,7 +5,7 @@ module Strongweak.Strength where import Strongweak.Weaken ( type Weakened ) import Data.Kind ( type Type ) -import Strongweak.WeakenN +import Strongweak.Chain import GHC.TypeNats ( type Natural ) -- | Strength enumeration: it's either strong, or weak. @@ -30,5 +30,5 @@ type family SW (s :: Strength) a :: Type where SW Strong a = a SW Weak a = Weakened a --- | Shortcut for a 'SW'-wrapped 'WeakenN'. -type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a) +-- | Shortcut for a 'SW'-wrapped 'SWChain'. +type SWN (s :: Strength) (n :: Natural) a = SW s (SWChain n a) diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs index 54f807e..fff49ff 100644 --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -1,11 +1,14 @@ {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE AllowAmbiguousTypes #-} -- StrengthenN, and typeRep' +-- StrengthenN type families in constraints +{-# LANGUAGE UndecidableInstances #-} module Strongweak.Strengthen ( -- * 'Strengthen' class Strengthen(..) , restrengthen + , StrengthenN(strengthenN) -- ** Helpers , strengthenBounded @@ -46,6 +49,11 @@ import Data.Bits ( FiniteBits ) import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) ) +-- for strengthenN +import GHC.TypeNats ( type Natural, type (-) ) +import Strongweak.Weaken ( type WeakenedN, WeakenN ) +import Unsafe.Coerce ( unsafeCoerce ) + {- | Attempt to strengthen some @'Weakened' a@, asserting certain invariants. We take 'Weaken' as a superclass in order to maintain strong/weak type pair @@ -250,3 +258,22 @@ f .> g = g . f typeRep' :: forall a. Typeable a => TypeRep typeRep' = typeRep (Proxy @a) + +class WeakenN n a => StrengthenN (n :: Natural) a where + strengthenN :: WeakenedN n a -> Either StrengthenFailure' a + +instance {-# OVERLAPPING #-} StrengthenN 0 a where + strengthenN = Right + +instance (Strengthen a, StrengthenN (n-1) (Weakened a)) + => StrengthenN n a where + strengthenN a = + case strengthenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of + Left e -> Left e + Right sa -> strengthen sa + +-- | Inductive 'WeakenedN'case. +-- +-- @n@ must not be 0. +weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a) +weakenedNLR1 = unsafeCoerce diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs index b86f3ea..738493a 100644 --- a/src/Strongweak/Weaken.hs +++ b/src/Strongweak/Weaken.hs @@ -1,9 +1,11 @@ {-# LANGUAGE UndecidableInstances #-} -- for WeakenedN +{-# LANGUAGE AllowAmbiguousTypes #-} -- for weakenN module Strongweak.Weaken ( Weaken(Weakened, weaken) , type WeakenedN + , WeakenN(weakenN) , liftWeakF , SWCoercibly(..) ) where @@ -20,6 +22,8 @@ import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) import GHC.TypeNats +import Unsafe.Coerce ( unsafeCoerce ) + {- | Weaken some @a@, relaxing certain invariants. See "Strongweak" for class design notes and laws. @@ -128,3 +132,23 @@ 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 + +class WeakenN (n :: Natural) a where + weakenN :: a -> WeakenedN n a + +-- | Zero case: return the value as-is. +instance {-# OVERLAPPING #-} WeakenN 0 a where + weakenN = id + +-- | Inductive case. @n /= 0@, else this explodes. +instance (Weaken a, WeakenN (n-1) (Weakened a)) + => WeakenN n a where + weakenN a = + case weakenN @(n-1) @(Weakened a) (weaken a) of + x -> weakenedNRL1 @n @a x + +-- | Inverted inductive 'WeakenedN'case. +-- +-- @n@ must not be 0. +weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a +weakenedNRL1 = unsafeCoerce diff --git a/src/Strongweak/WeakenN.hs b/src/Strongweak/WeakenN.hs deleted file mode 100644 index 4478418..0000000 --- a/src/Strongweak/WeakenN.hs +++ /dev/null @@ -1,38 +0,0 @@ -module Strongweak.WeakenN ( WeakenN(..) ) where - -import Strongweak.WeakenN.Internal -import Strongweak.Weaken ( Weaken(..), type WeakenedN ) -import Strongweak.Strengthen ( Strengthen(..) ) -import GHC.TypeNats ( type Natural ) - -{- | When weakening (or strengthening), chain the operation @n@ times. - -You may achieve this without extra newtypes by nesting uses of -'Strongweak.Weaken.SW'. However, strongweak generics can't handle this, forcing -you to write manual instances. - -'WeakenN' provides this nesting behaviour in a type. In return for adding a -boring newtype layer to the strong representation, you can chain weakening and -strengthenings without having to write them manually. - -The type works as follows: - -@ -Weakened (WeakenN 0 a) = a -Weakened (WeakenN 1 a) = Weakened a -Weakened (WeakenN 2 a) = Weakened (Weakened a) -Weakened (WeakenN n a) = WeakenedN n a -@ - -And so on. (This type is only much use from @n = 2@ onwards.) --} -newtype WeakenN (n :: Natural) a = WeakenN { unWeakenN :: a } - deriving stock Show - deriving (Ord, Eq) via a - -instance WeakenWeakenN n a => Weaken (WeakenN n a) where - type Weakened (WeakenN n a) = WeakenedN n a - weaken = weakenWeakenN @n @a . unWeakenN - -instance StrengthenWeakenN n a => Strengthen (WeakenN n a) where - strengthen = fmap WeakenN . strengthenWeakenN @n @a diff --git a/src/Strongweak/WeakenN/Internal.hs b/src/Strongweak/WeakenN/Internal.hs deleted file mode 100644 index 045f519..0000000 --- a/src/Strongweak/WeakenN/Internal.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints -{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes - -{- | 'Strongweak.WeakenN.WeakenN' internals. - -Just in case. You shouldn't need these, but they might be fun to look at. - -__Internal module. Exports may change without warning. Try not to use.__ --} - -module Strongweak.WeakenN.Internal where - -import Strongweak.Weaken ( Weaken(weaken), type WeakenedN ) -import Strongweak.Strengthen -import GHC.TypeNats ( type Natural, type (-) ) -import Unsafe.Coerce ( unsafeCoerce ) - -class WeakenWeakenN (n :: Natural) a where - weakenWeakenN :: a -> WeakenedN n a - --- | Zero case: return the value as-is. -instance {-# OVERLAPPING #-} WeakenWeakenN 0 a where - weakenWeakenN = id - --- | Inductive case. @n /= 0@, else this explodes. -instance (Weaken a, WeakenWeakenN (n-1) (Weakened a)) - => WeakenWeakenN n a where - weakenWeakenN a = - case weakenWeakenN @(n-1) @(Weakened a) (weaken a) of - x -> weakenedNRL1 @n @a x - --- | Inverted inductive 'WeakenedN'case. --- --- @n@ must not be 0. -weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a -weakenedNRL1 = unsafeCoerce - -class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where - strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a - -instance {-# OVERLAPPING #-} StrengthenWeakenN 0 a where - strengthenWeakenN = Right - -instance (Strengthen a, StrengthenWeakenN (n-1) (Weakened a)) - => StrengthenWeakenN n a where - strengthenWeakenN a = - case strengthenWeakenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of - Left e -> Left e - Right sa -> strengthen sa - --- | Inductive 'WeakenedN'case. --- --- @n@ must not be 0. -weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a) -weakenedNLR1 = unsafeCoerce diff --git a/strongweak.cabal b/strongweak.cabal index 9543d30..a057a7d 100644 --- a/strongweak.cabal +++ b/strongweak.cabal @@ -30,6 +30,7 @@ source-repository head library exposed-modules: Strongweak + Strongweak.Chain Strongweak.Generic Strongweak.Strength Strongweak.Strengthen @@ -38,8 +39,6 @@ library Strongweak.Util.TypeNats Strongweak.Weaken Strongweak.Weaken.Generic - Strongweak.WeakenN - Strongweak.WeakenN.Internal other-modules: Paths_strongweak hs-source-dirs: