Sometimes it might be better to read my responses in reverse order :-) I have realised the folly of my ways and agree that I was (kind-of) conflating two things. Actually when side - effects occur is relevant in the curried case, with a curried arity-N function side effects should only occurs after all N arguments have been supplied, as you cannot reorganise code imported from another module or foreign language. The other applications will be pure, but that doesn't deal with functions where you want all arguments at once in an uncurried way.
After considering the options (including monadic ones, sorry about having that discussion, but I don't mind starting it again elsewhere) I think representing that the arrow actually has multiple left arguments, that are not curried or tuples leads to a syntax like this: f :: a, b, c -> (b, c), a -> a -> b Arities (3, 2, 1) Keean. On 16 Feb 2015 14:26, "Jonathan S. Shapiro" <[email protected]> wrote: > 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
