Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Alberto
    @agocorona
    assigns Maybe to the effects that are not present in both sides
    Tim Pierson
    @o1lo01ol1o
    That might get you somewhere, although I think you may need a type-level Maybe to correctly pattern match via a type family
    in general, i'm not sure where this model of effect tracking will fall down since it relies on the ad-hoc assurances and not term-level proof, but certainly worth exploring (and those types help with documentation quite a bit -- you could add a phantom type to MThread (n :: Nat) and restrict the number of threads sub-processes can use)
    It also looks like you may actually want an Either for orElse, no? Since the types will be either the first of the alternatives or the second.
    Alberto
    @agocorona
    About the latter, the problem si that I'm not sure where is empty in the first expression, so it can execute half of the effects of the first therm and all of the others, or execute all of the first term and none of the other etc
    What do you mean by term-level proof?
    Tim Pierson
    @o1lo01ol1o
    Well, using reteff @EffectFoo foo, anyone can add or remove effects from the list as they want and it wouldn't change the runtime semantics of the expression.
    on the other hand, if async looked at whatever typelevel effects it had and then infered parameters to alter the expression, you get a bit further. Eg, using the MThread 3 : async = async' . maxThreads $ natval @n
    Alberto
    @agocorona
    that was a question that I was to ask to you, how to promote a value to the type level.
    Tim Pierson
    @o1lo01ol1o
    going from type-to-term is not hard, see natVal in typelits
    Alberto
    @agocorona
    I tried to define reteffas an internal hack because the problem with <|> Now I think that I do not need it.
    Tim Pierson
    @o1lo01ol1o
    going from term-to-type -- reification -- is, except when there's some magic; see https://hackage.haskell.org/package/reflection-2.1.6/docs/Data-Reflection.html
    singletons has the general-case withSomeSing that 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
    Alberto
    @agocorona
    :thumbsup:
    Tim Pierson
    @o1lo01ol1o
    (Also, I just noticed the FromSing pattern; 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.)
    Alberto
    @agocorona
    I have a "metaexpression" problem: when a programmer needs to sum their custom effects, for example in the case of thereads, two terms that use n threads and another m threads, I can change my definitions to do that, but the programmer that uses the library can't.
    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.