{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.ZX where

import Data.Bits (Bits (..), shiftL, (.|.))
import Data.Char (chr)
import Data.Complex (Complex (..), conjugate, magnitude, mkPolar)
import Data.List (intercalate, sort)
import Data.Map.Strict qualified as Map
import Data.Proxy (Proxy (..))
import GHC.TypeLits.Witnesses ((%+))
import GHC.TypeNats (KnownNat, Nat, natVal, pattern SNat, type (+))
import Numeric (showFFloat)
import Unsafe.Coerce (unsafeCoerce)
import Prelude hiding (id, (.))

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Object.Dual (CompactClosed (..), ExpSA, StarAutonomous (..), currySA, expSA, uncurrySA)
import Proarrow.Object.Exponential (Closed (..))

newtype Bitstring (n :: Nat) = BS Int
  deriving (Bitstring n -> Bitstring n -> Bool
(Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool) -> Eq (Bitstring n)
forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
== :: Bitstring n -> Bitstring n -> Bool
$c/= :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
/= :: Bitstring n -> Bitstring n -> Bool
Eq, Eq (Bitstring n)
Eq (Bitstring n) =>
(Bitstring n -> Bitstring n -> Ordering)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bool)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> Ord (Bitstring n)
Bitstring n -> Bitstring n -> Bool
Bitstring n -> Bitstring n -> Ordering
Bitstring n -> Bitstring n -> Bitstring n
forall (n :: Natural). Eq (Bitstring n)
forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
forall (n :: Natural). Bitstring n -> Bitstring n -> Ordering
forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Natural). Bitstring n -> Bitstring n -> Ordering
compare :: Bitstring n -> Bitstring n -> Ordering
$c< :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
< :: Bitstring n -> Bitstring n -> Bool
$c<= :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
<= :: Bitstring n -> Bitstring n -> Bool
$c> :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
> :: Bitstring n -> Bitstring n -> Bool
$c>= :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bool
>= :: Bitstring n -> Bitstring n -> Bool
$cmax :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
max :: Bitstring n -> Bitstring n -> Bitstring n
$cmin :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
min :: Bitstring n -> Bitstring n -> Bitstring n
Ord, Integer -> Bitstring n
Bitstring n -> Bitstring n
Bitstring n -> Bitstring n -> Bitstring n
(Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Bitstring n -> Bitstring n)
-> (Integer -> Bitstring n)
-> Num (Bitstring n)
forall (n :: Natural). Integer -> Bitstring n
forall (n :: Natural). Bitstring n -> Bitstring n
forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
+ :: Bitstring n -> Bitstring n -> Bitstring n
$c- :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
- :: Bitstring n -> Bitstring n -> Bitstring n
$c* :: forall (n :: Natural). Bitstring n -> Bitstring n -> Bitstring n
* :: Bitstring n -> Bitstring n -> Bitstring n
$cnegate :: forall (n :: Natural). Bitstring n -> Bitstring n
negate :: Bitstring n -> Bitstring n
$cabs :: forall (n :: Natural). Bitstring n -> Bitstring n
abs :: Bitstring n -> Bitstring n
$csignum :: forall (n :: Natural). Bitstring n -> Bitstring n
signum :: Bitstring n -> Bitstring n
$cfromInteger :: forall (n :: Natural). Integer -> Bitstring n
fromInteger :: Integer -> Bitstring n
Num)

instance (KnownNat n) => Bounded (Bitstring n) where
  minBound :: Bitstring n
minBound = Int -> Bitstring n
forall (n :: Natural). Int -> Bitstring n
BS Int
0
  maxBound :: Bitstring n
maxBound = Int -> Bitstring n
forall (n :: Natural). Int -> Bitstring n
BS ((Int
1 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` forall (n :: Natural). KnownNat n => Int
nat @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
instance Enum (Bitstring n) where
  fromEnum :: Bitstring n -> Int
fromEnum (BS Int
x) = Int
x
  toEnum :: Int -> Bitstring n
toEnum Int
x = Int -> Bitstring n
forall (n :: Natural). Int -> Bitstring n
BS Int
x

-- | Split n + m bits into two parts: the lower n bits and the higher m bits.
split :: (KnownNat n) => Bitstring (n + m) -> (Bitstring n, Bitstring m)
split :: forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring (n + m) -> (Bitstring n, Bitstring m)
split @n (BS Int
x) = case (Int
x Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`divMod` (Int
1 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` forall (n :: Natural). KnownNat n => Int
nat @n)) of (Int
m, Int
n) -> (Int -> Bitstring n
forall (n :: Natural). Int -> Bitstring n
BS Int
n, Int -> Bitstring m
forall (n :: Natural). Int -> Bitstring n
BS Int
m)

-- | Combine two bitstrings of lengths n and m into one bitstring with the n lower bits or m higher bits.
combine :: (KnownNat n) => Bitstring n -> Bitstring m -> Bitstring (n + m)
combine :: forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine @n (BS Int
x) (BS Int
y) = Int -> Bitstring (n + m)
forall (n :: Natural). Int -> Bitstring n
BS ((Int
y Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` forall (n :: Natural). KnownNat n => Int
nat @n) Int -> Int -> Int
forall a. Bits a => a -> a -> a
.|. Int
x)

-- The order is (output, input)!
type SparseMatrix o i = Map.Map (Bitstring o, Bitstring i) (Complex Double)

epsilon :: Double
epsilon :: Double
epsilon = Double
1e-12

filterSparse :: SparseMatrix o i -> SparseMatrix o i
filterSparse :: forall (o :: Natural) (i :: Natural).
SparseMatrix o i -> SparseMatrix o i
filterSparse = (Complex Double -> Bool)
-> Map (Bitstring o, Bitstring i) (Complex Double)
-> Map (Bitstring o, Bitstring i) (Complex Double)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Complex Double
z -> Double
epsilon Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Complex Double -> Double
forall a. RealFloat a => Complex a -> a
magnitude Complex Double
z)

transpose :: SparseMatrix o i -> SparseMatrix i o
transpose :: forall (o :: Natural) (i :: Natural).
SparseMatrix o i -> SparseMatrix i o
transpose = ((Bitstring o, Bitstring i) -> (Bitstring i, Bitstring o))
-> Map (Bitstring o, Bitstring i) (Complex Double)
-> Map (Bitstring i, Bitstring o) (Complex Double)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys \(Bitstring o
o, Bitstring i
i) -> (Bitstring i
i, Bitstring o
o)

mirror :: (KnownNat n) => Bitstring n -> Bitstring (n + n)
mirror :: forall (n :: Natural).
KnownNat n =>
Bitstring n -> Bitstring (n + n)
mirror @n (BS Int
x) = Int -> Bitstring (n + n)
forall (n :: Natural). Int -> Bitstring n
BS (Int -> Int -> Int -> Int
forall {t} {t}. (Bits t, Num t, Num t, Eq t) => t -> t -> t -> t
go (forall (n :: Natural). KnownNat n => Int
nat @n) Int
x Int
x)
  where
    go :: t -> t -> t -> t
go t
0 t
_ t
acc = t
acc
    go t
k t
y t
acc = t -> t -> t -> t
go (t
k t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (t
y t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) ((t
acc t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftL` Int
1) t -> t -> t
forall a. Bits a => a -> a -> a
.|. (t
y t -> t -> t
forall a. Bits a => a -> a -> a
.&. t
1))

enumAll :: (KnownNat n) => [Bitstring n]
enumAll :: forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll = [Bitstring n
forall a. Bounded a => a
minBound .. Bitstring n
forall a. Bounded a => a
maxBound]

nat :: (KnownNat n) => Int
nat :: forall (n :: Natural). KnownNat n => Int
nat @n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

type ZX :: CAT Nat
data ZX i o where
  ZX :: (KnownNat i, KnownNat o) => SparseMatrix o i -> ZX i o

instance (KnownNat n) => Show (Bitstring n) where
  show :: Bitstring n -> String
show (BS Int
x) = Int -> Int -> ShowS
forall {t}. (Eq t, Num t) => t -> Int -> ShowS
go (forall (n :: Natural). KnownNat n => Int
nat @n) Int
x String
""
    where
      go :: t -> Int -> ShowS
go t
0 Int
_ String
acc = String
acc
      go t
n Int
bs String
acc = case Int
bs Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`divMod` Int
2 of (Int
r, Int
b) -> t -> Int -> ShowS
go (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) Int
r (Int -> Char
chr (Int
48 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b) Char -> ShowS
forall a. a -> [a] -> [a]
: String
acc)

instance Show (ZX a b) where
  show :: ZX a b -> String
show (ZX SparseMatrix b a
m) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> [String]
forall a. Ord a => [a] -> [a]
sort (((Bitstring b, Bitstring a), Complex Double) -> String
forall {a} {a}.
(Show a, Show a) =>
((a, a), Complex Double) -> String
fmt (((Bitstring b, Bitstring a), Complex Double) -> String)
-> [((Bitstring b, Bitstring a), Complex Double)] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SparseMatrix b a -> [((Bitstring b, Bitstring a), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix b a
m))
    where
      fmt :: ((a, a), Complex Double) -> String
fmt ((a
o, a
i), Double
r :+ Double
c) =
        a -> String
forall a. Show a => a -> String
show a
i
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"->"
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
o
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"="
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Double -> Double
forall a. Num a => a -> a
abs (Double
1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
r) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
epsilon then String
"1" else Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3) Double
r String
"")
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Double -> Double
forall a. Num a => a -> a
abs Double
c Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
epsilon then String
"" else String
" :+ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3) Double
c String
"")

instance Profunctor ZX where
  dimap :: forall (c :: Natural) (a :: Natural) (b :: Natural) (d :: Natural).
(c ~> a) -> (b ~> d) -> ZX a b -> ZX c d
dimap = (c ~> a) -> (b ~> d) -> ZX a b -> ZX c d
ZX c a -> ZX b d -> ZX a b -> ZX c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: Natural) (b :: Natural) r.
((Ob a, Ob b) => r) -> ZX a b -> r
\\ ZX SparseMatrix b a
_ = r
(Ob a, Ob b) => r
r
instance Promonad ZX where
  id :: forall (a :: Natural). Ob a => ZX a a
id @n = SparseMatrix a a -> ZX a a
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix a a -> ZX a a) -> SparseMatrix a a -> ZX a a
forall a b. (a -> b) -> a -> b
$ [((Bitstring a, Bitstring a), Complex Double)] -> SparseMatrix a a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((Bitstring a
i, Bitstring a
i), Complex Double
1) | Bitstring a
i <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n]
  ZX SparseMatrix c b
n . :: forall (b :: Natural) (c :: Natural) (a :: Natural).
ZX b c -> ZX a b -> ZX a c
. ZX SparseMatrix b a
m =
    SparseMatrix c a -> ZX a c
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix c a -> ZX a c) -> SparseMatrix c a -> ZX a c
forall a b. (a -> b) -> a -> b
$
      SparseMatrix c a -> SparseMatrix c a
forall (o :: Natural) (i :: Natural).
SparseMatrix o i -> SparseMatrix o i
filterSparse (SparseMatrix c a -> SparseMatrix c a)
-> SparseMatrix c a -> SparseMatrix c a
forall a b. (a -> b) -> a -> b
$
        (Complex Double -> Complex Double -> Complex Double)
-> [((Bitstring c, Bitstring a), Complex Double)]
-> SparseMatrix c a
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith
          Complex Double -> Complex Double -> Complex Double
forall a. Num a => a -> a -> a
(+)
          [ ((Bitstring c
c, Bitstring a
a), Complex Double
mv Complex Double -> Complex Double -> Complex Double
forall a. Num a => a -> a -> a
* Complex Double
nv)
          | ((Bitstring c
c, Bitstring b
b1), Complex Double
mv) <- SparseMatrix c b -> [((Bitstring c, Bitstring b), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix c b
n
          , ((Bitstring b
b2, Bitstring a
a), Complex Double
nv) <- SparseMatrix b a -> [((Bitstring b, Bitstring a), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix b a
m
          , Bitstring b
b1 Bitstring b -> Bitstring b -> Bool
forall a. Eq a => a -> a -> Bool
== Bitstring b
b2
          ]
-- | The category of qubits, to implement ZX calculus from quantum computing.
instance CategoryOf Nat where
  type (~>) = ZX
  type Ob a = KnownNat a

instance DaggerProfunctor ZX where
  dagger :: forall (a :: Natural) (b :: Natural). ZX a b -> ZX b a
dagger (ZX SparseMatrix b a
m) = SparseMatrix a b -> ZX b a
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix a b -> ZX b a) -> SparseMatrix a b -> ZX b a
forall a b. (a -> b) -> a -> b
$ [((Bitstring a, Bitstring b), Complex Double)] -> SparseMatrix a b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((Bitstring a
i, Bitstring b
o), Complex Double -> Complex Double
forall a. Num a => Complex a -> Complex a
conjugate Complex Double
v) | ((Bitstring b
o, Bitstring a
i), Complex Double
v) <- SparseMatrix b a -> [((Bitstring b, Bitstring a), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix b a
m]

instance MonoidalProfunctor ZX where
  par0 :: ZX Unit Unit
par0 = SparseMatrix 0 0 -> ZX 0 0
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX SparseMatrix 0 0
forall k a. Map k a
Map.empty
  ZX @ni @no SparseMatrix x2 x1
n par :: forall (x1 :: Natural) (x2 :: Natural) (y1 :: Natural)
       (y2 :: Natural).
ZX x1 x2 -> ZX y1 y2 -> ZX (x1 ** y1) (x2 ** y2)
`par` ZX @mi @mo SparseMatrix y2 y1
m =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @ni @mi ((Ob (x1 ** y1) => ZX (x1 ** y1) (x2 ** y2))
 -> ZX (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => ZX (x1 ** y1) (x2 ** y2))
-> ZX (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @no @mo ((Ob (x2 ** y2) => ZX (x1 ** y1) (x2 ** y2))
 -> ZX (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => ZX (x1 ** y1) (x2 ** y2))
-> ZX (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
        SparseMatrix (x2 ** y2) (x1 ** y1) -> ZX (x1 ** y1) (x2 ** y2)
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix (x2 ** y2) (x1 ** y1) -> ZX (x1 ** y1) (x2 ** y2))
-> SparseMatrix (x2 ** y2) (x1 ** y1) -> ZX (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
          [((Bitstring (x2 + y2), Bitstring (x1 + y1)), Complex Double)]
-> Map (Bitstring (x2 + y2), Bitstring (x1 + y1)) (Complex Double)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
            [ ((Bitstring x2 -> Bitstring y2 -> Bitstring (x2 + y2)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring x2
no Bitstring y2
mo, Bitstring x1 -> Bitstring y1 -> Bitstring (x1 + y1)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring x1
ni Bitstring y1
mi), Complex Double
nv Complex Double -> Complex Double -> Complex Double
forall a. Num a => a -> a -> a
* Complex Double
mv)
            | ((Bitstring x2
no, Bitstring x1
ni), Complex Double
nv) <- SparseMatrix x2 x1
-> [((Bitstring x2, Bitstring x1), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix x2 x1
n
            , ((Bitstring y2
mo, Bitstring y1
mi), Complex Double
mv) <- SparseMatrix y2 y1
-> [((Bitstring y2, Bitstring y1), Complex Double)]
forall k a. Map k a -> [(k, a)]
Map.toList SparseMatrix y2 y1
m
            ]

-- | Addition of the number of qubits as monoidal tensor. This is the Kronecker product of the matrices.
instance Monoidal Nat where
  type Unit = 0
  type p ** q = p + q
  withOb2 :: forall (a :: Natural) (b :: Natural) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b Ob (a ** b) => r
r = case (forall (n :: Natural). KnownNat n => SNat n
SNat @a) SNat a -> SNat b -> SNat (a + b)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ (forall (n :: Natural). KnownNat n => SNat n
SNat @b) of SNat (a + b)
SNat -> r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: Natural). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
ZX a a
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  leftUnitorInv :: forall (a :: Natural). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
ZX a a
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  rightUnitor :: forall (a :: Natural). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
ZX a a
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  rightUnitorInv :: forall (a :: Natural). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
ZX a a
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  associator :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (a ** b) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(a + b) @c ((Ob ((a + b) ** c) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob ((a + b) ** c) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$ ZX ((a + b) + c) ((a + b) + c) -> ZX ((a + b) + c) (a + (b + c))
forall a b. a -> b
unsafeCoerce (forall (a :: Natural). (CategoryOf Natural, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a + b + c))
  associatorInv :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (a ** b) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(a + b) @c ((Ob ((a + b) ** c) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob ((a + b) ** c) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$ ZX ((a + b) + c) ((a + b) + c) -> ZX (a + (b + c)) ((a + b) + c)
forall a b. a -> b
unsafeCoerce (forall (a :: Natural). (CategoryOf Natural, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a + b + c))
instance SymMonoidal Nat where
  swap :: forall (a :: Natural) (b :: Natural).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @m @n =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @m @n ((Ob (a ** b) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a))
-> (Ob (a ** b) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @n @m ((Ob (b ** a) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a))
-> (Ob (b ** a) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
        SparseMatrix (b + a) (a + b) -> ZX (a + b) (b + a)
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix (b + a) (a + b) -> ZX (a + b) (b + a))
-> SparseMatrix (b + a) (a + b) -> ZX (a + b) (b + a)
forall a b. (a -> b) -> a -> b
$
          [((Bitstring (b + a), Bitstring (a + b)), Complex Double)]
-> SparseMatrix (b + a) (a + b)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
            [ ((Bitstring b -> Bitstring a -> Bitstring (b + a)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring b
n Bitstring a
m, Bitstring a -> Bitstring b -> Bitstring (a + b)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring a
m Bitstring b
n), Complex Double
1)
            | Bitstring b
n <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n
            , Bitstring a
m <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @m
            ]

instance Closed Nat where
  type x ~~> y = ExpSA x y
  withObExp :: forall (a :: Natural) (b :: Natural) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a @b Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b r
Ob (a ** b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @x @y = forall (a :: Natural) (b :: Natural) (c :: Natural).
(StarAutonomous Natural, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @x @y
  uncurry :: forall (b :: Natural) (c :: Natural) (a :: Natural).
(Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @y @z = forall (b :: Natural) (c :: Natural) (a :: Natural).
(StarAutonomous Natural, Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(StarAutonomous k, Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
uncurrySA @y @z
  ^^^ :: forall (a :: Natural) (b :: Natural) (x :: Natural) (y :: Natural).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA

instance StarAutonomous Nat where
  type Dual x = x
  dual :: forall (a :: Natural) (b :: Natural). (a ~> b) -> Dual b ~> Dual a
dual (ZX SparseMatrix b a
m) = SparseMatrix a b -> ZX b a
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix b a -> SparseMatrix a b
forall (o :: Natural) (i :: Natural).
SparseMatrix o i -> SparseMatrix i o
transpose SparseMatrix b a
m)
  dualInv :: forall (a :: Natural) (b :: Natural).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (a ~> b) -> Dual b ~> Dual a
(Dual a ~> Dual b) -> b ~> a
forall (a :: Natural) (b :: Natural). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual
  linDist :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @_ @b @c (ZX SparseMatrix c (a + b)
m) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c ((Ob (b ** c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c))
-> (Ob (b ** c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
      SparseMatrix (b + c) a -> ZX a (b + c)
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (((Bitstring c, Bitstring (a + b))
 -> (Bitstring (b + c), Bitstring a))
-> SparseMatrix c (a + b) -> SparseMatrix (b + c) a
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(Bitstring c
c, Bitstring (a + b)
ab) -> case Bitstring (a + b) -> (Bitstring a, Bitstring b)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring (n + m) -> (Bitstring n, Bitstring m)
split Bitstring (a + b)
ab of (Bitstring a
a, Bitstring b
b) -> (Bitstring b -> Bitstring c -> Bitstring (b + c)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring b
b Bitstring c
c, Bitstring a
a)) SparseMatrix c (a + b)
m)
  linDistInv :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @a @b (ZX SparseMatrix (b + c) a
m) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c)
-> (Ob (a ** b) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
      SparseMatrix c (a + b) -> ZX (a + b) c
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (((Bitstring (b + c), Bitstring a)
 -> (Bitstring c, Bitstring (a + b)))
-> SparseMatrix (b + c) a -> SparseMatrix c (a + b)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(Bitstring (b + c)
bc, Bitstring a
a) -> case Bitstring (b + c) -> (Bitstring b, Bitstring c)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring (n + m) -> (Bitstring n, Bitstring m)
split Bitstring (b + c)
bc of (Bitstring b
b, Bitstring c
c) -> (Bitstring c
c, Bitstring a -> Bitstring b -> Bitstring (a + b)
forall (n :: Natural) (m :: Natural).
KnownNat n =>
Bitstring n -> Bitstring m -> Bitstring (n + m)
combine Bitstring a
a Bitstring b
b)) SparseMatrix (b + c) a
m)

instance CompactClosed Nat where
  distribDual :: forall (a :: Natural) (b :: Natural).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @a @b = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ZX (a + b) (a + b)
Ob (a ** b) => ZX (a + b) (a + b)
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  dualUnit :: Dual Unit ~> Unit
dualUnit = SparseMatrix 0 0 -> ZX 0 0
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX SparseMatrix 0 0
forall k a. Map k a
Map.empty

zSpider :: (KnownNat i, KnownNat o) => Double -> ZX i o
zSpider :: forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
alpha = SparseMatrix o i -> ZX i o
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix o i -> ZX i o) -> SparseMatrix o i -> ZX i o
forall a b. (a -> b) -> a -> b
$ [((Bitstring o, Bitstring i), Complex Double)] -> SparseMatrix o i
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Bitstring o, Bitstring i), Complex Double)]
 -> SparseMatrix o i)
-> [((Bitstring o, Bitstring i), Complex Double)]
-> SparseMatrix o i
forall a b. (a -> b) -> a -> b
$ [((Bitstring o, Bitstring i)
forall a. Bounded a => a
minBound, Complex Double
1), ((Bitstring o, Bitstring i)
forall a. Bounded a => a
maxBound, Double -> Double -> Complex Double
forall a. Floating a => a -> a -> Complex a
mkPolar Double
1 Double
alpha)]

xSpider :: (KnownNat i, KnownNat o) => Double -> ZX i o
xSpider :: forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
alpha = ZX o o
forall (n :: Natural). KnownNat n => ZX n n
hadamard ZX o o -> ZX i o -> ZX i o
forall (b :: Natural) (c :: Natural) (a :: Natural).
ZX b c -> ZX a b -> ZX a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Double -> ZX i o
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
alpha ZX i o -> ZX i i -> ZX i o
forall (b :: Natural) (c :: Natural) (a :: Natural).
ZX b c -> ZX a b -> ZX a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ZX i i
forall (n :: Natural). KnownNat n => ZX n n
hadamard

cup :: (KnownNat n) => ZX 0 (n + n)
cup :: forall (n :: Natural). KnownNat n => ZX 0 (n + n)
cup @n = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @n @n ((Ob (n ** n) => ZX 0 (n + n)) -> ZX 0 (n + n))
-> (Ob (n ** n) => ZX 0 (n + n)) -> ZX 0 (n + n)
forall a b. (a -> b) -> a -> b
$ SparseMatrix (n + n) 0 -> ZX 0 (n + n)
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix (n + n) 0 -> ZX 0 (n + n))
-> SparseMatrix (n + n) 0 -> ZX 0 (n + n)
forall a b. (a -> b) -> a -> b
$ [((Bitstring (n + n), Bitstring 0), Complex Double)]
-> SparseMatrix (n + n) 0
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((Bitstring n -> Bitstring (n + n)
forall (n :: Natural).
KnownNat n =>
Bitstring n -> Bitstring (n + n)
mirror Bitstring n
i, Bitstring 0
0), Complex Double
1) | Bitstring n
i <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n]

cap :: (KnownNat n) => ZX (n + n) 0
cap :: forall (n :: Natural). KnownNat n => ZX (n + n) 0
cap @n = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @n @n ((Ob (n ** n) => ZX (n + n) 0) -> ZX (n + n) 0)
-> (Ob (n ** n) => ZX (n + n) 0) -> ZX (n + n) 0
forall a b. (a -> b) -> a -> b
$ SparseMatrix 0 (n + n) -> ZX (n + n) 0
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix 0 (n + n) -> ZX (n + n) 0)
-> SparseMatrix 0 (n + n) -> ZX (n + n) 0
forall a b. (a -> b) -> a -> b
$ [((Bitstring 0, Bitstring (n + n)), Complex Double)]
-> SparseMatrix 0 (n + n)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((Bitstring 0
0, Bitstring n -> Bitstring (n + n)
forall (n :: Natural).
KnownNat n =>
Bitstring n -> Bitstring (n + n)
mirror Bitstring n
i), Complex Double
1) | Bitstring n
i <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n]

zCopy :: ZX 1 2
zCopy :: ZX 1 2
zCopy = Double -> ZX 1 2
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
0

zDisc :: ZX 1 0
zDisc :: ZX 1 0
zDisc = Double -> ZX 1 0
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
0

xCopy :: ZX 1 2
xCopy :: ZX 1 2
xCopy = Double -> ZX 1 2
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
0

xDisc :: ZX 1 0
xDisc :: ZX 1 0
xDisc = Double -> ZX 1 0
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
0

zeroState :: ZX 0 1
zeroState :: ZX 0 1
zeroState = Double -> ZX 0 1
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
0

oneState :: ZX 0 1
oneState :: ZX 0 1
oneState = Double -> ZX 0 1
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
forall a. Floating a => a
pi

plusState :: ZX 0 1
plusState :: ZX 0 1
plusState = Double -> ZX 0 1
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
0

minusState :: ZX 0 1
minusState :: ZX 0 1
minusState = Double -> ZX 0 1
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
forall a. Floating a => a
pi

not :: ZX 1 1
not :: ZX 1 1
not = Double -> ZX 1 1
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider Double
forall a. Floating a => a
pi

-- | Controlled NOT gate
cnot :: ZX 2 2
cnot :: ZX 2 2
cnot = (ZX 1 1
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ZX 1 1 -> ZX 2 1 -> ZX (1 ** 2) (1 ** 1)
forall (x1 :: Natural) (x2 :: Natural) (y1 :: Natural)
       (y2 :: Natural).
ZX x1 x2 -> ZX y1 y2 -> ZX (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
xSpider @2 Double
0) ZX (1 + 2) 2 -> ZX 2 (1 + 2) -> ZX 2 2
forall (b :: Natural) (c :: Natural) (a :: Natural).
ZX b c -> ZX a b -> ZX a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ZX 1 2
zCopy ZX 1 2 -> ZX 1 1 -> ZX (1 ** 1) (2 ** 1)
forall (x1 :: Natural) (x2 :: Natural) (y1 :: Natural)
       (y2 :: Natural).
ZX x1 x2 -> ZX y1 y2 -> ZX (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` ZX 1 1
forall (a :: Natural). Ob a => ZX a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | Greenberger–Horne–Zeilinger state
ghzState :: ZX 0 3
ghzState :: ZX 0 3
ghzState = Double -> ZX 0 3
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
Double -> ZX i o
zSpider Double
0

hadamard :: (KnownNat n) => ZX n n
hadamard :: forall (n :: Natural). KnownNat n => ZX n n
hadamard @n = SparseMatrix n n -> ZX n n
forall (i :: Natural) (o :: Natural).
(KnownNat i, KnownNat o) =>
SparseMatrix o i -> ZX i o
ZX (SparseMatrix n n -> ZX n n) -> SparseMatrix n n -> ZX n n
forall a b. (a -> b) -> a -> b
$ [((Bitstring n, Bitstring n), Complex Double)] -> SparseMatrix n n
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((Bitstring n
i, Bitstring n
j), (Bitstring n -> Bitstring n -> Double
forall {a} {n :: Natural} {n :: Natural}.
Num a =>
Bitstring n -> Bitstring n -> a
sign Bitstring n
i Bitstring n
j Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
amp) Double -> Double -> Complex Double
forall a. a -> a -> Complex a
:+ Double
0) | Bitstring n
i <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n, Bitstring n
j <- forall (n :: Natural). KnownNat n => [Bitstring n]
enumAll @n]
  where
    amp :: Double
amp = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double -> Double
forall a. Floating a => a -> a
sqrt (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int -> Int
forall a. Bits a => a -> Int -> a
shiftL (Int
1 :: Int) (forall (n :: Natural). KnownNat n => Int
nat @n)))
    sign :: Bitstring n -> Bitstring n -> a
sign (BS Int
a) (BS Int
b) = if Int -> Bool
forall a. Integral a => a -> Bool
even (Int -> Int
forall a. Bits a => a -> Int
popCount (Int
a Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. Int
b)) then a
1 else -a
1