module Strongweak.Weaken
(
Weaken(..)
, liftWeakF
, Strength(..)
, SW
) where
import Refined ( Refined, unrefine )
import Numeric.Natural ( Natural )
import Data.Word
import Data.Int
import Data.Vector.Generic.Sized qualified as VGS
import Data.Vector.Generic qualified as VG
import Data.Kind ( Type )
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )
class Weaken a where
type Weak a :: Type
weaken :: a -> Weak a
liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b)
liftWeakF :: forall a b. Weaken a => (Weak a -> b) -> a -> b
liftWeakF Weak a -> b
f = Weak a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Weaken a => a -> Weak a
weaken
data Strength = Strong | Weak
type family SW (s :: Strength) a :: Type where
SW 'Strong a = a
SW 'Weak a = Weak a
instance Weaken (Refined p a) where
type Weak (Refined p a) = a
weaken :: Refined p a -> Weak (Refined p a)
weaken = forall {k} (p :: k) x. Refined p x -> x
unrefine
instance Weaken (NonEmpty a) where
type Weak (NonEmpty a) = [a]
weaken :: NonEmpty a -> Weak (NonEmpty a)
weaken = forall a. NonEmpty a -> [a]
NonEmpty.toList
instance VG.Vector v a => Weaken (VGS.Vector v n a) where
type Weak (VGS.Vector v n a) = [a]
weaken :: Vector v n a -> Weak (Vector v n a)
weaken = forall (v :: Type -> Type) a (n :: Nat).
Vector v a =>
Vector v n a -> [a]
VGS.toList
instance Weaken (Identity a) where
type Weak (Identity a) = a
weaken :: Identity a -> Weak (Identity a)
weaken = forall a. Identity a -> a
runIdentity
instance Weaken (Const a b) where
type Weak (Const a b) = a
weaken :: Const a b -> Weak (Const a b)
weaken = forall {k} a (b :: k). Const a b -> a
getConst
instance Weaken Word8 where
type Weak Word8 = Natural
weaken :: Word8 -> Weak Word8
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word16 where
type Weak Word16 = Natural
weaken :: Word16 -> Weak Word16
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word32 where
type Weak Word32 = Natural
weaken :: Word32 -> Weak Word32
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word64 where
type Weak Word64 = Natural
weaken :: Word64 -> Weak Word64
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int8 where
type Weak Int8 = Integer
weaken :: Int8 -> Weak Int8
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int16 where
type Weak Int16 = Integer
weaken :: Int16 -> Weak Int16
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int32 where
type Weak Int32 = Integer
weaken :: Int32 -> Weak Int32
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int64 where
type Weak Int64 = Integer
weaken :: Int64 -> Weak Int64
weaken = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken a => Weaken [a] where
type Weak [a] = [Weak a]
weaken :: [a] -> Weak [a]
weaken = forall a b. (a -> b) -> [a] -> [b]
map forall a. Weaken a => a -> Weak a
weaken
instance (Weaken a, Weaken b) => Weaken (a, b) where
type Weak (a, b) = (Weak a, Weak b)
weaken :: (a, b) -> Weak (a, b)
weaken (a
a, b
b) = (forall a. Weaken a => a -> Weak a
weaken a
a, forall a. Weaken a => a -> Weak a
weaken b
b)
instance (Weaken a, Weaken b) => Weaken (Either a b) where
type Weak (Either a b) = Either (Weak a) (Weak b)
weaken :: Either a b -> Weak (Either a b)
weaken = \case Left a
a -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. Weaken a => a -> Weak a
weaken a
a
Right b
b -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Weaken a => a -> Weak a
weaken b
b