{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE GADTs #-}
module Data.Unrestricted.Internal.Dupable
  (
  -- * Dupable
    Dupable(..)
  , dup
  , dup3
  ) where

import Data.Unrestricted.Internal.Consumable
import GHC.TypeLits
import Data.Type.Equality
import Data.V.Linear.Internal.V (V)
import qualified Data.V.Linear.Internal.V as V

-- | The laws of @Dupable@ are dual to those of 'Monoid':
--
-- * @first consume (dup2 a) ≃ a ≃ second consume (dup2 a)@ (neutrality)
-- * @first dup2 (dup2 a) ≃ (second dup2 (dup2 a))@ (associativity)
--
-- Where the @(≃)@ sign represents equality up to type isomorphism.
--
-- When implementing 'Dupable' instances for composite types, using 'dupV'
-- should be more convenient since 'V' has a zipping 'Applicative' instance.
class Consumable a => Dupable a where
  {-# MINIMAL dupV | dup2 #-}

  dupV :: forall n. KnownNat n => a %1-> V n a
  dupV a
a =
    case forall (n :: Nat).
KnownNat n =>
Either (n :~: 0) ((1 <=? n) :~: 'True)
V.caseNat @n of
      Prelude.Left n :~: 0
Refl -> a
a a %1 -> V n a %1 -> V n a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` forall (n :: Nat) a. KnownNat n => FunN n a (V n a)
V.make @0 @a
      Prelude.Right (1 <=? n) :~: 'True
Refl -> (a %1 -> (a, a)) -> a %1 -> V n a
forall (n :: Nat) a.
(KnownNat n, 1 <= n) =>
(a %1 -> (a, a)) -> a %1 -> V n a
V.iterate a %1 -> (a, a)
forall a. Dupable a => a %1 -> (a, a)
dup2 a
a

  dup2 :: a %1-> (a, a)
  dup2 a
a = V 2 a %1 -> FunN 2 a (a, a) %1 -> (a, a)
forall (n :: Nat) a b. KnownNat n => V n a %1 -> FunN n a b %1 -> b
V.elim (forall a (n :: Nat). (Dupable a, KnownNat n) => a %1 -> V n a
dupV @a @2 a
a) (,)

dup3 :: Dupable a => a %1-> (a, a, a)
dup3 :: forall a. Dupable a => a %1 -> (a, a, a)
dup3 a
x = V 3 a %1 -> FunN 3 a (a, a, a) %1 -> (a, a, a)
forall (n :: Nat) a b. KnownNat n => V n a %1 -> FunN n a b %1 -> b
V.elim (forall a (n :: Nat). (Dupable a, KnownNat n) => a %1 -> V n a
dupV @_ @3 a
x) (,,)

dup :: Dupable a => a %1-> (a, a)
dup :: forall a. Dupable a => a %1 -> (a, a)
dup = a %1 -> (a, a)
forall a. Dupable a => a %1 -> (a, a)
dup2