The problem is: I can handle the effects of the alternative operator carefully since they may or may not be executed. If I simply add the effects of both terms (minus the early termination) then this code:
(empty >> pay) <|> return()
HasPaid as if this effect has been executed, and this is not the case. To make sure that
HasPaid is executed, i should demand that both terms have the same effects, so either one or the other term has
pay on it.
But thar is too restrictive, since
async... <|> waitEvents have somme common effects and some that are differents and the alternative operator would not type check.
orElsefor a relaxed alternative, besides the strict alternative
-- >>> :t async -- async :: IO a -> T '[Async, MThread] a -- -- >>> :t waitEvents -- waitEvents :: IO a -> T '[Streaming, MThread] a -- test = async (P.return "hello") `orElse` waitEvents (P.return "world") -- >>> :t test -- test :: T '[Maybe Streaming, MThread, Maybe Async] [Char] --
MThread (n :: Nat)and restrict the number of threads sub-processes can use)
orElse, no? Since the types will be either the first of the alternatives or the second.
asynclooked at whatever typelevel effects it had and then infered parameters to alter the expression, you get a bit further. Eg, using the
async = async' . maxThreads $ natval @n
singletonshas the general-case
withSomeSingthat allows you to determin any type at runtime, but it's covered over in an existential: https://hackage.haskell.org/package/singletons-2.7/docs/Data-Singletons.html#v:withSingI
FromSingpattern; that looks nice. It would be nice if you could leverage something similar to get the necessary guarantees on effects, though unless you want the user to have to match on the term level (proof) contained in
SomeSing, you'll probably have to encode things in cps.)
runAtis a cloud primitive that need the Logged effect in his argument. Some errors are informative other not as much
runAt :: (Loggable a, Member Logged effs ~ True) => Node -> T effs a -> T (effs <: Cloud) a test3= runAt node $ localIO $ print "hello" -- >>> :t test3 -- test3 :: T '[IOEff, Logged, Cloud] () -- -- case 1 above: correct: print (IO), local (Logged) and Cloud added -- case 2 below: need localIO instead of local or Expect a TransIO comp, not an IO comp (print "hello") test3= runAt node $ local $ print "hello" • Couldn't match type ‘IO ()’ with ‘TR effs Transient.Internals.TransIO a’ Expected type: T effs a Actual type: IO () • In the second argument of ‘($)’, namely ‘print "hello"’ -- case 3: since there is no Logged effect in "return "hello" :: T ' String, -- Member effs ' is False, not True test3= runAt node $ return "hello" • Couldn't match type ‘'False’ with ‘'True’ arising from a use of ‘runAt’ • In the expression: runAt node In the expression: runAt node $ return "hello" In an equation for ‘test3’: test3 = runAt node $ return "hello"
The problem with type level and alternatives is going well:
*Main> :t (liftIO (print "HELLO") >> async (P.return "hello")) <|> (waitEvents (P.return "world") ) (liftIO (print "HELLO") >> async (P.return "hello")) <|> (waitEvents (P.return "world") ) :: T '[IOEff, Async, Maybe Streaming, MThread] [Char]
Since print is before
async which fork a new thread and executes the alternative
waitEvents, the IOEff of print is annotated as executed for sure. both branches are multithreaded, therefore MThread is sure to be executed. In the other side Streaming is an efect only of
waitEvents so one of the first thread do not execute it, but the second does, so
Maybe Streaming is the most that can be said in the type.
Great. now I can express the pay-> sendStuff constraint:
data HasPaid data SentStuff pay ::Int-> T ' '[HasPaid]() pay i= undefined sendStuff :: T '[HasPaid] '[SentStuff] () sendStuff =undefined test5= liftIO (print "hello") >> (return "hello" >> sendStuff) test6= pay 10 >> test5 *Main> :t test5 test5 :: T '[HasPaid] '[IOEff, SentStuff] () -- test5 need the HasPaid effect, produces IOEff, SendStuff *Main> :t test6 test6 :: T ' '[HasPaid, IOEff, SentStuff] () -- test6 need no effect (since pay is included)
Now I can also codify get like the state monad:
get :: T [State a] ' a
keep :: Typeable a => T ' effs a -> IO (Maybe a) -- accept only computations with  requirements *Main> :t keep test6 -- OK keep test6 :: IO (Maybe ()) *Main> :t keep test5 <interactive>:1:6: error: -- does not type check since HasPaid is not present • Couldn't match type ‘'[HasPaid]’ with ‘'’ Expected type: Tnr '[IOEff, SentStuff] () Actual type: T '[HasPaid] '[IOEff, SentStuff] () • In the first argument of ‘keep’, namely ‘test5’ In the expression: keep test5
test8= do x <- choose [1..10] if x `rem` 2 == 0 then empty else liftIO $ print x *Main> keep' test8 2 4 6 8 10
This program only print the even number since the odd numbers are filtered by if-empty. The threads created by choose, one for each number, stop at
guard when they carry an odd number. The type of this program could be like that:
test8 :: T ' '[Async, MThread, Streaming, Maybe EarlyTermination, IOEff] ()
Maybe EarlyTerminationsince some threads terminate and others don't
for this purpose, in the new type-level transient, the type of empty is
empty :: T '  '[EarlyTermination] a
But this is also a problem since both branches of ifThenElse should have the same signature. Since
print x has type
T ' '[IOEff] (), the program does not type match. So it is necessary to use guard instead.
guard :: Bool -> T ' '[Maybe EarlyTermination] () test8= do x <- choose [1..10:: Int] guard $ rem x 2 == 0 liftIO $ print x
This programs actually type match and has the type desired.
In the other side:
test9 = do test8 empty Main> :t test9 test9 :: T ' '[Async, MThread, Streaming, EarlyTermination, IOEff] b
That is, since
empty guarantees that test9 stop for all the threads, then
test9 terminates. So the Maybe of test8 is supressed
So far so good. I renamed the long name