Skip to content

Commit

Permalink
clarify instance design; add more decomposers
Browse files Browse the repository at this point in the history
  • Loading branch information
raehik committed Jun 8, 2022
1 parent cdd6341 commit c03b2ff
Show file tree
Hide file tree
Showing 4 changed files with 182 additions and 35 deletions.
30 changes: 29 additions & 1 deletion src/Strongweak.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,35 @@
module Strongweak
( module Strongweak.Weaken
(
-- * Instance design
-- $strongweak-instance-design

-- * Re-exports
module Strongweak.Weaken
, module Strongweak.Strengthen
) where

import Strongweak.Weaken
import Strongweak.Strengthen

{- $strongweak-instance-design
We identify two distinct types of instances for strongweak classes:
* /invariant handler:/ removes or adds an invariant
* /decomposer:/ transforms through some structural type
In order to provide good behaviour and composability, we don't mix both in a
single instance. The decomposers are really just convenience to ease instance
derivation. In general, decomposers will have a recursive context, and invariant
handlers won't.
An example is @'Data.List.NonEmpty.NonEmpty' a@. We could weaken this to @[a]@,
but also to @['Weak' a]@. However, the latter would mean decomposing and
removing an invariant simultaneously. It would be two separate strengthens in
one instance. And now, your 'a' must be in the strongweak ecosystem, which isn't
necessarily what you want - indeed, it appears this sort of design would require
a @'Weak' a = a, weaken = id@ overlapping instance, which I do not want. On the
other hand, @[a]@ /does/ weaken to @['Weak' a]@, because there are no invariants
present to remove, so decomposing is all the user could hope to do.
-}
83 changes: 60 additions & 23 deletions src/Strongweak/Strengthen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,25 +17,28 @@ module Strongweak.Strengthen
-- * Helpers
, strengthenBounded

-- * 'Weak' re-export
-- * Re-exports
, Strongweak.Weaken.Weak
) where

import Strongweak.Weaken ( Weaken(..) )
import Data.Either.Validation
import Type.Reflection ( Typeable, typeRep )
import Prettyprinter
import Prettyprinter.Render.String

import GHC.TypeNats ( Natural, KnownNat )
import Data.Word
import Data.Int
import Refined ( Refined, refine, Predicate )
import Data.Vector.Sized qualified as Vector
import Data.Vector.Sized ( Vector )
import Type.Reflection ( Typeable, typeRep )

import Prettyprinter
import Prettyprinter.Render.String

import Data.Either.Validation
import Data.List.NonEmpty ( NonEmpty( (:|) ) )
import Data.Foldable qualified as Foldable
import Control.Applicative ( liftA2 )
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty ( NonEmpty( (:|) ) )
import Data.List.NonEmpty qualified as NonEmpty

{- | You may attempt to transform a @'Weak' a@ to an @a@.
Expand All @@ -48,11 +51,27 @@ We take 'Weaken' as a superclass in order to maintain strong/weak type pair
consistency. We choose this dependency direction because we treat the strong
type as the "canonical" one, so 'Weaken' is the more natural (and
straightforward) class to define.
Instances should /either/ handle an invariant, or decompose. See "Strongweak"
for a discussion on this design.
-}
class Weaken a => Strengthen a where
-- | Attempt to transform a weak value to its associated strong one.
strengthen :: Weak a -> Validation (NonEmpty StrengthenFail) a

-- | Weaken a strong value, then strengthen it again.
--
-- Potentially useful if you have previously used
-- 'Strongweak.Strengthen.Unsafe.unsafeStrengthen' and now wish to check the
-- invariants. For example:
--
-- >>> restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]
-- Failure ...
restrengthen
:: (Strengthen a, Weaken a)
=> a -> Validation (NonEmpty StrengthenFail) a
restrengthen = strengthen . weaken

-- | Strengthen failure data type. Don't use these constructors directly, use
-- the existing helper functions.
--
Expand Down Expand Up @@ -103,9 +122,12 @@ strengthenFailBase
strengthenFailBase w msg = Failure (e :| [])
where e = StrengthenFailBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg

-- | Strengthen each element of a list.
instance Strengthen a => Strengthen [a] where
strengthen = traverse strengthen
-- | Obtain a non-empty list by asserting non-emptiness of a plain list.
instance (Typeable a, Show a) => Strengthen (NonEmpty a) where
strengthen a =
case NonEmpty.nonEmpty a of
Just a' -> Success a'
Nothing -> strengthenFailBase a "empty list"

-- | Obtain a sized vector by asserting the size of a plain list.
instance (KnownNat n, Typeable a, Show a) => Strengthen (Vector n a) where
Expand Down Expand Up @@ -149,15 +171,30 @@ strengthenBounded n =
maxB = fromIntegral @b @n maxBound
minB = fromIntegral @b @n minBound

-- | Weaken a strong value, then strengthen it again.
--
-- Potentially useful if you have previously used
-- 'Strongweak.Strengthen.Unsafe.unsafeStrengthen' and now wish to check the
-- invariants. For example:
--
-- >>> restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]
-- Failure ...
restrengthen
:: (Strengthen a, Weaken a)
=> a -> Validation (NonEmpty StrengthenFail) a
restrengthen = strengthen . weaken
--------------------------------------------------------------------------------

-- | Decomposer. Strengthen every element in a list.
instance Strengthen a => Strengthen [a] where
strengthen = traverse strengthen

-- | Decomposer.
instance (Strengthen a, Strengthen b) => Strengthen (a, b) where
strengthen (a, b) = liftA2 (,) (strengthen a) (strengthen b)

-- | Decomposer.
instance Strengthen a => Strengthen (Maybe a) where
strengthen = \case Just a -> Just <$> strengthen a
Nothing -> pure Nothing

-- | Decomposer.
instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where
strengthen = \case Left a -> Left <$> strengthen a
Right b -> Right <$> strengthen b

-- | Decomposer.
instance Strengthen a => Strengthen (Identity a) where
strengthen = fmap Identity . strengthen . runIdentity

-- | Decomposer.
instance Strengthen a => Strengthen (Const a b) where
strengthen = fmap Const . strengthen . getConst
55 changes: 48 additions & 7 deletions src/Strongweak/Strengthen/Unsafe.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,25 +8,38 @@ import Refined.Unsafe ( reallyUnsafeRefine )
import Data.Vector.Sized ( Vector )
import Data.Vector.Generic.Sized.Internal qualified
import Data.Vector qualified
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

{- | Unsafely transform a @'Weak' a@ to an @a@, without asserting invariants.
For example, you may unsafely strengthen some @'Numeric.Natural.Natural' n@ into
a 'Word8' by unsafely coercing the value, ignoring the possibility that @n >=
255@.
Some unsafe strengthens are more dangerous than others. The above one would
safely overflow on invalid inputs, but others will explode your computer if it
turns out you were lying and an invariant wasn't upheld. Only consider using
this if you have a guarantee that your value is safe to treat as strong.
What happens if it turns out you're lying to the computer and your weak value
doesn't fit in its strong counterpart? That depends on the strengthen.
* Numeric coercions should safely overflow.
* Some will raise an error (e.g. 'NonEmpty').
* Others will appear to work, but later explode your computer (sized vectors
will probably do this).
Only consider using this if you have a guarantee that your value is safe to
treat as strong.
Instances should /either/ handle an invariant, or decompose. See "Strongweak"
for a discussion on this design.
-}
class Weaken a => UnsafeStrengthen a where
-- | Unsafely transform a weak value to its associated strong one.
unsafeStrengthen :: Weak a -> a

-- | Unsafely strengthen each element of a list.
instance UnsafeStrengthen a => UnsafeStrengthen [a] where
unsafeStrengthen = map unsafeStrengthen
-- | Unsafely assume a list is non-empty.
instance UnsafeStrengthen (NonEmpty a) where
unsafeStrengthen = NonEmpty.fromList

-- | Unsafely assume the size of a plain list.
instance UnsafeStrengthen (Vector n a) where
Expand All @@ -49,3 +62,31 @@ instance UnsafeStrengthen Int8 where unsafeStrengthen = fromIntegral
instance UnsafeStrengthen Int16 where unsafeStrengthen = fromIntegral
instance UnsafeStrengthen Int32 where unsafeStrengthen = fromIntegral
instance UnsafeStrengthen Int64 where unsafeStrengthen = fromIntegral

--------------------------------------------------------------------------------

-- | Decomposer. Unsafely strengthen every element in a list.
instance UnsafeStrengthen a => UnsafeStrengthen [a] where
unsafeStrengthen = map unsafeStrengthen

-- | Decomposer.
instance (UnsafeStrengthen a, UnsafeStrengthen b) => UnsafeStrengthen (a, b) where
unsafeStrengthen (a, b) = (unsafeStrengthen a, unsafeStrengthen b)

-- | Decomposer.
instance UnsafeStrengthen a => UnsafeStrengthen (Maybe a) where
unsafeStrengthen = \case Just a -> Just $ unsafeStrengthen a
Nothing -> Nothing

-- | Decomposer.
instance (UnsafeStrengthen a, UnsafeStrengthen b) => UnsafeStrengthen (Either a b) where
unsafeStrengthen = \case Left a -> Left $ unsafeStrengthen a
Right b -> Right $ unsafeStrengthen b

-- | Decomposer.
instance UnsafeStrengthen a => UnsafeStrengthen (Identity a) where
unsafeStrengthen = Identity . unsafeStrengthen . runIdentity

-- | Decomposer.
instance UnsafeStrengthen a => UnsafeStrengthen (Const a b) where
unsafeStrengthen = Const . unsafeStrengthen . getConst
49 changes: 45 additions & 4 deletions src/Strongweak/Weaken.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,20 @@ import Data.Int
import Data.Vector.Sized qualified as Vector
import Data.Vector.Sized ( Vector )
import Data.Kind ( Type )
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

{- | Transform an @a@ to a @'Weak' a@.
A given strong type @a@ has exactly one associated weak type @'Weak' a@.
Multiple strong types may weaken to the same weak type.
Law: @a === b -> 'weaken' a === 'weaken' b@
Instances should /either/ handle an invariant, or decompose. See "Strongweak"
for a discussion on this design.
-}
class Weaken a where
-- | The type to weaken to.
Expand Down Expand Up @@ -57,10 +64,10 @@ type family SW (s :: Strength) a :: Type where
SW 'Strong a = a
SW 'Weak a = Weak a

-- | Weaken each element of a list.
instance Weaken a => Weaken [a] where
type Weak [a] = [Weak a]
weaken = map weaken
-- | Weaken non-empty lists into plain lists.
instance Weaken (NonEmpty a) where
type Weak (NonEmpty a) = [a]
weaken = NonEmpty.toList

-- | Weaken sized vectors into plain lists.
instance Weaken (Vector n a) where
Expand Down Expand Up @@ -97,3 +104,37 @@ instance Weaken Int32 where
instance Weaken Int64 where
type Weak Int64 = Integer
weaken = fromIntegral

--------------------------------------------------------------------------------

-- | Decomposer. Weaken every element in a list.
instance Weaken a => Weaken [a] where
type Weak [a] = [Weak a]
weaken = map weaken

-- | Decomposer.
instance (Weaken a, Weaken b) => Weaken (a, b) where
type Weak (a, b) = (Weak a, Weak b)
weaken (a, b) = (weaken a, weaken b)

-- | Decomposer.
instance Weaken a => Weaken (Maybe a) where
type Weak (Maybe a) = Maybe (Weak a)
weaken = \case Just a -> Just $ weaken a
Nothing -> Nothing

-- | Decomposer.
instance (Weaken a, Weaken b) => Weaken (Either a b) where
type Weak (Either a b) = Either (Weak a) (Weak b)
weaken = \case Left a -> Left $ weaken a
Right b -> Right $ weaken b

-- | Decomposer.
instance Weaken a => Weaken (Identity a) where
type Weak (Identity a) = Identity (Weak a)
weaken = Identity . weaken . runIdentity

-- | Decomposer.
instance Weaken a => Weaken (Const a b) where
type Weak (Const a b) = Const (Weak a) b
weaken = Const . weaken . getConst

0 comments on commit c03b2ff

Please sign in to comment.