Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Tim Pierson
    @o1lo01ol1o
    You'll probably need something like
    data AKnownEffect a where 
        FooE :: AKnownEffect Foo
        BarE :: AKnownEffect Bar
    
    appendEff :: T es a -> AKnownEffect e -> T (e':es) a
    Tim Pierson
    @o1lo01ol1o
    or
    type family AppendEffect es e where 
        AppendEffect es e = e:es
    
    reteff :: forall e a. a -> T (AppendEffect [] e) a
    
    >>> reteff @EffectFoo foo
    Alberto
    @agocorona
    Tanks!
    Alberto
    @agocorona

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

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

    Tim Pierson
    @o1lo01ol1o
    IIUC, you would need proper dependent types to handle that case. You could potentially do it so long as the Haskell expression is handled in an existentially quantified continuation, but even then you wouldn't know statically (ie, compile time) if something paid or not.
    Alberto
    @agocorona
    I created this hack orElse for 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]
    --
    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