{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}

{-# LANGUAGE NoMonomorphismRestriction #-}



-- Quantum lambda-calculus with named variables:
-- booleans, qbits, tests and pairing.

-- At the end, implementation of the teleportation algorithm.
-- No "real" instance for Judg yet

module FullQLC where

data Z = Z
data S a = S a

data Flag f a = Flag a

data Dup = Dup
data Sim = Sim

data Qbit = Qbit Bool

data Used a = Used a
data Free a = Free a

data Dummy = Dummy


-- Ordering on flags.

class FlagSubType a b

instance FlagSubType a a
instance FlagSubType Dup a
instance FlagSubType a Sim
instance (Dup ~ a) => FlagSubType a Dup
instance (Sim ~ a) => FlagSubType Sim a
-- close overlapping cases
instance FlagSubType Dup Sim
instance FlagSubType Dup Dup
instance FlagSubType Sim Sim
instance (Dup ~ Sim) => FlagSubType Sim Dup

-- Ordering on types
-- There are two of them so that one can infer left and right hands.
-- Double functional dependencies do not do the job, for some reason.

class TestSubType a b | a -> b, b -> a where
   subType :: a -> b

instance TestSubType Bool Bool where subType x = x
instance TestSubType Qbit Qbit where subType x = x

instance (TestSubType a b, FlagSubType f f2) => 
               TestSubType (Flag f a) (Flag f2 b) where
    subType (Flag x) = Flag (subType x)

instance (TestSubType c a, TestSubType b d) => 
                  TestSubType (a -> b) (c -> d) where
    subType f = \x -> subType (f (subType x))

instance (TestSubType a c, TestSubType b d) => 
                  TestSubType (a, b) (c, d) where
    subType (a,b) = (subType a, subType b)





class AddVar x a c2 c1 | x a c1 -> c2 where
   add :: x -> a -> c2 -> c1

instance AddVar n a () () where
   add n a () = ()

instance a1 ~ a2 => AddVar Z a1 (Free b,c) (Free a2,c) where
   add Z a (Free b,c) = (Free a, c)

instance a1 ~ a2 => AddVar Z a1 (Free b,c) (Used a2,c) where
   add Z a (Free b,c) = (Used a, c)

instance (AddVar n a c d) => AddVar (S n) a (b,c) (b,d) where
   add (S n) a (b,c) = (b,add n a c)



class IsNotEq a b
instance IsNotEq Z (S n)
instance IsNotEq (S n) Z
instance IsNotEq m n => IsNotEq (S m) (S n)

class Add2Var x a y b c2 c1 | x a y b c1 -> c2 where
   add2 :: x -> a -> y -> b -> c2 -> c1

instance (IsNotEq m n) => Add2Var m a n b () () where
   add2 x a y b () = ()

instance (IsNotEq Z Z) => Add2Var Z a Z b c c where
   add2 x a y b c = c

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var Z a1 (S m) b (Free y, c2) (Free a2, c1) where
   add2 Z a (S y) b (Free dummy, c2) = (Free a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var (S m) b Z a1 (Free y, c2) (Free a2, c1) where
   add2 (S y) b Z a (Free dummy, c2) = (Free a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var Z a1 (S m) b (Free y, c2) (Used a2, c1) where
   add2 Z a (S y) b (Free dummy, c2) = (Used a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var (S m) b Z a1 (Free y, c2) (Used a2, c1) where
   add2 (S y) b Z a (Free dummy, c2) = (Used a, add y b c2)

instance (Add2Var n a m b c d) => Add2Var (S n) a (S m) b (y,c) (y,d) where
   add2 (S n) a (S m) b (y,c) = (y,add2 n a m b c)





class GetVar x a c | x a -> c where
  get_var :: c -> x -> a

instance TestSubType a b => GetVar Z b (Used a,()) where
  get_var (Used a,c) Z = subType a

instance GetVar n a c => GetVar (S n) a (Free u,c) where
  get_var (u,c) (S n) = get_var c n



class Zip c1 c2 c3 | c1 c2 -> c3 where
   split :: c3 -> (c1,c2)
instance Zip () c c where
   split c = ((),c)
instance Zip c () c where
   split c = (c,())
instance Zip () () () where
   split () = ((),())

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Free a, c1) (Free b, c2) (Free c, c3) where
   split (Free c,c3) = let (c1,c2) = split c3 in ((Free c,c1),(Free c,c2))

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Free a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Free c,c1),(Used c,c2))

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Used a, c1) (Free b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used c,c1),(Free c,c2))

instance (Zip c1 c2 c3, (Flag Dup d) ~ c, c ~ a, c ~ b) => Zip (Used a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used c,c1),(Used c,c2))



class Match c1 c2 c3 | c1 c2 -> c3 where
   match :: c3 -> (c1,c2)
instance Match () c c where
   match c = ((),c)
instance Match c () c where
   match c = (c,())
instance Match () () () where
   match () = ((),())

instance (Match c1 c2 c3, c ~ a, c ~ b) => 
   Match (Free a, c1) (Free b, c2) (Free c, c3)
   where
   match (Free c,c3) = 
     let (c1,c2) = match c3 in 
     ((Free c,c1),(Free c,c2))
instance (Match c1 c2 c3, c ~ a, c ~ b) => 
   Match (Used a, c1) (Used b, c2) (Used c, c3)
   where
   match (Used c,c3) = 
     let (c1,c2) = match c3 in
     ((Used c,c1),(Used c,c2))





-- If the context contains a Sim-flagged type at some ConsYes place,
-- then d is Sim. Otherwise, it is Dup

class TestCont1 cont d | cont -> d
instance TestCont1 () Dup
instance (TestCont1 c f) => TestCont1 (Used (Flag Dup a), c) f
instance                    TestCont1 (Used (Flag Sim a), c) Sim
instance (TestCont1 c f) => TestCont1 (Free a, c) f

-- This relation states that if we have Dup as result, then all the
-- flags are Dup. If we have Sim, we cannot get any other information.

class TestCont2 c f
instance TestCont2 () Dup
instance (TestCont2 c Dup, (Flag Dup a) ~ b) => TestCont2 (Used b, c) Dup
instance (TestCont2 c Dup) => TestCont2 (Free b, c) Dup
instance TestCont2 c Sim

class TestCont c d
instance (TestCont1 c d, TestCont2 c d) => TestCont c d



class Or1 e a x | e a -> x
instance Or1 e Dup Dup
instance Or1 Dup e Dup
instance Or1 Sim Sim Sim
instance Or1 Dup Dup Dup
instance (a ~ b) => Or1 Sim a b
instance (a ~ b) => Or1 a Sim b

class Or2 e a x | x -> e a
instance Or2 Sim Sim Sim
instance Or2 e a Dup

class Or e a x
instance (Or1 e a x, Or2 e a x) => Or e a x 





-- The class of typing judgments!

class Judg j where
      lamb :: (AddVar x a c2 c1, TestCont c2 f1, FlagSubType f1 f) => x -> j w c1 b -> j (w,f1,f) c2 (Flag f (a -> b))
      appl :: Zip c1 c2 c3 => j w1 c1 (Flag d (a -> b)) -> j w2 c2 a -> j (w1,w2,d,a) c3 b
      var :: (GetVar x a c) => x -> j () c a
      tt :: j f () (Flag f Bool)
      ff :: j f () (Flag f Bool)
      ifx :: (Match c21 c22 c2, Zip c1 c2 c3) => j w1 c1 (Flag d Bool) -> j w2 c21 a -> j w3 c22 a -> j (w1,w2,w3,d) c3 a
      tens :: (Zip c1 c2 c3, Or e xa x, Or e yb y) => j w1 c1 (Flag x a) -> j w2 c2 (Flag y b) -> j (w1,w2,e,xa,x,yb,y) c3 (Flag e (Flag xa a, Flag yb b))
      new :: j w c (Flag f Bool) -> j (w,f) c (Flag Sim Qbit)
      meas ::  j w c (Flag f Qbit) -> j (w,f,f') c (Flag f' Bool)
      had :: j w c (Flag f Qbit) -> 
             j (w,f) c (Flag Sim Qbit)
      qnot :: j w c (Flag f Qbit) -> j (w,f) c (Flag Sim Qbit)
      not2 :: j w c (Flag f Qbit) -> j (w,f) c (Flag Sim Qbit)
      id2 :: j w c (Flag f Qbit) -> j (w,f) c (Flag Sim Qbit)
      cnot :: j w c (Flag f1 (Flag f2 Qbit,   Flag f3 Qbit)) -> 
              j (w,f1,f2,f3) c (Flag Sim (Flag Sim Qbit, Flag Sim Qbit))

-- separating this one is necessary to expose the types x, a, y and b.
class JudgTens j x a y b where
      lambtens :: (TestCont c3 f1, FlagSubType f1 f, Add2Var n (Flag x a) m (Flag y b) c3 c1, Or e xa x, Or e yb y) => 
        n -> m -> j w c1 d -> j (w,f1,f,e,xa,x,a,yb,y,b) c3 (Flag f ((Flag e (Flag xa a, Flag yb b)) -> d))

lettens x y m n = appl (lambtens x y n) m
letx x m n = appl (lamb x n) m




-- Concrete instance of judgments

data J w c a = J (c -> a)


instance Judg J where
      lamb x (J f) = J (\c -> Flag ((\a -> f (add x a c))))
      appl (J f) (J g) = J (\x -> let (x1,x2) = split x in let (Flag h) = f x1 in h (g x2))
      var x = J (\z -> get_var z x)
      tt = J $ \x -> Flag True
      ff = J $ \x -> Flag False
      ifx (J b) (J m) (J n) = J (\x -> let (x1,x2) = split x in let (x21,x22) = match x2 in let (Flag bb) = b x1 in
                                  if bb then (m x21) else (n x22))
      tens (J f) (J g) = J (\x -> let (x1,x2) = split x in let (Flag a) = f x1 in let (Flag b) = g x2 in (Flag (Flag a, Flag b)))
      new (J f) = J $ \x -> let (Flag y) = f x in Flag (Qbit y)
      meas (J f) = J $ \x -> let (Flag (Qbit y)) = f x in Flag y
      had (J f) = J $ \x -> let (Flag q) = f x in Flag q
      qnot (J f) = J $ \x -> let (Flag q) = f x in Flag q
      not2 (J f) = J $ \x -> let (Flag q) = f x in Flag q
      id2 (J f) = J $ \x -> let (Flag q) = f x in Flag q
      cnot (J f) = J $ \x -> let (Flag (Flag a, Flag b)) = f x in (Flag (Flag a, Flag b))

instance JudgTens J x a y b where
      lambtens n m (J f) = J (\c -> Flag ((\(Flag (Flag a, Flag b) :: (Flag e (Flag xa a, Flag yb b))) -> f (add2 n ((Flag a)::Flag x a) m ((Flag b)::Flag y b) c))))



-- Evaluation

data E w a = E a

class Eval c a where
   eval :: (J w c a) -> E w a

instance Eval () a where
   eval (J f) = E (f ())

instance (Eval c a, (Free Dummy) ~ b) => Eval (b,c) a where
   eval (J f) = eval (J (\c -> f (Free Dummy, c)))


setType :: E w a -> a -> E w a
setType x y = x

setJudg :: J w c a -> c -> a -> J w c a
setJudg x y z = x




-- We can also write the teleportation algorithm as specified in
-- [Selinger-Valiron]


x = Z
y = S Z
z = S (S Z)
t = S (S (S Z))

epr = lamb x (cnot (tens (had (new ff)) (new ff)))

bellmeasure =
    lamb x (
    lamb y (
    lettens z t 
      (cnot (tens (var x)
                  (var y))) 
      (tens (meas (had (var z)))
            (meas (var t)))))

ucorrection = 
    lamb z (
    lambtens x y (
        ifx (var x) (ifx (var y) (not2 (var z)) (id2 (var z))) 
                    (ifx (var y) (qnot (var z)) (var z))))

telep =
  lettens x y (appl epr ff) (
  letx z (appl bellmeasure (var x)) (
  letx t (appl ucorrection (var y)) (
  (lamb x (appl (var t) (appl (var z) (var x)))))))



{- trying to duplicate it fails, as hoped for

:t appl (lamb Z (tens (var Z) (var Z))) telep
==> Couldn't match type `Sim' with `Dup'

-}



{- It has the type specified in [Selinger-Valiron]:

eval telep
  :: (Or2 Sim f11 f11, Or2 f1 f5 y1, Or2 f1 f3 x, Or2 e xa f13,
      Or2 e yb f12, Or1 f1 f5 y1, Or1 f1 f3 x, Or1 e xa f13,
      Or1 e yb f12, FlagSubType f10 f11, FlagSubType f6 f10,
      FlagSubType f7 f6, FlagSubType f e, FlagSubType f4 yb,
      FlagSubType f5 f4, FlagSubType f2 xa, FlagSubType f3 f2,
      FlagSubType f1 f, FlagSubType f12 d7, FlagSubType f13 d5,
      FlagSubType f12 d6) =>
     E ... 
       (Flag Sim (Flag f7 Qbit -> Flag Sim Qbit))

-}