From e69ed7aa24d26b663e4b76dec13650595b9ac93e Mon Sep 17 00:00:00 2001 From: csicar Date: Sat, 4 Dec 2021 22:26:26 +0100 Subject: [PATCH 1/7] Add Mirror and Snoc type classes to Symbol --- src/Type/Data/Symbol.purs | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/src/Type/Data/Symbol.purs b/src/Type/Data/Symbol.purs index 8ff8564..534406c 100644 --- a/src/Type/Data/Symbol.purs +++ b/src/Type/Data/Symbol.purs @@ -5,6 +5,11 @@ module Type.Data.Symbol , compare , uncons , class Equals + , class Mirror + , class MirrorP + , mirror + , class Snoc + , snoc , equals ) where @@ -33,3 +38,36 @@ instance equalsSymbol equals :: forall proxy l r o. Equals l r o => proxy l -> proxy r -> Proxy o equals _ _ = Proxy + + +-- Mirror + +class MirrorP (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a + +instance mirrorEmpty :: MirrorP "" "" +else +instance mirrorCons :: (Cons head tail sym, MirrorP tailMirror tail, MirrorP tail tailMirror, Append tailMirror head mirror) => MirrorP sym mirror + +class Mirror (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a + +instance mirrorMirrorP :: (MirrorP a b, MirrorP b a) => Mirror a b + +mirror :: ∀a b. Mirror a b => SProxy a -> SProxy b +mirror _ = SProxy + +-- Snoc + +--| ```purescript +--| Snoc "symbo" "l" ?x ~~> ?x = "symbol" +--| Snoc ?a ?b "symbol" ~~> ?a = "symbo", ?b = "l" +--| ``` +-- | `end` must be a single character +class Snoc (list :: Symbol) (end :: Symbol) (symbol :: Symbol) | end list -> symbol, symbol -> end list + +instance snocMirror :: (Mirror sym mirror, Cons end listMirror mirror, Mirror listMirror list) => Snoc list end sym + +--| ```purescript +--| snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") = SProxy :: SProxy "symbol" +--| ``` +snoc :: ∀a b c. Snoc a b c => SProxy a -> SProxy b -> SProxy c +snoc _ _ = SProxy From a3f971420c05796055eba8bc8e42c899b6bd1004 Mon Sep 17 00:00:00 2001 From: csicar Date: Sat, 4 Dec 2021 22:30:50 +0100 Subject: [PATCH 2/7] Add tests --- test/Main.purs | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test/Main.purs diff --git a/test/Main.purs b/test/Main.purs new file mode 100644 index 0000000..9fede0c --- /dev/null +++ b/test/Main.purs @@ -0,0 +1,38 @@ +module Test.Main where + +import Prelude + +import Effect (Effect) +import Effect.Class.Console (log) +import Type.Data.Symbol (SProxy(..), mirror, snoc) + +-- mirror +testMirror :: SProxy "lobmys" +testMirror = mirror (SProxy::_ "symbol") + +testMirror1 :: SProxy _ +testMirror1 = mirror (SProxy::_ "symbol") + +testMirror2 :: SProxy "lobmyys" +testMirror2 = mirror (SProxy :: SProxy _) + +-- snoc +testSnoc :: SProxy "symbol" +testSnoc = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") + +testSnoc1 :: SProxy _ +testSnoc1 = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") + +testSnoc2 :: SProxy "symbol" +testSnoc2 = snoc (SProxy :: SProxy _) (SProxy :: SProxy "l") + +testSnoc3 :: SProxy "symbol" +testSnoc3 = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy _) + +testSnoc4 :: SProxy "s" +testSnoc4 = snoc (SProxy :: SProxy "") (SProxy :: SProxy "s") + + +main :: Effect Unit +main = do + log "asd" \ No newline at end of file From ef01738d414070dbd5c3af1d852d3c2374451d00 Mon Sep 17 00:00:00 2001 From: csicar Date: Sat, 4 Dec 2021 22:59:22 +0100 Subject: [PATCH 3/7] Remove deprecated `SProxy` uses --- src/Type/Data/Symbol.purs | 34 ++++++++++++++++++++-------------- test/Main.purs | 35 ++++++++++++++++++----------------- 2 files changed, 38 insertions(+), 31 deletions(-) diff --git a/src/Type/Data/Symbol.purs b/src/Type/Data/Symbol.purs index 534406c..e489ff1 100644 --- a/src/Type/Data/Symbol.purs +++ b/src/Type/Data/Symbol.purs @@ -1,17 +1,18 @@ module Type.Data.Symbol - ( module Prim.Symbol - , module Data.Symbol - , append - , compare - , uncons + ( append , class Equals , class Mirror , class MirrorP - , mirror , class Snoc - , snoc + , compare , equals - ) where + , mirror + , module Data.Symbol + , module Prim.Symbol + , snoc + , uncons + ) + where import Prim.Symbol (class Append, class Compare, class Cons) import Data.Symbol (SProxy(..), class IsSymbol, reflectSymbol, reifySymbol) @@ -46,14 +47,19 @@ class MirrorP (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a instance mirrorEmpty :: MirrorP "" "" else -instance mirrorCons :: (Cons head tail sym, MirrorP tailMirror tail, MirrorP tail tailMirror, Append tailMirror head mirror) => MirrorP sym mirror +instance mirrorCons :: + ( Cons head tail sym + , MirrorP tailMirror tail + , MirrorP tail tailMirror + , Append tailMirror head mirror + ) => MirrorP sym mirror class Mirror (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a instance mirrorMirrorP :: (MirrorP a b, MirrorP b a) => Mirror a b -mirror :: ∀a b. Mirror a b => SProxy a -> SProxy b -mirror _ = SProxy +mirror :: ∀ proxy a b. Mirror a b => proxy a -> Proxy b +mirror _ = Proxy -- Snoc @@ -67,7 +73,7 @@ class Snoc (list :: Symbol) (end :: Symbol) (symbol :: Symbol) | end list -> sym instance snocMirror :: (Mirror sym mirror, Cons end listMirror mirror, Mirror listMirror list) => Snoc list end sym --| ```purescript ---| snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") = SProxy :: SProxy "symbol" +--| snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") = Proxy :: Proxy "symbol" --| ``` -snoc :: ∀a b c. Snoc a b c => SProxy a -> SProxy b -> SProxy c -snoc _ _ = SProxy +snoc :: ∀a b c. Snoc a b c => Proxy a -> Proxy b -> Proxy c +snoc _ _ = Proxy diff --git a/test/Main.purs b/test/Main.purs index 9fede0c..25436ac 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -4,33 +4,34 @@ import Prelude import Effect (Effect) import Effect.Class.Console (log) -import Type.Data.Symbol (SProxy(..), mirror, snoc) +import Type.Data.Symbol (mirror, reifySymbol, snoc) +import Type.Proxy (Proxy(..)) -- mirror -testMirror :: SProxy "lobmys" -testMirror = mirror (SProxy::_ "symbol") +testMirror :: Proxy "lobmys" +testMirror = mirror (Proxy::_ "symbol") -testMirror1 :: SProxy _ -testMirror1 = mirror (SProxy::_ "symbol") +testMirror1 :: Proxy _ +testMirror1 = mirror (Proxy::_ "symbol") -testMirror2 :: SProxy "lobmyys" -testMirror2 = mirror (SProxy :: SProxy _) +testMirror2 :: Proxy "lobmyys" +testMirror2 = mirror (Proxy :: Proxy _) -- snoc -testSnoc :: SProxy "symbol" -testSnoc = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") +testSnoc :: Proxy "symbol" +testSnoc = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") -testSnoc1 :: SProxy _ -testSnoc1 = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy "l") +testSnoc1 :: Proxy _ +testSnoc1 = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") -testSnoc2 :: SProxy "symbol" -testSnoc2 = snoc (SProxy :: SProxy _) (SProxy :: SProxy "l") +testSnoc2 :: Proxy "symbol" +testSnoc2 = snoc (Proxy :: Proxy _) (Proxy :: Proxy "l") -testSnoc3 :: SProxy "symbol" -testSnoc3 = snoc (SProxy :: SProxy "symbo") (SProxy :: SProxy _) +testSnoc3 :: Proxy "symbol" +testSnoc3 = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy _) -testSnoc4 :: SProxy "s" -testSnoc4 = snoc (SProxy :: SProxy "") (SProxy :: SProxy "s") +testSnoc4 :: Proxy "s" +testSnoc4 = snoc (Proxy :: Proxy "") (Proxy :: Proxy "s") main :: Effect Unit From 49e94b4f519ec8ff138f6cafae8788243d1bffa7 Mon Sep 17 00:00:00 2001 From: csicar Date: Sat, 4 Dec 2021 23:24:18 +0100 Subject: [PATCH 4/7] Rename `reverse` to match convention --- src/Type/Data/Symbol.purs | 40 ++++++++++++++++++++++---------------- test/Main.purs | 41 ++++++++++++++++++++++++--------------- 2 files changed, 48 insertions(+), 33 deletions(-) diff --git a/src/Type/Data/Symbol.purs b/src/Type/Data/Symbol.purs index e489ff1..2af5549 100644 --- a/src/Type/Data/Symbol.purs +++ b/src/Type/Data/Symbol.purs @@ -1,12 +1,12 @@ module Type.Data.Symbol ( append , class Equals - , class Mirror - , class MirrorP + , class Reverse + , class ReverseP , class Snoc , compare , equals - , mirror + , reverse , module Data.Symbol , module Prim.Symbol , snoc @@ -41,25 +41,30 @@ equals :: forall proxy l r o. Equals l r o => proxy l -> proxy r -> Proxy o equals _ _ = Proxy --- Mirror +-- Reverse -class MirrorP (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a +class ReverseP (a :: Symbol) (reversed :: Symbol) | a -> reversed, reversed -> a -instance mirrorEmpty :: MirrorP "" "" +instance reverseEmpty :: ReverseP "" "" else -instance mirrorCons :: +instance reverseCons :: ( Cons head tail sym - , MirrorP tailMirror tail - , MirrorP tail tailMirror - , Append tailMirror head mirror - ) => MirrorP sym mirror + , ReverseP tailReverse tail + , ReverseP tail tailReverse + , Append tailReverse head reversed + ) => ReverseP sym reversed -class Mirror (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a +class Reverse (a :: Symbol) (reversed :: Symbol) | a -> reversed, reversed -> a -instance mirrorMirrorP :: (MirrorP a b, MirrorP b a) => Mirror a b +instance reverseReverseP :: (ReverseP a b, ReverseP b a) => Reverse a b -mirror :: ∀ proxy a b. Mirror a b => proxy a -> Proxy b -mirror _ = Proxy +--| ```purescript +--| > :t reverse (Proxy :: Proxy "symbol") +--| Proxy @Symbol "lobmys" +--| ``` +-- | +reverse :: ∀ proxy a b. Reverse a b => proxy a -> Proxy b +reverse _ = Proxy -- Snoc @@ -70,10 +75,11 @@ mirror _ = Proxy -- | `end` must be a single character class Snoc (list :: Symbol) (end :: Symbol) (symbol :: Symbol) | end list -> symbol, symbol -> end list -instance snocMirror :: (Mirror sym mirror, Cons end listMirror mirror, Mirror listMirror list) => Snoc list end sym +instance snocReverse :: (Reverse sym reversed, Cons end listReverse reversed, Reverse listReverse list) => Snoc list end sym --| ```purescript ---| snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") = Proxy :: Proxy "symbol" +--| > :t snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") +--| Proxy @Symbol "symbol" --| ``` snoc :: ∀a b c. Snoc a b c => Proxy a -> Proxy b -> Proxy c snoc _ _ = Proxy diff --git a/test/Main.purs b/test/Main.purs index 25436ac..0bef914 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -4,35 +4,44 @@ import Prelude import Effect (Effect) import Effect.Class.Console (log) -import Type.Data.Symbol (mirror, reifySymbol, snoc) +import Prim.Symbol (class Cons) +import Type.Data.Symbol (class Reverse, class Snoc, reifySymbol, reverse, snoc) import Type.Proxy (Proxy(..)) --- mirror -testMirror :: Proxy "lobmys" -testMirror = mirror (Proxy::_ "symbol") +-- reverse +testReverse :: Proxy "lobmys" +testReverse = reverse (Proxy :: Proxy "symbol") -testMirror1 :: Proxy _ -testMirror1 = mirror (Proxy::_ "symbol") +testReverseForward :: Proxy _ +testReverseForward = reverse (Proxy:: Proxy "symbol") -testMirror2 :: Proxy "lobmyys" -testMirror2 = mirror (Proxy :: Proxy _) +testReverseBackward :: Proxy "lobmyys" +testReverseBackward = reverse (Proxy :: Proxy _) + +testReverseSingle :: Proxy "s" +testReverseSingle = reverse $ Proxy :: Proxy "s" + +testReverseEmpty :: Proxy "" +testReverseEmpty = reverse $ Proxy :: Proxy "" -- snoc testSnoc :: Proxy "symbol" testSnoc = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") -testSnoc1 :: Proxy _ -testSnoc1 = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") +testSnocForward :: Proxy _ +testSnocForward = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") -testSnoc2 :: Proxy "symbol" -testSnoc2 = snoc (Proxy :: Proxy _) (Proxy :: Proxy "l") +testSnocBackwardLeft :: Proxy "symbol" +testSnocBackwardLeft = snoc (Proxy :: Proxy _) (Proxy :: Proxy "l") -testSnoc3 :: Proxy "symbol" -testSnoc3 = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy _) +testSnocBackwardRight :: Proxy "symbol" +testSnocBackwardRight = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy _) -testSnoc4 :: Proxy "s" -testSnoc4 = snoc (Proxy :: Proxy "") (Proxy :: Proxy "s") +testSnocBackwardBoth :: Proxy "symbol" +testSnocBackwardBoth = snoc (Proxy :: Proxy _) (Proxy :: Proxy _) +testSnocEmpty :: Proxy "s" +testSnocEmpty = snoc (Proxy :: Proxy "") (Proxy :: Proxy "s") main :: Effect Unit main = do From aa2c4a2a1c82ea0f3b1481fb016b6559a5a689a3 Mon Sep 17 00:00:00 2001 From: csicar Date: Mon, 6 Dec 2021 01:06:17 +0100 Subject: [PATCH 5/7] Add suggested idem test --- bower.json | 4 ++++ test/Main.purs | 19 +++++++++++++++++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/bower.json b/bower.json index 2ef2de0..ba889df 100644 --- a/bower.json +++ b/bower.json @@ -18,5 +18,9 @@ "dependencies": { "purescript-prelude": "^5.0.0", "purescript-type-equality": "^4.0.0" + }, + "devDependencies": { + "purescript-assert": "^5.0.0", + "purescript-console": "^5.0.0" } } diff --git a/test/Main.purs b/test/Main.purs index 0bef914..fdf3b71 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -2,10 +2,12 @@ module Test.Main where import Prelude +import Debug (spy) import Effect (Effect) import Effect.Class.Console (log) import Prim.Symbol (class Cons) -import Type.Data.Symbol (class Reverse, class Snoc, reifySymbol, reverse, snoc) +import Test.Assert (assertTrue) +import Type.Data.Symbol (class IsSymbol, class Reverse, class ReverseP, class Snoc, reflectSymbol, reverse, snoc) import Type.Proxy (Proxy(..)) -- reverse @@ -24,6 +26,16 @@ testReverseSingle = reverse $ Proxy :: Proxy "s" testReverseEmpty :: Proxy "" testReverseEmpty = reverse $ Proxy :: Proxy "" +-- or something like this that verifies this is true +propReverseIdem :: forall a b . IsSymbol a => IsSymbol b => Reverse a b => Reverse b a => Proxy a -> Boolean +propReverseIdem p = reflectSymbol p == reflectSymbol sameThing + where + sameThing = reverse (reverse p :: Proxy b) + +-- just confirming that more complex unicode works +testUnicode :: Proxy "🍎enip" +testUnicode = reverse (Proxy :: Proxy "pine🍎") + -- snoc testSnoc :: Proxy "symbol" testSnoc = snoc (Proxy :: Proxy "symbo") (Proxy :: Proxy "l") @@ -45,4 +57,7 @@ testSnocEmpty = snoc (Proxy :: Proxy "") (Proxy :: Proxy "s") main :: Effect Unit main = do - log "asd" \ No newline at end of file + assertTrue $ propReverseIdem (Proxy :: Proxy "Test Symbol") + assertTrue $ propReverseIdem (Proxy :: Proxy "Unico∀e") + assertTrue $ propReverseIdem (Proxy :: Proxy "<-<>") + assertTrue $ propReverseIdem (Proxy :: Proxy "pine🍎") \ No newline at end of file From 8ba140181e574180a32806eab0529607b38551a0 Mon Sep 17 00:00:00 2001 From: csicar Date: Mon, 6 Dec 2021 01:09:24 +0100 Subject: [PATCH 6/7] Update comments --- test/Main.purs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/test/Main.purs b/test/Main.purs index fdf3b71..658d6c5 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -26,13 +26,12 @@ testReverseSingle = reverse $ Proxy :: Proxy "s" testReverseEmpty :: Proxy "" testReverseEmpty = reverse $ Proxy :: Proxy "" --- or something like this that verifies this is true +-- Reversing a reversed Symbol should be the same as the Symbol itself propReverseIdem :: forall a b . IsSymbol a => IsSymbol b => Reverse a b => Reverse b a => Proxy a -> Boolean propReverseIdem p = reflectSymbol p == reflectSymbol sameThing where sameThing = reverse (reverse p :: Proxy b) --- just confirming that more complex unicode works testUnicode :: Proxy "🍎enip" testUnicode = reverse (Proxy :: Proxy "pine🍎") From 827bc31cc387cad295d96b19c8b2c530b6627138 Mon Sep 17 00:00:00 2001 From: csicar Date: Mon, 6 Dec 2021 01:24:50 +0100 Subject: [PATCH 7/7] Test single and empty string --- test/Main.purs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/Main.purs b/test/Main.purs index 658d6c5..e61c5b4 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -59,4 +59,6 @@ main = do assertTrue $ propReverseIdem (Proxy :: Proxy "Test Symbol") assertTrue $ propReverseIdem (Proxy :: Proxy "Unico∀e") assertTrue $ propReverseIdem (Proxy :: Proxy "<-<>") + assertTrue $ propReverseIdem (Proxy :: Proxy "") + assertTrue $ propReverseIdem (Proxy :: Proxy "1") assertTrue $ propReverseIdem (Proxy :: Proxy "pine🍎") \ No newline at end of file