From bbb13137be582a26d19c03471971e59463ddf7c8 Mon Sep 17 00:00:00 2001 From: Riley Evans Date: Mon, 12 Jul 2021 12:52:57 +0100 Subject: [PATCH 1/5] Add replicateInputs function --- circuitflow.cabal | 1 + src/Pipeline/Circuit.hs | 39 ++++++++++++++++++++++-- src/Pipeline/Internal/Common/TypeList.hs | 4 +++ tests/Pipeline/Network/MinimalTests.hs | 25 ++++++++++++++- 4 files changed, 65 insertions(+), 4 deletions(-) diff --git a/circuitflow.cabal b/circuitflow.cabal index 6ee33b6..c785664 100644 --- a/circuitflow.cabal +++ b/circuitflow.cabal @@ -73,6 +73,7 @@ library , directory hs-source-dirs: src default-language: Haskell2010 + ghc-options: -fprint-potential-instances test-suite test default-language: Haskell2010 diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index 615b34f..ec5b23d 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -8,6 +8,8 @@ Maintainer : haskell@rly.rocks This package contains all the constructors needed to build a 'Circuit'. -} + +{-# LANGUAGE UndecidableInstances #-} module Pipeline.Circuit ( -- * Main Type @@ -23,6 +25,7 @@ module Pipeline.Circuit , dropL , dropR , mapC + , replicateInputs ) where @@ -31,7 +34,7 @@ import Pipeline.Internal.Common.IFunctor.Modular ((:<:) (..)) import Pipeline.Internal.Common.Nat (IsNat, N1, N2, Nat (..), SNat (..), (:+)) import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, - Take, Replicate, (:++)) + Take, Replicate, Duplicate, (:++)) import qualified Pipeline.Internal.Core.CircuitAST as AST import Pipeline.Internal.Core.DataStore (DataStore, DataStore', Var) @@ -169,5 +172,35 @@ instance (DataStore f a, Eq a, Eq (f a)) => ReplicateN ('Succ ('Succ 'Zero)) f a instance (DataStore f a, Eq a, Eq (f a)) => ReplicateN ('Succ ('Succ ('Succ 'Zero))) f a where replicateN (SSucc n) = replicate2 <-> id <> replicateN n -replicateMany :: SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m -replicateMany = undefined + +class (DataStore' fs as) => ReplicateInputs m fs as where + replicateInputs :: ( Length fs ~ m + , Length as ~ m + , Length (Duplicate fs) ~ Length (Duplicate as) + , ('Succ 'Zero :+ m) ~ 'Succ m + , IsNat m + ) => SNat m -> AST.Circuit fs as (Duplicate fs) (Duplicate as) m + +instance (DataStore f a, Eq a, Eq (f a)) => ReplicateInputs ('Succ 'Zero) '[f] '[a] where + replicateInputs (SSucc SZero) = replicate2 + +instance ( DataStore f a + , DataStore' fs as + , DataStore' (Duplicate fs) (Duplicate as) + , ReplicateInputs ('Succ n) fs as + , Length fs ~ 'Succ n + , IsNat n + , Eq a + , Eq (f a) + ) => ReplicateInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where + replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) +-- replicateMany :: SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m +-- replicateMany n = undefined +-- where +-- replicateInputs :: ( m ~ Length fs +-- , m ~ Length as +-- , m ~ Length (Apply fs as) +-- , m ~ 'Succ n +-- ) => SNat m -> AST.Circuit fs as (Duplicate fs) (Duplicate as) m +-- replicateInputs (SSucc SZero) = replicate2 +-- replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) diff --git a/src/Pipeline/Internal/Common/TypeList.hs b/src/Pipeline/Internal/Common/TypeList.hs index 3a210b7..0a4e0e1 100644 --- a/src/Pipeline/Internal/Common/TypeList.hs +++ b/src/Pipeline/Internal/Common/TypeList.hs @@ -33,3 +33,7 @@ type family Apply (fs :: [Type -> Type]) (as :: [Type]) where type family Replicate (n :: Nat) (a :: k) :: [k] where Replicate 'Zero _ = '[] Replicate ('Succ n) x = x ': Replicate n x + +type family Duplicate (a :: [k]) :: [k] where + Duplicate '[] = '[] + Duplicate (x ': xs) = x ': x ': Duplicate xs diff --git a/tests/Pipeline/Network/MinimalTests.hs b/tests/Pipeline/Network/MinimalTests.hs index c8d9102..3d62379 100644 --- a/tests/Pipeline/Network/MinimalTests.hs +++ b/tests/Pipeline/Network/MinimalTests.hs @@ -25,6 +25,7 @@ minimalTests = testGroup "Minimal Examples" [ idTests , replicate2Tests + , replicate3Tests , thenTests , besideTests , swapTests @@ -33,6 +34,7 @@ minimalTests = testGroup , functionTaskTests , multiInputTaskTests , mapTests + , replicateInputsTests ] @@ -84,7 +86,7 @@ replicate2Tests = testGroup out <- fetch' o out @?= HCons 0 (HCons 0 HNil) ] - + replicate3Circuit :: Circuit '[Var] @@ -104,6 +106,27 @@ replicate3Tests = testGroup out <- fetch' o out @?= HCons 0 (HCons 0 (HCons 0 HNil)) ] + + +replicateInputsCircuit + :: Circuit + '[VariableStore, VariableStore] + '[Int, Int] + '[VariableStore Int, VariableStore Int] + '[VariableStore , VariableStore , VariableStore, VariableStore] + '[Int , Int , Int, Int] + '[VariableStore Int , VariableStore Int , VariableStore Int, VariableStore Int] + N2 +replicateInputsCircuit = replicateInputs (SSucc (SSucc SZero)) + +replicateInputsTests :: TestTree +replicateInputsTests = testGroup + "(replicateN 3) should" + [ testCase "return a trupled input value" $ do + let i = HCons' (Var 0) (HCons' (Var 2) HNil') + o <- singleInputTest replicateInputsCircuit i + o @?= Right (HCons' (Var 0) (HCons' (Var 0) (HCons' (Var 2) (HCons' (Var 2) HNil')))) + ] -- Tests for the 'Then' constructor thenCircuit From 8fe142f1659f0a98220dd76193dc532a6463e445 Mon Sep 17 00:00:00 2001 From: Riley Evans Date: Wed, 14 Jul 2021 15:59:59 +0100 Subject: [PATCH 2/5] Bit stuck --- circuitflow.cabal | 2 +- src/Pipeline/Circuit.hs | 78 ++++++++++++++++++++---- src/Pipeline/Internal/Common/TypeList.hs | 28 +++++++++ 3 files changed, 96 insertions(+), 12 deletions(-) diff --git a/circuitflow.cabal b/circuitflow.cabal index c785664..af844df 100644 --- a/circuitflow.cabal +++ b/circuitflow.cabal @@ -73,7 +73,7 @@ library , directory hs-source-dirs: src default-language: Haskell2010 - ghc-options: -fprint-potential-instances + ghc-options: -fprint-potential-instances -freduction-depth=201 test-suite test default-language: Haskell2010 diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index ec5b23d..41ea66b 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -33,7 +33,7 @@ import Pipeline.Internal.Common.IFunctor (IFix5 (..)) import Pipeline.Internal.Common.IFunctor.Modular ((:<:) (..)) import Pipeline.Internal.Common.Nat (IsNat, N1, N2, Nat (..), SNat (..), (:+)) -import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, +import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, Swap, Pair, Transpose, Concat, Take, Replicate, Duplicate, (:++)) import qualified Pipeline.Internal.Core.CircuitAST as AST import Pipeline.Internal.Core.DataStore (DataStore, @@ -194,13 +194,69 @@ instance ( DataStore f a , Eq (f a) ) => ReplicateInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) --- replicateMany :: SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m --- replicateMany n = undefined --- where --- replicateInputs :: ( m ~ Length fs --- , m ~ Length as --- , m ~ Length (Apply fs as) --- , m ~ 'Succ n --- ) => SNat m -> AST.Circuit fs as (Duplicate fs) (Duplicate as) m --- replicateInputs (SSucc SZero) = replicate2 --- replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) + + +class DataStore' fs as => OrganiseInputs m fs as where + organiseInputs :: SNat m + -> AST.Circuit fs + as + (Concat (Transpose (Pair fs))) + (Concat (Transpose (Pair as))) + (Length fs) + +instance (DataStore f a, DataStore g b, Eq a, Eq (f a), Eq b, Eq (g b)) => OrganiseInputs ('Succ 'Zero) '[f, g] '[a, b] where + organiseInputs (SSucc SZero) = id <> id + +instance (DataStore f a, DataStore' fs as, Eq a, Eq (f a)) => OrganiseInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where + organiseInputs = undefined -- Stuck here + + +class DataStore' fs as => SwapInputs n fs as where + swapInputs :: SNat n -> AST.Circuit fs as (Swap n fs) (Swap n as) (Length fs) + +instance (DataStore f a, DataStore g b, Eq b, Eq (g b), Eq a, Eq (f a)) => SwapInputs ('Succ 'Zero) '[f, g] '[a, b] where + swapInputs (SSucc SZero) = swap + +instance ( DataStore f a + , DataStore g b + , SwapInputs ('Succ n) hs cs + , Length hs ~ Length cs + , Length (Swap ('Succ n) hs) ~ Length (Swap ('Succ n) cs) + , (N2 :+ Length cs) ~ 'Succ ('Succ (Length cs)) + , (DataStore' (Swap ('Succ n) hs) (Swap ('Succ n) cs)) + , IsNat (Length cs) + , Eq b, Eq (g b) + , Eq a, Eq (f a) + ) => SwapInputs ('Succ ('Succ n)) (f ': g ': hs) (a ': b ': cs) where + swapInputs (SSucc n) = swap <> swapInputs n + +replicateMany :: ( 'Succ 'Zero :+ m ~ 'Succ m + , Length fs ~ m + , Length as ~ m + , Length (Apply fs as) ~ m + , Length (Duplicate fs) ~ Length (Duplicate as) + , Length (Duplicate fs) ~ Length (Apply (Duplicate fs) (Duplicate as)) + , (as :++ as) ~ Concat (Transpose (Pair (Duplicate as))) + , (fs :++ fs) ~ Concat (Transpose (Pair (Duplicate fs))) + , ReplicateInputs m fs as + , OrganiseInputs m (Duplicate fs) (Duplicate as) + , IsNat m + , DataStore' (Duplicate fs) (Duplicate as) + , DataStore' fs as + , DataStore' (Concat (Transpose (Pair (Duplicate fs)))) (Concat (Transpose (Pair (Duplicate as)))) + ) => SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m +replicateMany n = replicateInputs n + <-> + organiseInputs n + -- where + -- organiseInputs :: SNat n + -- -> AST.Circuit fs + -- as + -- (Apply fs as) + -- (Concat (Transpose (Pair fs))) + -- (Concat (Transpose (Pair as))) + -- (Apply (Concat (Transpose (Pair fs))) (Concat (Transpose (Pair as)))) + -- (Length fs) + -- organiseInputs (SSucc SZero) = id <> id + -- organiseInputs (SSucc n) = (id <> swapInputs n <> id + -- <-> id <> organiseInputs n <> id) diff --git a/src/Pipeline/Internal/Common/TypeList.hs b/src/Pipeline/Internal/Common/TypeList.hs index 0a4e0e1..0e7ecc3 100644 --- a/src/Pipeline/Internal/Common/TypeList.hs +++ b/src/Pipeline/Internal/Common/TypeList.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE UndecidableInstances #-} module Pipeline.Internal.Common.TypeList where import Pipeline.Internal.Common.Nat (Nat (..)) @@ -37,3 +38,30 @@ type family Replicate (n :: Nat) (a :: k) :: [k] where type family Duplicate (a :: [k]) :: [k] where Duplicate '[] = '[] Duplicate (x ': xs) = x ': x ': Duplicate xs + +type family Swap (n :: Nat) (a :: [k]) :: [k] where + Swap n '[] = '[] + Swap 'Zero l = l + Swap ('Succ n) (x ': y ': xs) = y ': x ': Swap n xs + + +type family Pair (xs :: [k]) :: [[k]] where + Pair '[] = '[] + Pair (x ': y ': xs) = '[x, y] ': Pair xs + +type family Concat (xss :: [[k]]) :: [k] where + Concat '[] = '[] + Concat ('[] ': l) = Concat l + Concat ((x ': xs) ': l) = x ': Concat (xs ': l) + +type family Transpose (xss :: [[k]]) :: [[k]] where + Transpose ('[] ': _) = '[] + Transpose xss = Heads xss ': Transpose (Tails xss) + +type family Heads (xss :: [[k]]) :: [k] where + Heads '[] = '[] + Heads ((x ': xs) ': xss) = x ': Heads xss + +type family Tails (xss :: [[k]]) :: [[k]] where + Tails '[] = '[] + Tails ((x ': xs) ': xss) = xs ': Tails xss From 9db28bf10128871ec26119dfbb0fb438e2272743 Mon Sep 17 00:00:00 2001 From: Riley Evans Date: Wed, 14 Jul 2021 16:03:43 +0100 Subject: [PATCH 3/5] Comments --- src/Pipeline/Circuit.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index 41ea66b..4130513 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -207,6 +207,11 @@ class DataStore' fs as => OrganiseInputs m fs as where instance (DataStore f a, DataStore g b, Eq a, Eq (f a), Eq b, Eq (g b)) => OrganiseInputs ('Succ 'Zero) '[f, g] '[a, b] where organiseInputs (SSucc SZero) = id <> id + +-- Problem with the type as I need it to be something like f ': fs ': '[g] +-- function peels one off each end of the list, which can't do with Haskell list! +-- Any other way to write a function that does the same thing...? +-- Currently its 'centre-recursive', a tail-recursive function would probably avoid the problem instance (DataStore f a, DataStore' fs as, Eq a, Eq (f a)) => OrganiseInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where organiseInputs = undefined -- Stuck here From d80ba802d71094a77cba2fa4ea1053cb81488dd9 Mon Sep 17 00:00:00 2001 From: Riley Evans Date: Tue, 31 Aug 2021 12:45:59 +0100 Subject: [PATCH 4/5] Update tests to latest changes --- src/Pipeline/Circuit.hs | 1 - tests/Pipeline/Network/MinimalTests.hs | 19 ++++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index 4130513..56b312b 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -240,7 +240,6 @@ replicateMany :: ( 'Succ 'Zero :+ m ~ 'Succ m , Length as ~ m , Length (Apply fs as) ~ m , Length (Duplicate fs) ~ Length (Duplicate as) - , Length (Duplicate fs) ~ Length (Apply (Duplicate fs) (Duplicate as)) , (as :++ as) ~ Concat (Transpose (Pair (Duplicate as))) , (fs :++ fs) ~ Concat (Transpose (Pair (Duplicate fs))) , ReplicateInputs m fs as diff --git a/tests/Pipeline/Network/MinimalTests.hs b/tests/Pipeline/Network/MinimalTests.hs index 3d62379..e67ef3a 100644 --- a/tests/Pipeline/Network/MinimalTests.hs +++ b/tests/Pipeline/Network/MinimalTests.hs @@ -110,12 +110,10 @@ replicate3Tests = testGroup replicateInputsCircuit :: Circuit - '[VariableStore, VariableStore] - '[Int, Int] - '[VariableStore Int, VariableStore Int] - '[VariableStore , VariableStore , VariableStore, VariableStore] - '[Int , Int , Int, Int] - '[VariableStore Int , VariableStore Int , VariableStore Int, VariableStore Int] + '[Var , Var] + '[Int , Int] + '[Var , Var , Var , Var] + '[Int , Int , Int , Int] N2 replicateInputsCircuit = replicateInputs (SSucc (SSucc SZero)) @@ -123,9 +121,12 @@ replicateInputsTests :: TestTree replicateInputsTests = testGroup "(replicateN 3) should" [ testCase "return a trupled input value" $ do - let i = HCons' (Var 0) (HCons' (Var 2) HNil') - o <- singleInputTest replicateInputsCircuit i - o @?= Right (HCons' (Var 0) (HCons' (Var 0) (HCons' (Var 2) (HCons' (Var 2) HNil')))) + var1 <- varWith 0 + var2 <- varWith 2 + let i = HCons' var1 (HCons' var2 HNil') + (Right o) <- singleInputTest replicateInputsCircuit i + out <- fetch' o + out @?= HCons 0 (HCons 0 (HCons 2 (HCons 2 HNil))) ] -- Tests for the 'Then' constructor From 5aa95d44cd20bc72b0930de101dd803d6ca7d3f0 Mon Sep 17 00:00:00 2001 From: Riley Evans Date: Wed, 10 Nov 2021 20:41:26 +0000 Subject: [PATCH 5/5] wip --- src/Pipeline/Circuit.hs | 24 ++++++++++-------------- src/Pipeline/Internal/Core/CircuitAST.hs | 11 +++++++++-- 2 files changed, 19 insertions(+), 16 deletions(-) diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index 56b312b..4e29418 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -195,7 +195,6 @@ instance ( DataStore f a ) => ReplicateInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) - class DataStore' fs as => OrganiseInputs m fs as where organiseInputs :: SNat m -> AST.Circuit fs @@ -207,14 +206,22 @@ class DataStore' fs as => OrganiseInputs m fs as where instance (DataStore f a, DataStore g b, Eq a, Eq (f a), Eq b, Eq (g b)) => OrganiseInputs ('Succ 'Zero) '[f, g] '[a, b] where organiseInputs (SSucc SZero) = id <> id - --- Problem with the type as I need it to be something like f ': fs ': '[g] +-- Problem with the type as I need it to be something like f ': (fs :++ '[g]) -- function peels one off each end of the list, which can't do with Haskell list! -- Any other way to write a function that does the same thing...? -- Currently its 'centre-recursive', a tail-recursive function would probably avoid the problem instance (DataStore f a, DataStore' fs as, Eq a, Eq (f a)) => OrganiseInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where organiseInputs = undefined -- Stuck here +-- organiseInputs :: (DataStore' fs as) => SNat n +-- -> AST.Circuit fs +-- as +-- (Concat (Transpose (Pair fs))) +-- (Concat (Transpose (Pair as))) +-- (Length fs) +-- organiseInputs (SSucc SZero) = id <> id +-- organiseInputs (SSucc n) = (id <> swapInputs n <> id +-- <-> id <> organiseInputs n <> id) class DataStore' fs as => SwapInputs n fs as where swapInputs :: SNat n -> AST.Circuit fs as (Swap n fs) (Swap n as) (Length fs) @@ -253,14 +260,3 @@ replicateMany n = replicateInputs n <-> organiseInputs n -- where - -- organiseInputs :: SNat n - -- -> AST.Circuit fs - -- as - -- (Apply fs as) - -- (Concat (Transpose (Pair fs))) - -- (Concat (Transpose (Pair as))) - -- (Apply (Concat (Transpose (Pair fs))) (Concat (Transpose (Pair as)))) - -- (Length fs) - -- organiseInputs (SSucc SZero) = id <> id - -- organiseInputs (SSucc n) = (id <> swapInputs n <> id - -- <-> id <> organiseInputs n <> id) diff --git a/src/Pipeline/Internal/Core/CircuitAST.hs b/src/Pipeline/Internal/Core/CircuitAST.hs index 6e5604b..c57fc81 100644 --- a/src/Pipeline/Internal/Core/CircuitAST.hs +++ b/src/Pipeline/Internal/Core/CircuitAST.hs @@ -23,8 +23,8 @@ import Pipeline.Internal.Common.IFunctor (IFix5 (..), import Pipeline.Internal.Common.IFunctor.Modular ((:+:) (..)) import Pipeline.Internal.Common.Nat (IsNat (..), N1, N2, Nat (..), (:+), - (:=)) -import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, + (:=), SNat (..)) +import Pipeline.Internal.Common.TypeList (Drop, Length, Take, (:++)) import Pipeline.Internal.Core.DataStore (DataStore, DataStore', Var) @@ -42,6 +42,13 @@ data Replicate (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Na Replicate ::(DataStore' '[f] '[a]) => Replicate iF '[f] '[a] [f, f] '[a, a] N1 +data ReplicateManyN (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Nat -> Type) + (inputsS :: [Type -> Type]) (inputsT :: [Type]) + (outputsS :: [Type -> Type]) (outputsT :: [Type]) (ninputs :: Nat) where + ReplicateManyN ::(DataStore' '[f] '[a]) + => SNat n -> SNat m -> ReplicateManyN iF '[f] '[a] [f, f] '[a, a] N1 + + data Then (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Nat -> Type) (inputsS :: [Type -> Type]) (inputsT :: [Type]) (outputsS :: [Type -> Type]) (outputsT :: [Type]) (ninputs :: Nat) where