> > > def f(g,x) y = g(x,y) > would be f :: ((a, b) -> c, a) -> b -> c > OR > f :: ((a, b) -> F c) -> b -> F c
Of course I meant: f :: ((a, b) -> F c, a) -> b -> F c Keean. On 15 February 2015 at 14:42, Keean Schupke <[email protected]> wrote: > > On 15 Feb 2015 10:34, "Matt Oliveri" <[email protected]> wrote: > > > > Now we're getting somewhere. Just a few questions left. > > > > On Sun, Feb 15, 2015 at 4:24 AM, Keean Schupke <[email protected]> wrote: > > >> As defined, the inferred type of f is ('a -> 'a -> 'a) -> 'a -> 'a -> > 'a. > > > > > > f is a function passed a function and returning a function that takes a > > > single argument and returns a function taking a single argument and > > > returning a value, so native arity (1, 1, 1) > > > > > > The first argument is a function that takes a function and returns a > > > function that takes a value and returns a value (1, 1). > > > > I'm assuming you meant "takes a value and returns a function that > > takes a value and returns a value". I don't really know why you're > > spelling it out it English. > > Because I want to make sure we agree the meaning of the notation. > > > > > > >> When f is called from another module, what native arity must a closure > > >> be in order to safely pass it to f? > > > > > > It must have arity (1, 1)... i.e. a function which takes a single > argument > > > and which returns a function that takes a single argument (all of type > 'a). > > > > >> What native arity is assumed of the parameter g when compiling f? > > > > > > (1, 1) as described above > > > > >> Note that the answers to the above two questions must be the same, but > > >> one answer must come from the compiler of a module importing f, and > > >> one must come from the compiler of the module defining f. > > > > > > Here's where you lose me. We have already said all type signatures at > module > > > boundaries should be explicit, due to the desire for a stable > interface. In > > > any case, in one module you would say: > > > > > > export f :: ('a -> 'a -> 'a) -> 'a -> 'a -> 'a > > > > > > In the other module you would say: > > > > > > import f :: ('a -> 'a ->'a) -> 'a -> 'a -> 'a > > > > > > If these are different it is a link-time error, not a compile time > error. > > > > So in this case, no tuplization/uncurrying/whatever occurs. So of > > course then it works. > > > > >> How does your scheme ensure that these answers will always be the > same? > > > > > > It doesn't mismatch is a link time error, but libraries can provide > 'import' > > > header files to make sure users get this right and don't have to type > it all > > > in. > > > > Or something like that. But again, since nothing really happened in > > this example, it really is just comparing the surface types. > > > > >> And finally: > > >> In your scheme, what does the programmer do to control the native > arity of > > >> g? > > > > > > 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) > > > > > 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. > > > > > Is your answer to write f like > > > > def f(g,x) y = g(x,y) > > would be f :: ((a, b) -> c, a) -> b -> c > > OR > > f :: ((a, b) -> F c) -> b -> F c > > because we want to note the 'arity' rather than the argument grouping. > > > > > and then maybe say something like "But use it as > (('a->'a->'a)->'a->'a->'a)."? > > > > >> >> Anyway, how is this business of using different inter-module types > any > > >> >> better than using an arity-aware type system for compiled modules, > or > > >> >> automatically tuplizing functions under the hood? > > >> > > > >> > Hmm, the type system is arity aware, the exact arities are encoded > in > > >> > the > > >> > types using tuples. > > >> > > >> OK, I can use that point of view. The comparison I was asking for is > > >> essentially the same, whether you use arities or unboxed tuples under > > >> the hood. > > > > > > Well I could imagine a third syntax for arities like: > > > > > > h :: {int32, int32, int32} -> {int32, int32} -> int32 > > > > > > but it ends up looking just like tuples, and for unboxed tuples the > stack > > > representation would likely be the same. However if you want to allow > > > unboxed tuples, it might be necessary to have something like this... > > > > Whether we want to treat multi-arg as different from unboxed tuples is > > independent of how we pick native arity. It looks like Shap is leaning > > towards using unboxed tuples exclusively. > > I am now leaning towards marking arity in the type signature using a > datatype allowing tuples to represent something more like 'C' structs. > > > > > > > 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. > > > > > > 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. > > 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. > > > > > 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. Then the question is, if you have a general mechanism > for modelling things that effects behave like, why would you introduce > another mechanism into your type system. In my experience simpler, generic > things produce better, simpler type systems. Parametric Monads use > parameter sets to mark effects in exactly the fine-grained way you > describe. You should read this: > > http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf > > > > > The difficulty of composing monads might be due to the huge amount of > > extra generality of monads over effects. The problem of composing > > monads in general is not a problem for BitC, AFAICT. > > Parametric monads solve a lot of the composition problems. Again monads > are simply a category, a bunch of things with similar properties that are > abstracted into a common pattern. If you don't allow the common pattern to > be expressed, then you will have to write boilerplate for each thing. > > > > > > I don't see any reason why you couldn't do concurrent programming in > > the IO monad. But I also don't see any reason why BitC would _want_ > > to. > > Because the ML way of having impure arrows throws away control of > side-effects. Taking the monadic approach leads to a much nicer, more > general type system that more closely resembles a logical-framework. These > things become important when you want to start proving things about > programs. Its also worth reading this: > > http://r6.ca/blog/20110520T220201Z.html > > As you can see IO is actually a datatype with a special deconstructor > which is where the side effects happen. It just happens to fit a > composition pattern that is called a Monad. Being monadic is an emergent > property of the semantics of the datatype, not something arbitrary imposed > by the language. > > So the discussion is not monadic or not-monadic, but are side effects best > represented by arrows or datatypes. On the basis that we need to represent > arities in types, separately from tuples, then we would need pure arrows, > so that applying a curried function does not result in side-effects. We > could introduce a new type of arrow like this: > > f :: a-> b ~> c > > Where ~> is side-effectful application, however to add effects would > require a whole lot of different flavour arrows and ways to compose > different arrow types... its starting to look a mess. > > but I would rather use an existing mechanism like datatypes: > > f :: a -> b -> Eff e c > > Where 'e' is the set of inferred effects in function 'f'. Now it just so > happens that we can compose effects, and the composition rules share the > structure of a Monad. So if we declare (Eff e) to be a monad, with the > relevant composition rules, we can infer composed effects. > > To me there is a natural structure to type-systems, and that should be > followed, rather than just making stuff up. > > > Keean. > > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
