diff --git a/src/Strongweak/Strength.hs b/src/Strongweak/Strength.hs index 77dd7df..940d9ac 100644 --- a/src/Strongweak/Strength.hs +++ b/src/Strongweak/Strength.hs @@ -1,9 +1,14 @@ +-- | Definitions using a type-level strength switch. + module Strongweak.Strength where import Strongweak.Weaken ( type Weakened ) import Data.Kind ( type Type ) --- | Strength enumeration: is it strong, or weak? +import Strongweak.WeakenN +import GHC.TypeNats ( type Natural ) + +-- | Strength enumeration: it's either strong, or weak. -- -- Primarily interesting at the type level (using DataKinds). data Strength = Strong | Weak @@ -24,3 +29,6 @@ data A (s :: Strength) = A 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) diff --git a/src/Strongweak/WeakenN.hs b/src/Strongweak/WeakenN.hs index 7b97c02..da0f281 100644 --- a/src/Strongweak/WeakenN.hs +++ b/src/Strongweak/WeakenN.hs @@ -1,17 +1,9 @@ -{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints -{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes +module Strongweak.WeakenN ( WeakenN(..) ) where -module Strongweak.WeakenN - ( WeakenN(..) - , type SWN - ) where - -import Strongweak.Weaken ( Weaken(weaken), type WeakenedN ) -import Strongweak.Strengthen -import GHC.TypeNats ( type Natural, type (-) ) -import Unsafe.Coerce ( unsafeCoerce ) - -import Strongweak.Strength ( type Strength, type SW ) +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. @@ -37,53 +29,9 @@ And so on. (This type is only much use from @n = 2@ onwards.) newtype WeakenN (n :: Natural) a = WeakenN { unWeakenN :: a } deriving stock Show --- | Shortcut for a 'SW'-wrapped 'WeakenN'. -type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a) - instance WeakenWeakenN n a => Weaken (WeakenN n a) where type Weakened (WeakenN n a) = WeakenedN n a weaken = weakenWeakenN @n @a . unWeakenN -class WeakenWeakenN (n :: Natural) a where - weakenWeakenN :: a -> WeakenedN n a - --- | Zero case: return the value as-is. --- --- TODO The overlapping rules always confuse me. @OVERLAPPING@ is right, right? -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 - --- | Inductive 'WeakenedN'case. --- --- @n@ must not be 0. -weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a) -weakenedNLR1 = unsafeCoerce - instance StrengthenWeakenN n a => Strengthen (WeakenN n a) where strengthen = fmap WeakenN . strengthenWeakenN @n @a - -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 diff --git a/src/Strongweak/WeakenN/Internal.hs b/src/Strongweak/WeakenN/Internal.hs new file mode 100644 index 0000000..045f519 --- /dev/null +++ b/src/Strongweak/WeakenN/Internal.hs @@ -0,0 +1,55 @@ +{-# 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 69c7d6d..dc6d7fe 100644 --- a/strongweak.cabal +++ b/strongweak.cabal @@ -39,6 +39,7 @@ library Strongweak.Weaken Strongweak.Weaken.Generic Strongweak.WeakenN + Strongweak.WeakenN.Internal other-modules: Paths_strongweak hs-source-dirs: