Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
==================== Tidy Core ====================
2019-03-26 16:42:16.733069541 UTC
Result size of Tidy Core
= {terms: 572, types: 1,423, coercions: 358, joins: 0/6}
-- RHS size: {terms: 5, types: 17, coercions: 9, joins: 0/0}
$WUnion :: forall (e :: * -> *) a. e a -> Union '[e] a
$WUnion
= \ (@ (e :: * -> *)) (@ a) (dt :: e a) ->
Union @ '[e] @ a @ e @~ <Co:9> dt
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
main2 :: Int
main2 = I# 0#
-- RHS size: {terms: 17, types: 78, coercions: 17, joins: 0/0}
main3
:: forall x.
Union '[State (Sum Int)] x -> Sum Int -> Identity (x, Sum Int)
main3
= \ (@ x) (u :: Union '[State (Sum Int)] x) (eta :: Sum Int) ->
case u of { Union @ e co a ->
case a `cast` <Co:5> of {
Get k -> (k eta, eta) `cast` <Co:6>;
Put s k -> (k, s) `cast` <Co:6>
}
}
-- RHS size: {terms: 2, types: 6, coercions: 0, joins: 0/0}
lvl :: State (Sum Int) (Sum Int)
lvl = Get @ (Sum Int) @ (Sum Int) (id @ (Sum Int))
-- RHS size: {terms: 2, types: 16, coercions: 11, joins: 0/0}
lvl1 :: Union '[State (Sum Int)] (Sum Int)
lvl1
= Union
@ '[State (Sum Int)] @ (Sum Int) @ (State (Sum Int)) @~ <Co:11> lvl
Rec {
-- RHS size: {terms: 40, types: 80, coercions: 65, joins: 0/2}
main_$sgo
:: Int#
-> (forall x.
Union '[State (Sum Int)] x -> StateT (Sum Int) Identity x)
-> StateT (Sum Int) Identity ()
main_$sgo
= \ (x :: Int#)
(eta
:: forall x1.
Union '[State (Sum Int)] x1 -> StateT (Sum Int) Identity x1) ->
let {
m1 :: StateT (Sum Int) Identity (Sum Int)
m1 = eta @ (Sum Int) lvl1 } in
let {
ds1 :: StateT (Sum Int) Identity ()
ds1
= case x of wild {
__DEFAULT -> main_$sgo (+# wild 1#) eta;
100# -> (\ (s1 :: Sum Int) -> ((), s1)) `cast` <Co:16>
} } in
(\ (s1 :: Sum Int) ->
case ((m1 `cast` <Co:6>) s1) `cast` <Co:6> of { (a1, s') ->
case a1 `cast` <Co:2> of { I# ipv ->
case (((eta
@ ()
(Union
@ '[State (Sum Int)]
@ ()
@ (State (Sum Int))
@~ <Co:11>
(Put @ (Sum Int) @ () ((I# (+# ipv x)) `cast` <Co:3>) ())))
`cast` <Co:5>)
s')
`cast` <Co:5>
of
{ (a2, s'1) ->
(ds1 `cast` <Co:5>) s'1
}
}
})
`cast` <Co:6>
end Rec }
-- RHS size: {terms: 18, types: 20, coercions: 37, joins: 0/0}
main1 :: String
main1
= case (((main_$sgo 0# (main3 `cast` <Co:22>)) `cast` <Co:5>)
(main2 `cast` <Co:3>))
`cast` <Co:5>
of
{ (a1, b1) ->
case b1 `cast` <Co:2> of { I# ww3 ->
case $wshowSignedInt 0# ww3 ([] @ Char) of { (# ww5, ww6 #) ->
: @ Char ww5 ww6
}
}
}
-- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
main :: IO ()
main = hPutStr' stdout main1 True
-- RHS size: {terms: 2, types: 1, coercions: 0, joins: 0/0}
main4 :: State# RealWorld -> (# State# RealWorld, () #)
main4 = runMainIO1 @ () main
-- RHS size: {terms: 1, types: 0, coercions: 3, joins: 0/0}
main :: IO ()
main = main4 `cast` <Co:3>
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Get3 :: Addr#
$tc'Get3 = "'Get"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Get2 :: TrName
$tc'Get2 = TrNameS $tc'Get3
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Put3 :: Addr#
$tc'Put3 = "'Put"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Put2 :: TrName
$tc'Put2 = TrNameS $tc'Put3
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcState2 :: Addr#
$tcState2 = "State"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcState1 :: TrName
$tcState1 = TrNameS $tcState2
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcSemantic3 :: Addr#
$tcSemantic3 = "Semantic"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcSemantic2 :: TrName
$tcSemantic2 = TrNameS $tcSemantic3
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Union3 :: Addr#
$tc'Union3 = "'Union"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Union2 :: TrName
$tc'Union2 = TrNameS $tc'Union3
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcUnion2 :: Addr#
$tcUnion2 = "Union"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcUnion1 :: TrName
$tcUnion1 = TrNameS $tcUnion2
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$krep :: KindRep
$krep = KindRepVar 0#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$krep1 :: KindRep
$krep1 = KindRepVar 1#
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep2 :: KindRep
$krep2 = KindRepFun $krep $krep1
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep3 :: KindRep
$krep3 = KindRepApp $krep $krep1
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep4 :: [KindRep]
$krep4 = : @ KindRep $krep1 ([] @ KindRep)
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep5 :: [KindRep]
$krep5 = : @ KindRep $krep $krep4
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep6 :: [KindRep]
$krep6 = : @ KindRep krep$*Arr* ([] @ KindRep)
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep7 :: KindRep
$krep7 = KindRepTyConApp $tc[] $krep6
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tcSemantic1 :: KindRep
$tcSemantic1 = KindRepFun $krep7 krep$*Arr*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep8 :: KindRep
$krep8 = KindRepTyConApp $tc'[] $krep6
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep9 :: [KindRep]
$krep9 = : @ KindRep $krep8 ([] @ KindRep)
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep10 :: [KindRep]
$krep10 = : @ KindRep $krep $krep9
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep11 :: [KindRep]
$krep11 = : @ KindRep krep$*Arr* $krep10
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep12 :: KindRep
$krep12 = KindRepTyConApp $tc': $krep11
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep13 :: [KindRep]
$krep13 = : @ KindRep $krep12 $krep4
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule2 :: Addr#
$trModule2 = "Main"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule1 :: TrName
$trModule1 = TrNameS $trModule2
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule4 :: Addr#
$trModule4 = "main"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule3 :: TrName
$trModule3 = TrNameS $trModule4
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$trModule :: Module
$trModule = Module $trModule3 $trModule1
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcUnion :: TyCon
$tcUnion
= TyCon
229884759504400770##
13528229582907927977##
$trModule
$tcUnion1
0#
$tcSemantic1
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep14 :: KindRep
$krep14 = KindRepTyConApp $tcUnion $krep13
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Union1 :: KindRep
$tc'Union1 = KindRepFun $krep3 $krep14
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Union :: TyCon
$tc'Union
= TyCon
6632976870638181383##
15290975553766063960##
$trModule
$tc'Union2
2#
$tc'Union1
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcSemantic :: TyCon
$tcSemantic
= TyCon
9508779775375363839##
14545629556631013737##
$trModule
$tcSemantic2
0#
$tcSemantic1
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcState :: TyCon
$tcState
= TyCon
11500382755588220783##
3741540518684525139##
$trModule
$tcState1
0#
krep$*->*->*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep15 :: KindRep
$krep15 = KindRepTyConApp $tcState $krep5
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep16 :: KindRep
$krep16 = KindRepFun $krep1 $krep15
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Put1 :: KindRep
$tc'Put1 = KindRepFun $krep $krep16
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Get1 :: KindRep
$tc'Get1 = KindRepFun $krep2 $krep15
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Put :: TyCon
$tc'Put
= TyCon
15201137817969246407##
1251973250185875189##
$trModule
$tc'Put2
2#
$tc'Put1
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Get :: TyCon
$tc'Get
= TyCon
4894226031785183458##
8801726891554456039##
$trModule
$tc'Get2
2#
$tc'Get1
-- RHS size: {terms: 27, types: 61, coercions: 6, joins: 0/2}
$w$c>>
:: forall (f :: [* -> *]) a b.
Semantic f a
-> Semantic f b
-> forall (m :: * -> *).
Applicative m =>
(forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
-> (forall a1 b1. m a1 -> m b1 -> m b1)
-> (forall a1. a1 -> m a1)
-> (forall x. Union f x -> m x)
-> m b
$w$c>>
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(w :: Semantic f a)
(w1 :: Semantic f b)
(@ (m :: * -> *))
(ww :: Applicative m)
(ww1 :: forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
(ww2 :: forall a1 b1. m a1 -> m b1 -> m b1)
(ww3 :: forall a1. a1 -> m a1)
(w2 :: forall x. Union f x -> m x) ->
let {
$dMonad :: Monad m
$dMonad = C:Monad @ m ww ww1 ww2 ww3 } in
let {
lvl2 :: m b
lvl2 = (w1 `cast` <Co:3>) @ m $dMonad w2 } in
ww1 @ a @ b ((w `cast` <Co:3>) @ m $dMonad w2) (\ _ -> lvl2)
-- RHS size: {terms: 19, types: 59, coercions: 0, joins: 0/0}
$c>>
:: forall (f :: [* -> *]) a b.
Semantic f a
-> Semantic f b
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m b
$c>>
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(w :: Semantic f a)
(w1 :: Semantic f b)
(@ (m :: * -> *))
(w2 :: Monad m)
(w3 :: forall x. Union f x -> m x) ->
case w2 of { C:Monad ww1 ww2 ww3 ww4 ->
$w$c>> @ f @ a @ b w w1 @ m ww1 ww2 ww3 ww4 w3
}
-- RHS size: {terms: 1, types: 0, coercions: 22, joins: 0/0}
$fMonadSemantic_$c>>
:: forall (f :: [* -> *]) a b.
Semantic f a -> Semantic f b -> Semantic f b
$fMonadSemantic_$c>> = $c>> `cast` <Co:22>
-- RHS size: {terms: 26, types: 60, coercions: 6, joins: 0/1}
$w$c>>=
:: forall (f :: [* -> *]) a b.
Semantic f a
-> (a -> Semantic f b)
-> forall (m :: * -> *).
Applicative m =>
(forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
-> (forall a1 b1. m a1 -> m b1 -> m b1)
-> (forall a1. a1 -> m a1)
-> (forall x. Union f x -> m x)
-> m b
$w$c>>=
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(w :: Semantic f a)
(w1 :: a -> Semantic f b)
(@ (m :: * -> *))
(ww :: Applicative m)
(ww1 :: forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
(ww2 :: forall a1 b1. m a1 -> m b1 -> m b1)
(ww3 :: forall a1. a1 -> m a1)
(w2 :: forall x. Union f x -> m x) ->
let {
$dMonad :: Monad m
$dMonad = C:Monad @ m ww ww1 ww2 ww3 } in
ww1
@ a
@ b
((w `cast` <Co:3>) @ m $dMonad w2)
(\ (z1 :: a) -> ((w1 z1) `cast` <Co:3>) @ m $dMonad w2)
-- RHS size: {terms: 19, types: 60, coercions: 0, joins: 0/0}
$c>>=
:: forall (f :: [* -> *]) a b.
Semantic f a
-> (a -> Semantic f b)
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m b
$c>>=
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(w :: Semantic f a)
(w1 :: a -> Semantic f b)
(@ (m :: * -> *))
(w2 :: Monad m)
(w3 :: forall x. Union f x -> m x) ->
case w2 of { C:Monad ww1 ww2 ww3 ww4 ->
$w$c>>= @ f @ a @ b w w1 @ m ww1 ww2 ww3 ww4 w3
}
-- RHS size: {terms: 1, types: 0, coercions: 23, joins: 0/0}
$fMonadSemantic_$c>>=
:: forall (f :: [* -> *]) a b.
Semantic f a -> (a -> Semantic f b) -> Semantic f b
$fMonadSemantic_$c>>= = $c>>= `cast` <Co:23>
-- RHS size: {terms: 9, types: 21, coercions: 3, joins: 0/0}
runSemantic
:: forall (r :: [* -> *]) a.
Semantic r a
-> forall (m :: * -> *).
Monad m =>
(forall x. Union r x -> m x) -> m a
runSemantic
= \ (@ (r :: [* -> *]))
(@ a)
(dk :: Semantic r a)
(@ (m :: * -> *))
($dMonad :: Monad m)
(ds :: forall x. Union r x -> m x) ->
(dk `cast` <Co:3>) @ m $dMonad ds
-- RHS size: {terms: 18, types: 23, coercions: 0, joins: 0/0}
$fFunctorState_$cfmap
:: forall s a b. (a -> b) -> State s a -> State s b
$fFunctorState_$cfmap
= \ (@ s) (@ a) (@ b) (f :: a -> b) (ds :: State s a) ->
case ds of {
Get a1 -> Get @ s @ b (\ (b3 :: s) -> f (a1 b3));
Put a1 a2 -> Put @ s @ b a1 (f a2)
}
-- RHS size: {terms: 15, types: 22, coercions: 0, joins: 0/0}
$fFunctorState_$c<$ :: forall s a b. a -> State s b -> State s a
$fFunctorState_$c<$
= \ (@ s) (@ a) (@ b) (z1 :: a) (ds :: State s b) ->
case ds of {
Get a1 -> Get @ s @ a (\ _ -> z1);
Put a1 a2 -> Put @ s @ a a1 z1
}
-- RHS size: {terms: 4, types: 6, coercions: 0, joins: 0/0}
$fFunctorState :: forall s. Functor (State s)
$fFunctorState
= \ (@ s) ->
C:Functor
@ (State s) ($fFunctorState_$cfmap @ s) ($fFunctorState_$c<$ @ s)
-- RHS size: {terms: 24, types: 42, coercions: 6, joins: 0/0}
$fApplicativeSemantic2
:: forall (f :: [* -> *]) a b c.
(a -> b -> c)
-> Semantic f a
-> Semantic f b
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m c
$fApplicativeSemantic2
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(@ c)
(f1 :: a -> b -> c)
(x :: Semantic f a)
(eta :: Semantic f b)
(@ (m :: * -> *))
(eta1 :: Monad m)
(eta2 :: forall x1. Union f x1 -> m x1) ->
<*>
@ m
($p1Monad @ m eta1)
@ b
@ c
(fmap
@ m
($p1Applicative @ m ($p1Monad @ m eta1))
@ a
@ (b -> c)
f1
((x `cast` <Co:3>) @ m eta1 eta2))
((eta `cast` <Co:3>) @ m eta1 eta2)
-- RHS size: {terms: 5, types: 13, coercions: 0, joins: 0/0}
$fApplicativeSemantic1
:: forall b a (f :: [* -> *]).
Semantic f a
-> Semantic f b
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m a
$fApplicativeSemantic1
= \ (@ b) (@ a) (@ (f :: [* -> *])) ->
$fApplicativeSemantic2 @ f @ a @ b @ a (const @ a @ b)
-- RHS size: {terms: 12, types: 23, coercions: 0, joins: 0/1}
$cpure
:: forall (f :: [* -> *]) a.
a
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m a
$cpure
= \ (@ (f :: [* -> *]))
(@ a)
(a1 :: a)
(@ (m :: * -> *))
($dMonad :: Monad m) ->
let {
ds :: m a
ds = pure @ m ($p1Monad @ m $dMonad) @ a a1 } in
\ _ -> ds
-- RHS size: {terms: 1, types: 0, coercions: 13, joins: 0/0}
$fApplicativeSemantic_$cpure
:: forall (f :: [* -> *]) a. a -> Semantic f a
$fApplicativeSemantic_$cpure = $cpure `cast` <Co:13>
-- RHS size: {terms: 17, types: 32, coercions: 7, joins: 0/0}
$c<*>
:: forall (f :: [* -> *]) a b.
Semantic f (a -> b)
-> Semantic f a
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m b
$c<*>
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(ds :: Semantic f (a -> b))
(ds1 :: Semantic f a)
(@ (m :: * -> *))
($dMonad :: Monad m)
(eta :: forall x. Union f x -> m x) ->
<*>
@ m
($p1Monad @ m $dMonad)
@ a
@ b
((ds `cast` <Co:4>) @ m $dMonad eta)
((ds1 `cast` <Co:3>) @ m $dMonad eta)
-- RHS size: {terms: 1, types: 0, coercions: 23, joins: 0/0}
$fApplicativeSemantic_$c<*>
:: forall (f :: [* -> *]) a b.
Semantic f (a -> b) -> Semantic f a -> Semantic f b
$fApplicativeSemantic_$c<*> = $c<*> `cast` <Co:23>
-- RHS size: {terms: 17, types: 30, coercions: 3, joins: 0/0}
$fApplicativeSemantic4
:: forall (f :: [* -> *]) a b.
a
-> Semantic f b
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m a
$fApplicativeSemantic4
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(x :: a)
(eta :: Semantic f b)
(@ (m :: * -> *))
(eta1 :: Monad m)
(eta2 :: forall x1. Union f x1 -> m x1) ->
fmap
@ m
($p1Applicative @ m ($p1Monad @ m eta1))
@ b
@ a
(\ _ -> x)
((eta `cast` <Co:3>) @ m eta1 eta2)
-- RHS size: {terms: 16, types: 30, coercions: 3, joins: 0/0}
$cfmap
:: forall (f :: [* -> *]) a b.
(a -> b)
-> Semantic f a
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m b
$cfmap
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(f1 :: a -> b)
(ds :: Semantic f a)
(@ (m :: * -> *))
($dMonad :: Monad m)
(eta :: forall x. Union f x -> m x) ->
fmap
@ m
($p1Applicative @ m ($p1Monad @ m $dMonad))
@ a
@ b
f1
((ds `cast` <Co:3>) @ m $dMonad eta)
-- RHS size: {terms: 1, types: 0, coercions: 21, joins: 0/0}
$fFunctorSemantic_$cfmap
:: forall (f :: [* -> *]) a b.
(a -> b) -> Semantic f a -> Semantic f b
$fFunctorSemantic_$cfmap = $cfmap `cast` <Co:21>
-- RHS size: {terms: 4, types: 7, coercions: 16, joins: 0/0}
$fFunctorSemantic :: forall (f :: [* -> *]). Functor (Semantic f)
$fFunctorSemantic
= \ (@ (f :: [* -> *])) ->
C:Functor
@ (Semantic f)
($fFunctorSemantic_$cfmap @ f)
(($fApplicativeSemantic4 @ f) `cast` <Co:16>)
-- RHS size: {terms: 19, types: 36, coercions: 3, joins: 0/0}
$fApplicativeSemantic3
:: forall (f :: [* -> *]) a b.
Semantic f a
-> Semantic f b
-> forall (m :: * -> *).
Monad m =>
(forall x. Union f x -> m x) -> m b
$fApplicativeSemantic3
= \ (@ (f :: [* -> *]))
(@ a)
(@ b)
(a1 :: Semantic f a)
(a2 :: Semantic f b)
(@ (m :: * -> *))
(eta :: Monad m)
(eta1 :: forall x. Union f x -> m x) ->
<*>
@ m
($p1Monad @ m eta)
@ b
@ b
($fApplicativeSemantic4
@ f @ (b -> b) @ a (breakpoint @ b) a1 @ m eta eta1)
((a2 `cast` <Co:3>) @ m eta eta1)
-- RHS size: {terms: 10, types: 17, coercions: 61, joins: 0/0}
$fApplicativeSemantic
:: forall (f :: [* -> *]). Applicative (Semantic f)
$fApplicativeSemantic
= \ (@ (f :: [* -> *])) ->
C:Applicative
@ (Semantic f)
($fFunctorSemantic @ f)
($fApplicativeSemantic_$cpure @ f)
($fApplicativeSemantic_$c<*> @ f)
(($fApplicativeSemantic2 @ f) `cast` <Co:25>)
(($fApplicativeSemantic3 @ f) `cast` <Co:18>)
((\ (@ a) (@ b) -> $fApplicativeSemantic1 @ b @ a @ f)
`cast` <Co:18>)
-- RHS size: {terms: 6, types: 9, coercions: 0, joins: 0/0}
$fMonadSemantic :: forall (f :: [* -> *]). Monad (Semantic f)
$fMonadSemantic
= \ (@ (f :: [* -> *])) ->
C:Monad
@ (Semantic f)
($fApplicativeSemantic @ f)
($fMonadSemantic_$c>>= @ f)
($fMonadSemantic_$c>> @ f)
($fApplicativeSemantic_$cpure @ f)
@isovector

This comment has been minimized.

Copy link
Owner Author

commented Mar 26, 2019

note to self:

this is the diff to get SAT working after late specialize

@@ -319,7 +319,14 @@ getCoreToDo dflags
 
         runWhen late_specialise
           (CoreDoPasses [ CoreDoSpecialising
-                        , simpl_phase 0 ["post-late-spec"] max_iter]),
+                        , simpl_phase 0 ["post-late-spec"] max_iter
+                        , simpl_gently
+                        , CoreDoStaticArgs
+                        , CoreDoSpecialising
+                        , simpl_phase 0 ["post-late-spec"] max_iter
+                        , simpl_phases
+                        , simpl_gently
+                        ]),
@isovector

This comment has been minimized.

Copy link
Owner Author

commented Apr 8, 2019

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UnicodeSyntax         #-}

module MVP (main) where

import qualified Control.Monad.Trans.State.Strict as S
import           Data.Coerce
import           Data.Functor.Compose
import           Data.Functor.Identity
import           Data.Typeable

newtype Semantic r a = Semantic
  { runSemantic
        :: ∀ m
         . Monad m
        => (∀ x. Union r (Semantic r) x -> m x)
        -> m a
  }

usingSemantic
    :: Monad m
    => ( x. Union r (Semantic r) x -> m x)
    -> Semantic r a
    -> m a
usingSemantic k m = runSemantic m k
{-# INLINE usingSemantic #-}

instance Functor (Semantic f) where
  fmap f (Semantic m) = Semantic $ \k -> fmap f $ m k
  {-# INLINE fmap #-}

instance Applicative (Semantic f) where
  pure a = Semantic $ const $ pure a
  {-# INLINE pure #-}

  Semantic f <*> Semantic a = Semantic $ \k -> f k <*> a k
  {-# INLINE (<*>) #-}

instance Monad (Semantic f) where
  return = pure
  {-# INLINE return #-}

  Semantic ma >>= f = Semantic $ \k -> do
    z <- ma k
    runSemantic (f z) k
  {-# INLINE (>>=) #-}

liftSemantic :: Union r (Semantic r) a -> Semantic r a
liftSemantic u = Semantic $ \k -> k u
{-# INLINE liftSemantic #-}

hoistSemantic
    :: ( x. Union r (Semantic r) x -> Union r' (Semantic r') x)
    -> Semantic r a
    -> Semantic r' a
hoistSemantic nat (Semantic m) = Semantic $ \k -> m $ \u -> k $ nat u
{-# INLINE hoistSemantic #-}

raise :: forall e r a. Semantic r a -> Semantic (e ': r) a
raise = hoistSemantic $ hoist raise' . weaken
{-# INLINE raise #-}

raise' :: Semantic r a -> Semantic (e ': r) a
raise' = raise
{-# NOINLINE raise' #-}

send :: Member e r => e (Semantic r) a -> Semantic r a
send = liftSemantic . inj
{-# INLINE[3] send #-}

sendM :: Member (Lift m) r => m a -> Semantic r a
sendM = send . Lift
{-# INLINE sendM #-}

run :: Semantic '[] a -> a
run (Semantic m) = runIdentity $ m absurdU
{-# INLINE run #-}

runM :: Monad m => Semantic '[Lift m] a -> m a
runM (Semantic m) = m $ \z ->
  case extract z of
    Yo e s _ f -> do
      a <- unLift e
      pure $ f $ a <$ s
{-# INLINE runM #-}

slowBeforeSpecialization :: Member (State Int) r => Semantic r Int
slowBeforeSpecialization = do
  n <- get
  if n <= 0
     then pure n
     else do
       put $ n - 1
       slowBeforeSpecialization

main :: IO ()
main = print $ countDown 100

countDown :: Int -> Int
countDown s =
  fst . run . runState s $ slowBeforeSpecialization

data State s m a where
  Get :: State s m s
  Put :: s -> State s m ()

get :: Member (State s) r => Semantic r s
get = send Get
{-# INLINE get #-}

put :: Member (State s) r => s -> Semantic r ()
put = send . Put
{-# INLINE put #-}

gets :: Member (State s) r => (s -> a) -> Semantic r a
gets f = fmap f get
{-# INLINE gets #-}

modify :: Member (State s) r => (s -> s) -> Semantic r ()
modify f = do
  s <- get
  put $ f s
{-# INLINE modify #-}

runState :: s -> Semantic (State s ': r) a -> Semantic r (s, a)
runState = stateful $ \case
  Get   -> \s -> pure (s, s)
  Put s -> const $ pure (s, ())
{-# INLINE[3] runState #-}

{-# RULES "runState/reinterpret"
   forall s e (f :: forall m x. e m x -> Semantic (State s ': r) x).
     runState s (reinterpret f e) = stateful (\x s' -> runState s' $ f x) s e
     #-}

swap :: (a, b) -> (b, a)
swap ~(a, b) = (b, a)
{-# INLINE swap #-}

type Tactically m r x =  f. Functor f => Semantic (Tactics f m r ': r) (f x)

interpretH
    :: forall e r a
     . ( x m . e m x -> Tactically m r x)
    -> Semantic (e ': r) a
    -> Semantic r a
interpretH f (Semantic m) = m $ \u ->
  case decomp u of
    Left  x -> liftSemantic $ hoist (interpretH f) x
    Right (Yo e s d y) -> do
      a <- runTactics s (interpretH f . d) (f e)
      pure $ y a
{-# INLINE interpretH #-}

interpret
    :: ( x m. e m x -> Semantic r x)
    -> Semantic (e ': r) a
    -> Semantic r a
interpret f = interpretH $ \(e :: e m x) -> toH @m $ f e
{-# INLINE interpret #-}

interpretInStateT
    :: ( x m. e m x -> S.StateT s (Semantic r) x)
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
interpretInStateT f s (Semantic m) = Semantic $ \k ->
  fmap swap $ flip S.runStateT s $ m $ \u ->
    case decomp u of
        Left x -> S.StateT $ \s' ->
          k . fmap swap
            . weave (s', ()) (uncurry $ interpretInStateT_b f)
            $ x
        Right (Yo e z _ y) ->
          fmap (y . (<$ z)) $ S.mapStateT (usingSemantic k) $ f e
{-# INLINE interpretInStateT #-}

interpretInStateT_b
    :: ( x m. e m x -> S.StateT s (Semantic r) x)
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
interpretInStateT_b = interpretInStateT
{-# NOINLINE interpretInStateT_b #-}

reinterpretH
    :: forall e2 e1 r a
     . ( m x. e1 m x -> Tactically m (e2 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': r) a
reinterpretH f (Semantic m) = Semantic $ \k -> m $ \u ->
  case decompCoerce u of
    Left x  -> k $ hoist (reinterpretH f) $ x
    Right (Yo e s d y) -> do
      a <- usingSemantic k $ runTactics s (reinterpretH f . d) $ f e
      pure $ y a
{-# INLINE[3] reinterpretH #-}

reinterpret2H
    :: forall e2 e3 e1 r a
     . ( m x. e1 m x -> Tactically m (e2 ': e3 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': e3 ': r) a
reinterpret2H f (Semantic m) = Semantic $ \k -> m $ \u ->
  case decompCoerce u of
    Left x  -> k $ weaken $ hoist (reinterpret2H f) $ x
    Right (Yo e s d y) -> do
      a <- usingSemantic k $ runTactics s (reinterpret2H f . d) $ f e
      pure $ y a
{-# INLINE[3] reinterpret2H #-}

interceptH
    :: forall e r a. Member e r
    => ( x m. e m x -> Tactically m r x)
    -> Semantic r a
    -> Semantic r a
interceptH f (Semantic m) = Semantic $ \k -> m $ \u ->
  case prj @e u of
    Just (Yo e s d y) -> usingSemantic k $ fmap y $ runTactics s d $ f e
    Nothing -> k u
{-# INLINE interceptH #-}

stateful
    :: ( x m. e m x -> s -> Semantic r (s, x))
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
stateful f = interpretInStateT $ \e -> S.StateT $ fmap swap . f e
{-# INLINE[3] stateful #-}

reinterpret
    :: forall e2 e1 r a
     . ( m x. e1 m x -> Semantic (e2 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': r) a
reinterpret f = reinterpretH $ \(e :: e m x) -> toH @m $ f e
{-# INLINE[3] reinterpret #-}

reinterpret2
    :: forall e2 e3 e1 r a
     . ( m x. e1 m x -> Semantic (e2 ': e3 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': e3 ': r) a
reinterpret2 f = reinterpret2H $ \(e :: e m x) -> toH @m $ f e
{-# INLINE[3] reinterpret2 #-}

intercept
    :: forall e r a. Member e r
    => ( x m. e m x -> Semantic r x)
    -> Semantic r a
    -> Semantic r a
intercept f (Semantic m) = Semantic $ \k -> m $ \u ->
  case prj @e u of
    Just (Yo e s _ y) -> usingSemantic k $ fmap (y . (<$ s)) $ f e
    Nothing -> k u
{-# INLINE intercept #-}

data Union (r :: [(* -> *) -> * -> *]) (m :: * -> *) a where
  Union
      :: SNat n
         -- ^ A proof that the effect is actually in @r@.
      -> Yo (IndexOf r n) m a
         -- ^ The effect to wrap. The functions 'prj' and 'decomp' can help
         -- retrieve this value later.
      -> Union r m a

data Yo e m a where
  Yo :: (Functor f)
     => e m a
     -> f ()
     -> (forall x. f (m x) -> n (f x))
     -> (f a -> b)
     -> Yo e n b

liftYo :: Functor m => e m a -> Yo e m a
liftYo e = Yo e (Identity ()) (fmap Identity . runIdentity) runIdentity

instance Functor (Yo e m) where
  fmap f (Yo e s d f') = Yo e s d (f . f')

instance Effect (Yo e) where
  weave s' d (Yo e s nt f) =
    Yo e (Compose $ s <$ s')
         (fmap Compose . d . fmap nt . getCompose)
         (fmap f . getCompose)
  hoist = defaultHoist

instance (Functor m) => Functor (Union r m) where
  fmap f (Union w t) = Union w $ fmap' f t
    where
      -- This is necessary to delay the interaction between the type family
      -- 'IndexOf' and the quantified superclass constraint on 'Effect'.
      fmap' :: (Functor m, Effect f) => (a -> b) -> f m a -> f m b
      fmap' = fmap
      {-# INLINE fmap' #-}
  {-# INLINE fmap #-}

instance Effect (Union r) where
  weave s f (Union w e) = Union w $ weave s f e
  {-# INLINE weave #-}

  hoist f (Union w e) = Union w $ hoist f e
  {-# INLINE hoist #-}

type Member e r =
  ( Find r e
  -- , Break (AmbiguousSend r e) (IndexOf r (Found r e))
  , e ~ IndexOf r (Found r e)
  -- , Effect e
  )

data Dict c where Dict :: c => Dict c

induceTypeable :: SNat n -> Dict (Typeable n)
induceTypeable SZ = Dict
induceTypeable (SS _) = Dict
{-# INLINE induceTypeable #-}

data Nat = Z | S Nat
  deriving Typeable

data SNat :: Nat -> * where
  SZ :: SNat 'Z
  SS :: Typeable n => SNat n -> SNat ('S n)
  deriving Typeable

type family IndexOf (ts :: [k]) (n :: Nat) :: k where
  IndexOf (k ': ks) 'Z = k
  IndexOf (k ': ks) ('S n) = IndexOf ks n

type family Found (ts :: [k]) (t :: k) :: Nat where
  Found (t ': ts) t = 'Z
  Found (u ': ts) t = 'S (Found ts t)

class Typeable (Found r t) => Find (r :: [k]) (t :: k) where
  finder :: SNat (Found r t)

instance {-# OVERLAPPING #-} Find (t ': z) t where
  finder = SZ
  {-# INLINE finder #-}

instance ( Find z t
         , Found (_1 ': z) t ~ 'S (Found z t)
         ) => Find (_1 ': z) t where
  finder = SS $ finder @_ @z @t
  {-# INLINE finder #-}

decomp :: Union (e ': r) m a -> Either (Union r m a) (Yo e m a)
decomp (Union p a) =
  case p of
    SZ   -> Right a
    SS n -> Left $ Union n a
{-# INLINE decomp #-}

extract :: Union '[e] m a -> Yo e m a
extract (Union SZ a) = a
extract _ = error "impossible"
{-# INLINE extract #-}

absurdU :: Union '[] m a -> b
absurdU = absurdU

weaken :: Union r m a -> Union (e ': r) m a
weaken (Union n a) =
  case induceTypeable n of
    Dict -> Union (SS n) a
{-# INLINE weaken #-}

inj :: forall r e a m. (Functor m , Member e r) => e m a -> Union r m a
inj e = Union (finder @_ @r @e) $ liftYo e
{-# INLINE inj #-}

prj :: forall e r a m
     . ( Member e r
       )
    => Union r m a
    -> Maybe (Yo e m a)
prj (Union (s :: SNat n) a) =
  case induceTypeable s of
    Dict ->
      case eqT @n @(Found r e) of
        Just Refl -> Just a
        Nothing -> Nothing
{-# INLINE prj #-}

decompCoerce
    :: Union (e ': r) m a
    -> Either (Union (f ': r) m a) (Yo e m a)
decompCoerce (Union p a) =
  case p of
    SZ -> Right a
    SS n -> Left (Union (SS n) a)
{-# INLINE decompCoerce #-}

class ( m. Functor m => Functor (e m)) => Effect e where
  weave
      :: (Functor s, Functor m, Functor n)
      => s ()
      -> ( x. s (m x) -> n (s x))
      -> e m a
      -> e n (s a)
  default weave
      :: ( Coercible (e m (s a)) (e n (s a))
         , Functor s
         , Functor m
         , Functor n
         )
      => s ()
      -> ( x. s (m x) -> n (s x))
      -> e m a
      -> e n (s a)
  weave s _ = coerce . fmap (<$ s)
  {-# INLINE weave #-}

  hoist
        :: ( Functor m
           , Functor n
           )
        => ( x. m x -> n x)
        -> e m a
        -> e n a

  default hoist
      :: ( Coercible (e m a) (e n a)
         , Functor m
         )
      => ( x. m x -> n x)
      -> e m a
      -> e n a
  hoist _ = coerce
  {-# INLINE hoist #-}

defaultHoist
      :: ( Functor m
         , Functor n
         , Effect e
         )
      => ( x. m x -> n x)
      -> e m a
      -> e n a
defaultHoist f
  = fmap runIdentity
  . weave (Identity ())
          (fmap Identity . f . runIdentity)
{-# INLINE defaultHoist #-}

newtype Lift m z a = Lift
  { unLift :: m a
  }

data Tactics f n r m a where
  GetInitialState     :: Tactics f n r m (f ())
  HoistInterpretation :: (a -> n b) -> Tactics f n r m (f a -> Semantic r (f b))

start
    :: forall f n r r' a
     . Member (Tactics f n r) r'
    => n a
    -> Semantic r' (Semantic r (f a))
start na = do
  istate <- send @(Tactics f n r) GetInitialState
  na'    <- continue (const na)
  pure $ na' istate

continue :: Member (Tactics f n r) r' => (a -> n b) -> Semantic r' (f a -> Semantic r (f b))
continue f = send $ HoistInterpretation f

toH
    :: forall n f r r' a e
     . ( Functor f
       , r' ~ (e : r)
       , Member (Tactics f n r) r'
       )
    => Semantic r a
    -> Semantic r' (f a)
toH m = do
  istate <- send @(Tactics f n r) GetInitialState
  raise $ fmap (<$ istate) m

runTactics
   :: Functor f
   => f ()
   -> ( x. f (m x) -> Semantic r (f x))
   -> Semantic (Tactics f m r ': r) a
   -> Semantic r a
runTactics s d (Semantic m) = m $ \u ->
  case decomp u of
    Left x -> liftSemantic $ hoist (runTactics s d) x
    Right (Yo GetInitialState s' _ y) ->
      pure $ y $ s <$ s'
    Right (Yo (HoistInterpretation na) s' _ y) -> do
      pure $ y $ (d . fmap na) <$ s'
{-# INLINE runTactics #-}

freer mvp

@isovector

This comment has been minimized.

Copy link
Owner Author

commented Apr 8, 2019

after !668, -flate-specialise -O2 -fstatic-argument-transformation -fmax-simplifier-iterations=10:

Rec {
-- RHS size: {terms: 22, types: 132, coercions: 5, joins: 0/0}
main3
  :: ((forall x.
       Union '[State Int] (Semantic '[State Int]) x
       -> Int -> Identity (x, Int))
      ~R# (forall x.
           Union '[State Int] (Semantic '[State Int]) x
           -> StateT Int Identity x))
     -> Applicative (StateT Int Identity) => Int -> Identity (Int, Int)
main3
  = \ (sg_s6rY
         :: (forall x.
             Union '[State Int] (Semantic '[State Int]) x
             -> Int -> Identity (x, Int))
            ~R# (forall x.
                 Union '[State Int] (Semantic '[State Int]) x
                 -> StateT Int Identity x))
      (sc_s6rX :: Applicative (StateT Int Identity))
      (eta_B1 :: Int) ->
      case eta_B1 of wild_a5Hp { I# x_a5Hr ->
      case <=# x_a5Hr 0# of {
        __DEFAULT -> main3 @~ <Co:1> sc_s6rX (I# (-# x_a5Hr 1#));
        1# ->
          ((pure @ (StateT Int Identity) sc_s6rX @ Int wild_a5Hp)
           `cast` <Co:4>)
            wild_a5Hp
      }
      }
end Rec }
@isovector

This comment has been minimized.

Copy link
Owner Author

commented Apr 8, 2019

after keeping EVERYTHING + the simplcore changes:

Rec {
-- RHS size: {terms: 18, types: 6, coercions: 8, joins: 0/0}
main2 :: Int -> Identity (Int, Int)
main2
  = \ (s1_a6pN :: Int) ->
      case s1_a6pN of wild_a5Hp { I# x_a5Hr ->
      case <=# x_a5Hr 0# of {
        __DEFAULT -> main2 (I# (-# x_a5Hr 1#));
        1# -> (wild_a5Hp, wild_a5Hp) `cast` <Co:8>
      }
      }
end Rec }

-- RHS size: {terms: 17, types: 18, coercions: 4, joins: 0/0}
main1 :: String
main1
  = case (main2 (I# 100#)) `cast` <Co:4> of { (a_a2BS, b_a2BT) ->
    case b_a2BT of { I# ww3_a5Lf ->
    case $wshowSignedInt 0# ww3_a5Lf ([] @ Char) of
    { (# ww5_a5Lj, ww6_a5Lk #) ->
    : @ Char ww5_a5Lj ww6_a5Lk
    }
    }
    }

-- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
main :: IO ()
main = hPutStr' stdout main1 True

completely free abstraction :) :) :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.