Today should be my last day of household wiring, but I'm afraid it will be another day of fitful replies.
On Sun, Feb 15, 2015 at 2:17 PM, Keean Schupke <[email protected]> wrote: > > f :: a -> b -> Eff e a > > Eff is a special datatype that represents 'effectful-function-call' as > such it is the deconstruction that actually makes the call. The unit > construction just injects the return value 'a' into the datatype. 'e' is a > phantom type representing the effects inferred. > OK. Let's see if I can muddle my way through to understanding this. First, let me note in passing that I saw your comment in the non-SPAM sub-thread concerning type-level sets. I'd like to take up set types and type-level sets separately, and I think that has little bearing on the present discussion. Unless there is some reason not to do so, I will assume for this discussion that there are two possible values for /e/: NoEffect and SomeEffect. So first, let me confirm my reading of this syntax. I think it reads (approximately) as "f is called with two arguments, with the consequence that effect /e/ occurs and a return value of type /a/ is returned. Q1: if I thought about this in the more conventional region and effect typing style, wouldn't the /e/ be decorating the arrow? Isn't this really just an odd way of annotating the arrow? [Read below before responding - I now think your answer must be "no"] Q2: Do I actually (syntactically) have to un-wrap this construction at the return point? I'm concerned that we just turned essentially all function calls into "(f a b).value" [having read further, I think you really intend the deconstruction to be explicit] If we accept all side-effects with no distinction (like Haskell's IO monad) > we can remove the 'e' parameter to leave something like: > > f :: a -> b -> Fn a > > As you can see there is not a 'Fn' on the right of every arrow, only the > one where side-effects (the actual function is called). > So actually I *don't* see that, but I'm probably just confused here. As you have talked about this idea, you have used phrases similar to the one above "where side-effects (the actual function is called)" I'm not clear whether you are using "side effect" in the conventional sense that something has been mutated. I could read your text to mean that the mere performance of the call is the side-effect you have in mind. It seems to me that there are some arrow annotations of interest that are not side-effects, but that most naturally seem to "fit" in the place where an effect annotation would be expected. Are you saying that a return value like "Eff e a" would ONLY appear on procedures that perform some effect of interest /e/, and then an "effect free" procedure would merely return /a/ without the effect wrapper? That won't work, because if we do that, we will be unable to discern the native arity of non-effecting functions. Consistency would seem to suggest that a non-effecting function should return "Eff {} a", where I intend {} to be read as "the empty set". That notation for sets won't work, but it will suffice for now. Part of my (still ignorant) concern here is that systems programs tend to have lots and lots of impurity, so a solution that requires explicitly unwrapping results is syntactically unacceptable. What I *do* like about this idea is that it's giving us the beginnings of a notation to use to describe effects. Even if it turns out that *this* isn't the right notation, we clearly need *some* notation, and it's a lot easier to relocate a notation you have already worked out than it is to come up with a capturing notation in the first place. > In this case it indicates that both arguments 'a' and 'b' must be > accumulated before the call can be made. The call can be explicit, for > example: > > data Fn a = Fn {call :: a} > > call (f x y) > > Of course you can have syntactic sugar for this. > I am not certain what you mean here by "the call can be explicit". What do the two notations above actually do? This allows us to distinguish between tuples and calling. Consider the > differences between: > > > f :: a -> b -> Fn a -- curried > g :: (a, b) -> Fn a -- pass a tuple > h :: a -> Fn (b -> Fn a) -- multiple calls / explicit partial evaluation > > In all cases arguments are provided / accumulated, but the final nullary > function is not evaluated until the result datatype is deconstructed. In > this model the function is a sequence of pure operations and all the > impurity is in the the datatype deconstruction. > OK. I'm now convinced that you *are* using the term "side-effect" in the traditional way, because you now emphasize that impurity occurs as a consequence of the deconstruction. In which case, I'm sorry, but no, this is not solving the problem we need to solve. It is very interesting to me as a possible way to record effects that I had not previously considered, but it isn't doing anything to solve the native arity and calling convention problem, and it is failing to do so for a very simple and clear reason: We need to solve the arity problem whether the function has effects or not! If I am understanding your proposal, you are conflating two completely unrelated things. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
