m ado not type match in Haskell
It seems that the type level stuff finally works, thanks to the new type-level list from @o1lo01ol1o .
It does most of what I was looking for:
Above, the IDE infers correctly the type of
test: It has two states (Int, and String) It handles SomeException exceptions, it can terminate early (since it uses empty), perform IO, do streaming (because waitEvents) and it is multithreaded.
It also has subtle effect cancellation rules. For example, EarlyTermination is cancelled by the operator
test2 = getState <|> return (0 :: Int) -- >>> :t getState -- getState -- :: Typeable a => -- T '[EarlyTermination] a -- -- >>> :t test2 -- test2 :: T ' Int
I can force the compiler to check for the presence of an effect. for example,
runAtwould not compile if his argument is not logged and notifies that it is a cloud computation:
runAt :: (Loggable a, Member Logged effs ~ True) => Tr.Node -> T effs a -> T (effs <: Cloud) a
I'm still testing for some improvements and completing the definitions
One really cool thing of this system , in my opinion, is the really low cost for creating custom effects in order to control invariants of the domain problem effectively.
data HasPaid pay :: T '[HasPaid,IOEff,BlaBlaBlah...]() pay.... sendStuff :: (Member HasPaid effs)=> Address -> T '[IOEff,.....] ()
This would type check
do pay ... ... sendStuff
But if pay is not present before sendStuff that would produce a compilation error
This has even more value in Transient, since the execution can span across different computers. It can support shutdowns and restarts, so
sendStuff can execute in a remote computer some time after. Maintaining the paid flag in a single database and make programmers aware of that requirement are the kind of problems that can be eliminated.
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"