Safe Haskell | None |
---|---|
Language | Haskell2010 |
promoted functions for proxies
Synopsis
- data ProxyT
- data Proxy1T
- data Proxy2T
- data Proxify p
- data Pop0 p q
- data Pop1 p q r
- data Pop2 p q r s
- data Pop1' p q r
- data Pop2' p q r s
- data PApp p q
- data PApp2 p q r
- type family Proxy2TT (x :: Type) :: Type -> Type where ...
- type family Pop0T (p :: Type) (q :: Type) :: Type where ...
- type family Pop1T (p :: Type) (q :: k) (r :: Type) :: Type where ...
- type family Pop1'T (p :: Type) (q :: Type) (r :: Type) :: Type where ...
- type family Pop2T (p :: Type) (q :: k) (r :: k1) (s :: Type) :: Type where ...
- type family Pop2'T (p :: Type) (q :: Type) (r :: Type) (s :: Type) :: Type where ...
- type family PAppT (p :: Type) (q :: Type) :: Type where ...
- type family PApp2T (p :: Type) (q :: Type) (r :: Type) :: Type where ...
- type family ProxifyT p where ...
create a proxy from a type
makes a proxy from a simple type: similar to the P instance for 'Proxy but requires a show instance
>>>
pz @(Pop1' (Proxy FromInteger) ProxyT 123) (4 % 0)
Val (123 % 1)
>>>
pz @(Pop1' (Proxy MEmptyT) ProxyT ()) (SG.Product 4)
Val (Product {getProduct = 1})
>>>
pz @((Id $$ 44) >> Pop1' (Proxy MEmptyT) ProxyT ()) SG.Product
Val (Product {getProduct = 1})
>>>
pz @((ProxyT << Fst) >> FMap Head) ([True],13) ^!? acts . _Val . to typeRep -- Proxify is easier
Just Bool
makes a proxy from a one parameter container
>>>
pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Nothing
Val Nothing
>>>
pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) (Just 10)
Val Nothing
>>>
pz @((Id $$ ()) >> Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Just
Val Nothing
makes a proxy from a two parameter container
>>>
pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Left "ASf")
Val (Left "")
>>>
pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Right 1)
Val (Left "")
>>>
pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Left
Val (Left "")
>>>
pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Right
Val (Left "")
>>>
pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Right
Val (Left "")
>>>
pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Left
Val (Left "")
create a Proxy z from proxy z where z is the expression pointed to by p
: Proxify alway returns Val (Proxy @z)
>>>
pz @(Proxify Fst) ([True],13) ^!? acts . _Val . only (Proxy @Bool)
Just ()
>>>
pz @(Proxify (MkJust 1)) () ^!? acts . _Val . to typeRep
Just Int
>>>
pz @(Proxify (FailT [Double] "abc")) () ^!? acts . _Val . to typeRep
Just Double
>>>
pz @(Proxify "abc") () ^!? acts . _Val . to typeRep
Just Char
>>>
eval (Proxy @(Proxify Id)) defOpts ([] @Double) ^!? acts . ttVal . _Val . to typeRep
Just Double
>>>
eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? _Id . ttVal . _Val == Just (Proxy @Int)
True
>>>
eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? _Wrapped @(Identity _) . ttVal . _Val == Just (Proxy @Int)
True
>>>
eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? folded @Identity . ttVal . _Val == Just (Proxy @Int)
True
simple proxy application
run the proxy p
in the environment pointed to by q
>>>
pl @(Pop0 (Proxy '(Head,Len)) "abcdef") ()
Present ('a',6) (Pop0 | '('a',6)) Val ('a',6)
>>>
pz @(Pop0 Id "abcdef") (Proxy @'(Head,Len))
Val ('a',6)
>>>
pl @(Pop0 Fst Snd) (Proxy @Snd,("dd","ee"))
Present "ee" (Pop0 | Snd "ee" | ("dd","ee")) Val "ee"
>>>
pz @(Pop0 Fst L22) (Proxy @(Fst <> Snd),(True,("dd","ee")))
Val "ddee"
>>>
pz @(Pop0 Id () <> "def") (Proxy @"abc") -- Proxy works for any kind!
Val "abcdef"
>>>
pz @(Pop0 Id () <> "def") (Nothing @(W "abc")) -- Proxy works for any kind!
Val "abcdef"
>>>
pz @(Pop0 Id (C "A")) (Proxy @Succ)
Val 'B'
>>>
pz @(Pop0 Fst Snd) (Proxy @(All1 Even),[1,5,2,3,4])
Val False
>>>
pz @(Pop0 Fst Snd) (Proxy @(Partition Even Snd),(True,[8,1,5,2,3,4,6]))
Val ([8,2,4,6],[1,5,3])
>>>
pl @(Proxy Snd >> Pop0 Id '( 'True,2)) ()
Present 2 ((>>) 2 | {Pop0 | Snd 2 | (True,2)}) Val 2
>>>
pl @(Proxy (Fst <> Snd) >> Pop0 Id '("aa","bb")) ()
Present "aabb" ((>>) "aabb" | {Pop0 | "aa" <> "bb" = "aabb"}) Val "aabb"
>>>
pz @(Pop0 Fst Snd) (Proxy @Succ,EQ)
Val GT
>>>
pz @(Pop0 Fst Snd) (Proxy @(FMap Succ),Just 23)
Val (Just 24)
>>>
pz @(Pop0 Id (1 ... 12)) (Proxy @(FMap Succ))
Val [2,3,4,5,6,7,8,9,10,11,12,13]
>>>
pz @(Pop0 Id '( 'True, MkJust 12)) (Proxy @(FMap $ FMap Succ))
Val (True,Just 13)
>>>
pz @('(Id, PApp (Proxy '(,)) (Proxy 4)) >> Second (PApp Id (Proxy Fst)) >> Pop0 Snd Fst) ("abc",True)
Val (4,"abc")
>>>
pz @(Pop1 (Proxy Proxy) "abc" () >> Pop0 Id ()) ()
Val "abc"
>>>
pz @(Proxy (Proxy (Proxy "asdff")) >> Pop0 Id () >> Pop0 Id () >> Pop0 Id ()) ()
Val "asdff"
needs kind signatures on p
applies Proxy p
to q
in the environment pointed to by r
: needs kind signatures on p
>>>
pz @(Pop1 Fst L22 Snd) (Proxy @Length,(False,('x',"abcdef")))
Val 6
>>>
pz @(Proxy Length >> Pop1 IdT Snd '(1,'[1,2,3,4])) ()
Val 4
>>>
pz @(LiftA2 (Pop1 Fst Snd Id) (MkJust (Proxy (Lift Succ))) (MkJust 1)) ()
Val (Just 2)
>>>
pz @(LiftA2 (Pop1 Fst Snd Id) (MkJust (Proxy ((*) 4))) (MkJust 3)) ()
Val (Just 12)
>>>
pz @(Pop1 Fst Snd Id <$> MkJust (Proxy ((*) 4)) <:> MkJust 3) ()
Val (Just 12)
>>>
pz @(Pop1 Fst Snd Id <$> Fst <:> Snd) (Just (Proxy @((*) 4)), Just 3)
Val (Just 12)
>>>
pz @(Proxy (Lift "asdf") >> Pop1 Id 123 Id) ()
Val "asdf"
>>>
pz @(Pop1 Id "abc" ()) (Proxy @(K 99))
Val 99
>>>
pz @(Pop1 Id "abc" ()) (Proxy @(Flip K 99))
Val "abc"
>>>
pz @(Pop1 (Proxy ('(,) 'True)) Len "abc") ()
Val (True,3)
apply Proxy p
to q
and r
then run in the environment pointed to by s
: needs kind signatures on p
>>>
pz @(Pop2 (Proxy '(,)) Fst 14 Id) ([1..4],'True)
Val ([1,2,3,4],14)
>>>
pz @(Pop2' (Proxy Pure) (Proxy SG.Sum) (Proxy Id) Id) 123
Val (Sum {getSum = 123})
apply Proxy p
to Proxy q
and run in the environment pointed to by r
: needs kind signatures on p
>>>
pz @(Pop1' (Proxy ((<>) Snd)) (Proxy Fst) Id) ("abc","def")
Val "defabc"
>>>
pz @(Pop1' (Proxy ((>>) Snd)) (Proxy (Resplit "\\." >> Map (ReadP Int Id))) Id) (1,"123.33.5")
Val [123,33,5]
>>>
pz @(Pop1' (Proxy (Lift Snd)) (Proxy Fst) Id) ((True,2),("abc",1 % 4))
Val 2
>>>
pz @(Pop1' Fst Snd Thd) (Proxy @(Lift Snd), Proxy @Fst,((True,2),("abc",1 % 4)))
Val 2
>>>
pz @(Pop1' Fst Snd '( '( 'True,2),'("abc",1 % 4))) (Proxy @(Lift Snd), Proxy @Fst)
Val 2
>>>
pz @(Pop1' (Proxy MEmptyT) (Proxy (SG.Sum _)) ()) ()
Val (Sum {getSum = 0})
>>>
pz @(Pop1' (Proxy MEmptyT) (PApp (Proxy SG.Sum) (Proxy Float)) ()) ()
Val (Sum {getSum = 0.0})
>>>
pz @(Pop1' (Proxy Proxy) (Proxy Fst) () >> Pop0 Id '("abc",1234)) ()
Val "abc"
>>>
pz @(Pop1' (Proxy ToEnum) 'Proxy 100) 'a'
Val 'd'
>>>
pz @(Pop1' (Proxy ToEnum) 'Proxy 120) (undefined :: Char)
Val 'x'
Applies Proxy p
to Proxy q
and Proxy r
and runs in the environment pointed to by s
: needs kind signatures on p
>>>
pz @(Pop2' (Proxy '(,)) (Proxy 1) (Proxy "sss") ()) ()
Val (1,"sss")
>>>
pz @(Pop2' (Proxy '(,)) (Proxy L31) (Proxy (Fst % Snd)) '(11,99,'("ss",3))) ()
Val ("ss",1 % 9)
>>>
pz @(Pop2' Fst Snd Thd (L4 Id)) (Proxy @'(,), Proxy @L31, Proxy @(Fst % Snd), (11,99,("ss",3)))
Val ("ss",1 % 9)
applies Proxy p
to Proxy q
and returns a Proxy: needs kind signatures on p
>>>
pz @(PApp Fst Snd >> Pop0 Id '("abcdef",99)) (Proxy @('(,) (Fst >> Len)), Proxy @16)
Val (6,16)
>>>
pz @('(Id,PApp (Proxy ('(,) (Fst >> Len))) (Proxy 16)) >> Pop0 Snd Fst) ("abcdefg",101)
Val (7,16)
>>>
pz @('(Id,PApp (Proxy '(,)) (Proxy (Fst >> Len))) >> Second (PApp Id (Proxy 16)) >> Pop0 Snd Fst) ("abcdefg",101) -- or can call PApp2
Val (7,16)
>>>
pz @(PApp (PApp (Proxy ('(,) :: GL.Nat -> GL.Symbol -> (GL.Nat,GL.Symbol))) (Proxy 1)) (Proxy "abc")) () ^!? acts . _Val . to typeRep
Just ('(,) Nat Symbol 1 "abc")
>>>
pz @(PApp (Proxy '(,)) (Proxy 4) >> PApp Id (Proxy Fst) >> Pop0 Id (W '(1,2))) ()
Val (4,1)
>>>
pz @(PApp (Proxy '(,)) (Proxy 4) >> PApp Id (Proxy Fst) >> Pop0 Id '( 'True,"hello")) ()
Val (4,True)
>>>
pan @(PApp (Proxy (MsgI "hello ")) Fst >> Pop0 Id '(1,2,3)) (Proxy @"there",())
P (>>) "there" | +- P PApp | `- P Pop0 | hello '"there" | +- P '(,,) | | | +- P '1 | | | +- P '2 | | | `- P '3 | `- P hello '"there" Val "there"
>>>
pz @(PApp (Proxy Proxy) (Proxy "abc") >> Pop0 Id () >> Pop0 Id ()) ()
Val "abc"
>>>
pz @(PApp (Proxy '(,,)) (Proxy 10) >> PApp Id (Proxy "ss") >> PApp Id (Proxy Fst) >> Pop0 Id '(13 % 44,C "x")) ()
Val (10,"ss",13 % 44)
>>>
pz @('(Id,PApp (Proxy '(,,)) (Proxy 10) >> PApp Id (Proxy "ss") >> PApp Id (Proxy Fst)) >> Pop0 Snd Fst) (13 % 44,'x')
Val (10,"ss",13 % 44)
applies Proxy p
to Proxy q
and Proxy r
and returns a Proxy: needs kind signatures on p
>>>
pz @(PApp2 (Proxy '(,)) (Proxy 2) (Proxy 'True) >> Pop0 Id ()) ()
Val (2,True)
>>>
pz @('(Snd, PApp2 (Proxy (+)) L11 L12) >> Pop0 Snd Fst) ((Proxy @Fst,Proxy @(Length Snd)),(5,"abcdef"))
Val 11
>>>
pz @(PApp2 (Proxy (+)) Fst Snd >> Pop0 Id ()) (Proxy @(W 3),Proxy @(W 7))
Val 10
>>>
pz @(PApp2 Fst Snd Thd >> Pop0 Id ()) (Proxy @(&&&), Proxy @(W "abc"), Proxy @(W 13))
Val ("abc",13)
type families
type family Pop2T (p :: Type) (q :: k) (r :: k1) (s :: Type) :: Type where ... Source #
Pop2T (Proxy z) q r s = PP (z q r) s | |
Pop2T p q r s = TypeError (((('Text "Pop2T: requires 'Proxy z' and z must be a function requiring one parameter!!" :$$: ('Text " p = " :<>: 'ShowType p)) :$$: ('Text " q = " :<>: 'ShowType q)) :$$: ('Text " r = " :<>: 'ShowType r)) :$$: ('Text " s = " :<>: 'ShowType s)) |
type family Pop2'T (p :: Type) (q :: Type) (r :: Type) (s :: Type) :: Type where ... Source #
Pop2'T (Proxy z) (Proxy w) (Proxy v) s = PP (z w v) s | |
Pop2'T p q r s = TypeError (((('Text "Pop2'T: requires 'Proxy z' and z must be a function requiring one parameter!!" :$$: ('Text " p = " :<>: 'ShowType p)) :$$: ('Text " q = " :<>: 'ShowType q)) :$$: ('Text " r = " :<>: 'ShowType r)) :$$: ('Text " s = " :<>: 'ShowType s)) |