I'm splitting this reply into two emails, one for a debate about monadic effects, one for everything else. This one is the "everything else".
On Sun, Feb 15, 2015 at 9:42 AM, Keean Schupke <[email protected]> wrote: > On 15 Feb 2015 10:34, "Matt Oliveri" <[email protected]> wrote: >> On Sun, Feb 15, 2015 at 4:24 AM, Keean Schupke <[email protected]> wrote: >> > Hmm, I don't see the issue, nothing here has required local aliases so >> > far, >> > but lets say I do: >> > >> > import f :: ('a -> 'a -> 'a) -> 'a -> 'a -> 'a as (('a ,'a) -> 'a, 'a) >> > -> 'a >> > >> > I could then use it with a 'g' with the type ('a, 'a) -> 'a locally in >> > this >> > module. >> >> ((('a ,'a) -> 'a, 'a) -> 'a) doesn't look like isomorphic to (('a -> >> 'a -> 'a) -> 'a -> 'a -> 'a). Your type of function only gets one 'a. >> Maybe you meant ((('a ,'a) -> 'a, 'a) -> 'a -> 'a). > > I actually meant: > > (('a, 'a) -> 'a, 'a, 'a) -> 'a > > OR, more correctly, as not I think about it, a datatype more correctly > represents the semantics, and allows us to distinguish arity from tuples. > > 'a -> 'a -> F ('a -> 'a -> 'a -> F 'a) *Sigh*, that's like ('a,'a)->('a,'a,'a)->'a . You mean ('a->'a->F 'a)->'a->'a->F 'a ? I understand what you're thinking with that, but it seems too Haskell-ish for BitC. To think that a function application that doesn't yield an instance of F is not really a function call probably would seem like complete bull crap to systems programmers. It does fit very well with monadic effects though; I'll grant you that. Keep in mind that if you want the F convention to be doing anything, you'll have to forbid partially applied F's that escape. There are other ways to distinguish arity from tuples if necessary. Ad-hoc syntactic rules would actually be preferable, since you know it won't interact with the rest of the type system. >> But anyway, that's the opposite of what I'm asking for. You are >> showing me how to make f look like a different type than from its >> definition without actually changing the way the definition is >> compiled. I want to know how you'd get the compiler to implement it as >> if it had the type ((('a,'a)->'a,'a)->'a->'a), so that g has arity 2. >> (And apparently, f has (2,1) while we're at it.) > > You can do it both ways. Curried to un-Curried, or un-Curried to Curried. That's what I figured. >> Is your answer to write f like >> >> def f(g,x) y = g(x,y) > > would be f :: ((a, b) -> c, a) -> b -> c Oops. Well, you know what I mean. >> > I need >> > to think about this some more as there are other reasons to make >> > function >> > calling explicit verses a value. IE a unary function needs to be >> > distinguished in the type system from a value. >> >> BitC will be eager evaluating. A _nullary_ function needs to be >> distinguished from a value. Probably with unit, if we're using tuples. > > The way I am now proposing an int value would be: > > f = (13 :: Int32) > > a nullary function (note the name of the Datatype 'F' is entirely > arbitrary): > > f = (13 :: F Int32) > > of course you now need to 'deconstruct F' to get the value. Deconstructing > the datatype is when side effects happen. Yep. Got that. >> > In Haskell this would be done >> > with a datatype. Lets just say we have a datatype 'F' for function >> > application the above can be: >> > >> > h :: int32 -> int32 -> int32 -> F (int32 -> int32 -> F int32) >> > >> > This is probably my preferred solution as F captures side effects too, >> > leaving the function arrow '->' as a pure function. We can then make 'F' >> > a >> > monad to allow composition of function application. We might call this >> > monad >> > 'IO'? >> >> Whether to use monads for effects is another issue that really seems >> quite separate to me. > > Actually it is closely tied to the arity question. Haskell (and type systems > for pure languages) have pure 'arrows' in types, this means a nullary > function is indistinguishable from a value. If you want side-effects to > occur only when the function has all necessary arguments, then you do not > want impure arrows, instead you need a special arrow to mark where side > effects can occur, consider: > > a -> b > > a -> F b > > the first is a pure arrow, the second we can consider the side effects occur > in the 'deconstruction' of F. You are telling this stuff on the wrong mailing list. We know how Haskell works. As for the connection to arity, you didn't elaborate on that until much later so the reply is in the other email. > In a 'C' function call f() the '()' represent the function call, so we could > call the datatype for impure function evaluation '()' in which case we would > get a type like: > > data Fun a = Fun {call :: a} > > a -> Fun b > > test = Fun 123 > > value = call test > > > Of course some syntactic sugar would help make this nice. That's silly. There's no point in wrapping a value in Fun if you can just take it back out. Fun would have to be a monad, and arrows would have to be pure, otherwise this isn't doing anything. >> While I'm on monads, I think for the first time on this list, I'd like >> to say that I don't like the point of view that effects are _just_ >> certain monads. They can be modeled with certain monads, but they're >> special, because the purpose of effects is to expose some subset of >> the functionality of one particular monad: the IO monad. IO is the >> "true" monad which gives you all the stuff your computer can do that >> Haskell left out. Effects hand out pieces of that power in a more >> fine-grained way. But monads in general have nothing to do with the IO >> monad in particular. > > Hmm I'm not sure I get what you are saying. Effects are things that happen, > we can model these in the type system by using special datatypes. Those > datatypes happen to have the structure of category theoretic monads. There > is nothing to like or dislike, the structure fits the pattern whether you > like it or not. Yes I know. That's kind of what I was trying to say, phrased differently. What I don't like is when people think facts about effects will generalize to all monads, or think monads and effects are competing alternatives. These are both naive opinions that do not appreciate the generality of monads. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
