Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Alberto
    @agocorona
    I think that I need to try one more attempt to implement the type-level layer. I didn't came back to it since @o1lo01ol1o gave me some type level set skeleton that I needed for that. I'm looking for it. Until then I used type level set from Dominic Orchard that was difficult to extend.
    Alberto
    @agocorona
    Now transient calls between nodes bypass HTTP proxies! This is very important for WAN networks. Probably this is one of the first distributed systems that do so. The code is in the transient-stack repo.
    I need to fix the TLS option for secure communications which appears to be broken in that repo.
    Alberto
    @agocorona
    Now that is fixed.
    Now transient nodes can communicate across HTTP proxies and manage proxy authentication as well as secure TLS communications, so NASA, now you can type check your interplanetary communications:
    Alberto
    @agocorona
    To use a proxy, just set the environment variables:
    > export http_proxy=http://user:password@host:port
    > export https_proxy=http://user:password@host:port
    Alberto
    @agocorona
    I'm now doing some tentative implementation of the cloudshell language
    Alberto
    @agocorona
    image.png
    That effect system is awesome. https://www.youtube.com/watch?v=yicXcdLI2YA
    Alberto
    @agocorona
    Seeing that effect system, the closest that Haskell can go is something like my type-level effects since at least there are no lift-run cluttering
    Although the implicit applications and the non distinction between pure and efectful terms in Unison are not possible to achieve in Haskell. Now I understand the efforts of Conor McBride with the idiom brackets to make applicatives implicit.
    The problem is that a and m a do not type match in Haskell
    Alberto
    @agocorona
    image.png
    Alberto
    @agocorona

    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
    All the primitives use the same monad T, in contrast with transient, which use different monads: TransIO, Cloud, Widget, StateIO..
    Tim Pierson
    @o1lo01ol1o
    :100:
    @agocorona Is the type-level effects stuff integrated into transient-universe?
    Alberto
    @agocorona
    @o1lo01ol1o It is a fine layer over the transient libraries, with only type level definitions, no runtime code. My idea is to make it a drop-in replacement so the programmer can use it optionally with the same code (with the exception of the type signatures)
    I don't know I adding modules to the current packages or making a new package
    Tim Pierson
    @o1lo01ol1o
    kk; when you do decide and it's useable, can you point me to it? this covid buisness has everything out of whack but I'd like to look at doing something
    Alberto
    @agocorona
    Sure.
    Alberto
    @agocorona

    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.

    Alberto
    @agocorona

    @o1lo01ol1o a question: I need to creata a return that include some effect. sort of:

    reteff    ::  a -> (eff :: [*]) -> T eff a

    but it complains with:

    • Expected a type, but ‘(eff :: [])’ has kind ‘[]’
    • In the type signature: reteff :: a -> (eff :: [*]) -> T eff a

    Alberto
    @agocorona
    Ok I found a workaround
    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