by

Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Tim Pierson
    @o1lo01ol1o
    setMaxThreads :: T effs -> T (SetMaxThreads effs)
    Alberto
    @agocorona
    What is the type of setMaxThreads 5 foo >> setMaxthreads 6 bar?
    Tim Pierson
    @o1lo01ol1o
    depends on how you implement it ;)
    Alberto
    @agocorona
    I defined :++ that aggregate the effects, and I could add rules to sum SetMaxThreads n and m. But external programmers could not do for their effects. That's what I meant
    Tim Pierson
    @o1lo01ol1o
    if you wanted to use the reflect trick, probably MThreads 6 would be the desired value in the return T effs?
    Alberto
    @agocorona
    reflection is important. There are primitives that have meaning only if the argument is a multithreaded computation like collect
    Alberto
    @agocorona
    runAt is 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 typeIO ()
                     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"
    Alberto
    @agocorona
    The third case says that runAt has a check for some condition that does not meet. Not entirely bad message
    Tim Pierson
    @o1lo01ol1o
    @agocorona You might see here for some ideas on making those type errors more informative: https://github.com/hasktorch/hasktorch/blob/91f1a1c2ad0e4c92c4a1fc8eb91a82a1cb2a9bc3/hasktorch/src/Torch/Typed/Aux.hs#L45
    Alberto
    @agocorona
    :thumbsup:
    Alberto
    @agocorona

    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.

    Alberto
    @agocorona
    @o1lo01ol1o I uploaded it as I have it now https://github.com/agocorona/tltransient
    The test.hs contain some expressions that I'm testing
    Tim Pierson
    @o1lo01ol1o
    :thumbsup:
    Michał J. Gajda
    @mgajda
    @o1lo01ol1o Nice to see that the work progresses here :-).
    @o1lo01ol1o I saw that you stopped responding to me on private channel. Is it something I said about money?
    Tim Pierson
    @o1lo01ol1o
    @mgajda No, gitter just gets closed and some of the messages fall through the cracks; keybase is useually better
    Michał J. Gajda
    @mgajda
    @o1lo01ol1o I am also available on Keybase. Indeed it seems better. I am a bit scared after I heard the news that Zoom took them over.
    Tim Pierson
    @o1lo01ol1o
    Yes, I know, it's a bit worrying
    Alberto
    @agocorona
    I have to include a second set of required effects:
    T (required ::[*])  (produced ::[*]) a
    Alberto
    @agocorona

    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
    since
    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 presentCouldn'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
    Alberto
    @agocorona

    So sendStuff could not be executed without payment.

    (Tnr eff x is an shorthand for T '[] effs x. Probably I will remove it)

    Is that nice and useful or what?
    Alberto
    @agocorona
    So a software component can publish the effect required and the effects that it produces, and it cannot compile until all required effects have been given.
    Alberto
    @agocorona
    That is what I was looking for since the beginning. Not a mere description of what each program does, but some way to let the compiler verify the requirements that each programmer can use in his domain problem.
    Alberto
    @agocorona
    image.png
    Alberto
    @agocorona
    Uploaded the last version with required effects
    Alberto
    @agocorona
    I added more modules. The idea is to have a typelevel module for each transient module
    Alberto
    @agocorona
    One of the main problems in transient is to know if block of code continues or not, since the execution can be stopped at any moment. Moreover, since the transient is inherently multithreaded and single threading is just a particular case, some threads can follow a path in which they stop and other don´t.
    Alberto
    @agocorona

    For example

    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] ()

    It has 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 Earlytermination to Terminates

    Alberto
    @agocorona
    or perhaps "Stop" instead
    Hugh JF Chen
    @hughjfchen

    One of the main problems in transient is to know if block of code continues or not, since the execution can be stopped at any moment. Moreover, since the transient is inherently multithreaded and single threading is just a particular case, some threads can follow a path in which they stop and other don´t.

    I must admit that this is the most confusing problem I'd been facing since the first time I met transient. So a type level safety is really welcome and necessary

    Alberto
    @agocorona
    I suspect that if-then-else expressions with monadic code will no type-match in many cases when using this library.
    Alberto
    @agocorona

    For example:

    test10 x= if x == 5 then liftIO $ print x else askfornumber
    
    askfornumber= do
          n <- input (<10) "give me a number >"  
          liftIO $ print (n :: Int)

    The error produced at the else :

    src/Transient/TypeLevel/test.hs:41:48: error:
        • Couldn't match type ‘Terminal’ with ‘IOEff’
          Expected type: T '[] '[IOEff] ()
            Actual type: T '[] '[Terminal, IOEff] ()
        • In the expression: askfornumber
          In the expression:...

    because the "then" side has type T '[] '[Terminal] () since it uses terminal input, while the "else" side uses IO. Since both branches should have the same type, hence the error.

    To solve the problem, the best way I found until now is to use guard in combination with alternative, which is IMHO, a good style that improves readability:

    test11 x=  is5 x <|> askfornumber
     where
     is5 x=  do guard $ x==5 ; liftIO $ print x

    This type check. What is the signature? A mess of Termination-maybe-non-termination?
    Using GHCI:

    *Main> :t test11
    test11
      :: (Eq a, Num a, Show a) => a -> T '[] '[IOEff, Terminal] ()

    The type adds the two effects. The same type that the if-then-else expression would have if it would type-check.

    Termination is wiped out since <|> has been redefined under the "RebindableSyntax" extension to cancel any Termination effect of the first term

    Alberto
    @agocorona

    Ooops... No. That latter type is not good, since I can cheat the compiler telling that I paid when I don't:

    (do guard False; pay) <|> sendStuff

    This is the same old problem that I had with "empty" and alternatives, now appears again with "guard".

    Alberto
    @agocorona
    After some type-level list processing, the type of test11 is the desired:
    *Main> :t   test11
    test11
      :: (Eq a, Num a) => a -> T '[] '[Maybe Terminal, Maybe IOEff] ()
    Alberto
    @agocorona

    I told that one of the requirements is to allow the definition of contraints between effects defined by the programmer like the pay-> sendStuff ordering.But these are a zero level kind of requirement.

    Even though I thought it couldn't be possible, it's possible to give the programmer detailed control of invariants of the domain problem using self-defined effects by making use of the rebindable syntax, so that the programmer can redefine the monadic,applicative etc operators using the already defined operators as base:

    {-# LANGUAGE RebindableSyntax, TypeFamilies, TypeOperators,DataKinds,RankNTypes, ScopedTypeVariables #-}
    import  Prelude  hiding ((>>=),(>>),return,concat)
    import qualified Prelude as P 
    import qualified Transient.TypeLevel.Effects as Eff
    import Transient.TypeLevel.Base 
    import Transient.TypeLevel.Move
    import Transient.TypeLevel.Indeterminism
    ...
    -- Transient.TypeLevel.Effects has >>= redefined using  rebindable syntax too
    data MyEffect1
    data MyEffect2
    ....
    
    -- my own bind ,  for my problem, with more effects rules defined by me. 
    -- He can use the rules already defined in the Eff module to manage effects to sum, subtract, 
    -- test inclusion etc
    
    -- In this case, not redefined
    
    (>>=) = (Eff.>>=)
    Alberto
    @agocorona
    I'm using transient in a project with web services and I spent some days dealing with timeouts and reconnections in HTTP/1.1 with TLS. and also an obnoxious bug with the interpretation of the command line parameters. In certain precise circumstances and with some parameters these problems produced so crazy outputs that made me think that I was dealing with some fundamental flaw of the execution model.
    At the end I was just a matter of bad management of two varables and some unnecessary complications in the code.
    I learned one thing or two. The HTTP code is producing more headaches than anything else in transient. I will upload a new version as soon as I can.
    Alberto
    @agocorona
    watched the superb talk of alexis king about performance and effects.
    Alberto
    @agocorona

    This talk inspires me some considerations about effect systems, continuations and performance:
    I wanted continuations to be given by the runtime instead of in programmer space in a continuation monad. In fact I worked in ETA to redefine it so that the IO monad delivers it. That was my dream since many effects are not possible without continuations. But having continuations as a monad in a monadic stack add extra complexity and extra performance loss.

    I tried to define transient so that the primitives are independent of how the effects are implemented, as long as they provide state and continuations over Applicative/Alternative/Monad instances. In fact I have two different engines. The second one uses a different continuations monad and exceptions to implement the Alternative instance. When the patch of Alexis become available, the translation of transient to wathever monad that uses it is relatively straigforward.

    Alberto
    @agocorona
    In the meantime, The current monad does not add a lot of boilerplate. The monad implements continuations maintaining a stack of bind parameters which is lazily constructed and discarded when not used. It is possible to use noTrans, to use the underlying monad, when I write ordinary code without async, empty, react or distributed computing. The bind in this case is as fast as one of the ordinary state monad. What may be slower is getState and setState. It is the price to pay for the flexibility of intruducing and retrieving any variable state at any moment, as many of them as you please, without recompiling/redefining/adding instances runners and/or handlers anywhere in the rest of the modules that may be involved. However that performance of state is similar to the best of the extensible record libraries i guess.
    Alberto
    @agocorona
    To handle many states is the main chore of monadic stacks and effect systems. since the rest of the effects have limited number of them, but states can be unlimited. However in Transient the need of state is drastically reduced, since basically data is in scope in the form of ordinary variables:
    let  x=  MyData.....
    y <-  multireaded,distributed,streaming...
    --   x still in scope! (even if now it is in a different machine!!)
    Alberto
    @agocorona
    Concerning effects, there are different views of what an effect is:
    • In effect libraries, an effect is associated with an interpreter/handler which is called when the effect is needed
    • In Final Tagless/MTL libraries, they are monad transformers in a stack.
    • In libraries like RIO they are class instances that group methods.
    • In Transient, in the type-level transient that I'm developing, effects are salient features of the computation
    Alberto
    @agocorona

    The first three can aggregate effects in the type signature and this is good for documentation purposes and to tell the type system what and how the runners and lifters should be inserted in the code to make it type match.

    I think the main functionality of type-level lists of effects in effect libraries is to make type signatures less ugly than monad transformers and to make sure that the runner of each effect is present. and Oleg Kiselyov designed them originally for that purpose. In the case of MTL, the monadic stack signatures are a consequence of his very structure, and in the case of Has.... strategy, it is intended for documentation purposes, to make the program more readable.

    In Transient since the effect can be created with a simple data declaration without runtime representation, they can be used to check the compliance of domain-specific requirements at compile time using type-level logic, as the examples written here above detail.

    Alberto
    @agocorona
    In transient any other effect can be created by the combination of the already existent. I don't provide a reader of writer effect since getRData/setRData is equivalent to the reader/writer effects.
    Alberto
    @agocorona
    I have to create a table of how-to-do features based on https://www.47deg.com/blog/io-haskell/
    Alberto
    @agocorona
    I defined whileException:
    -- re execute the first argument as long as the exception is produced within the argument. 
    -- The second argument is executed before every re-execution
    -- if the second argument executes `empty` the execution is aborted.
    
    whileException :: Exception e =>  TransIO b -> (e -> TransIO())  -> TransIO b 
    whileException mx fixexc =  mx `catcht` \e -> do fixexc e; whileException mx fixexc
    the IO version would be exactly the same, but using catch instead of catchc.