{-# LANGUAGE FunctionalDependencies #-}

module Strongweak.Weaken where

import Refined ( Refined, unrefine )
import Numeric.Natural ( Natural )
import Data.Word
import Data.Int
import Data.Vector.Sized qualified as Vector
import Data.Vector.Sized ( Vector )

{- | Any 's' can be "weakened" into a 'w'.

For example, you may weaken a 'Word8' into a 'Natural'.

Note that we restrict strengthened types to having only one corresponding weak
representation using functional dependencies.
-}
class Weaken s w | s -> w where weaken :: s -> w

-- | Weaken each element of a list
instance Weaken s w => Weaken [s] [w] where weaken :: [s] -> [w]
weaken = (s -> w) -> [s] -> [w]
forall a b. (a -> b) -> [a] -> [b]
map s -> w
forall s w. Weaken s w => s -> w
weaken

-- | Weaken sized vectors into plain lists.
instance Weaken (Vector n a) [a] where weaken :: Vector n a -> [a]
weaken = Vector n a -> [a]
forall (n :: Nat) a. Vector n a -> [a]
Vector.toList

-- | Strip the refinement from refined types.
instance Weaken (Refined p a) a where weaken :: Refined p a -> a
weaken = Refined p a -> a
forall p a. Refined p a -> a
unrefine

-- Weaken the bounded Haskell numeric types using 'fromIntegral'.
instance Weaken Word8  Natural where weaken :: Word8 -> Nat
weaken = Word8 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word16 Natural where weaken :: Word16 -> Nat
weaken = Word16 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word32 Natural where weaken :: Word32 -> Nat
weaken = Word32 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word64 Natural where weaken :: Word64 -> Nat
weaken = Word64 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int8   Integer where weaken :: Int8 -> Integer
weaken = Int8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int16  Integer where weaken :: Int16 -> Integer
weaken = Int16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int32  Integer where weaken :: Int32 -> Integer
weaken = Int32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int64  Integer where weaken :: Int64 -> Integer
weaken = Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral