Replies: 2 comments
-
Just for reference, this is partially discussed in section 2.3 of this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf |
Beta Was this translation helpful? Give feedback.
-
So this is the issue that presents itself with your suggestion.
If both e1 and e2 contain The type signature is not "wrong" because effect types just mention which handlers are in the dynamic scope and could be used by the function argument. It doesn't say which effects are definitely used. Therefore the @chtenb Great find on the paper section, I'm glad it is documented somewhere that function types in arguments should by default have the same effect row (I believe there is an exception to this rule if it has duplicate effects or is under a mask or overridden handler). We should document that more clearly for sure. Potentially we could surface a better error message as well if there is no mask (though this might require a transitive search of all called functions if the function argument is propagated - which might make this less feasible). |
Beta Was this translation helpful? Give feedback.
-
In the documentation S 3.2.3 of the book, there is a discussion of polymorphic effects on while.
I am new to Koka, but i am struck that something may not be exactly straightforward with the typing for effect extensions.
There is a discussion in this section of how in
while
, that while the reader may be worried, that the effect types ofpred
andaction
ultimately unify, but i am worried that user types don't then match reality.I am curious if you have already considered having user make explicit in the effect types of
while
thatpred
andaction
can have distinct effects. You would then require some kind of merging, which would i guess look more complicated, but i feel like it would ultimately be simpler for the user. I don't know what would be a good merging syntax, but you could make it explicit that you are merging the effects e1 and e2. Something like:while : ( pred : () -> <div|e1> bool, action : () -> <div|e2> () ) -> <div|e1+e2> ().
or maybe just
while : ( pred : () -> <div|e1> bool, action : () -> <div|e2> () ) -> <div|e1|e2> ().
I don't know how good either of these would actually be, but you get the idea.
Am i missing something or do others agree the types seem "wrong"? The reason they seem wrong is because the actual type signature of while doesn't reflect that the
e
ofpred
and thee
ofaction
are different. And because, if as a user i unify that in my head, i would think that bothpred
andaction
would then have the same fully merged input type as the result type of while. Does that match reality? Are the effect types of the args truly unified to be the same as that of the result?Wouldn't it be more clear if the types reflected the reality of the possibly different effects? Could this not be made simple? Could it not be better for the type system to make this explicit?
Again, i am new so i may be missing something. But i thought i would add my 2c in case it is indeed a bit off and you are considering comments.
Beta Was this translation helpful? Give feedback.
All reactions