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
    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.
    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.