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
