Optionally declare functions `pure`?
Opened this issue · 214 comments
Also, the compiler can use a much simpler form of path analysis (independent of run-time state) to do that performance optimization without needing dependent typing (although without purity it becomes more difficult for the compiler to know what is safe to reorder).
Purity provides more opportunities for optimization.
I would rather have monadic types for impurity. In this way we have a sound type system that can be expanded for full effects support. I would like to have inferred monadic side-effects. The inference means the average user does not need to bother or understand them, but you can use type classes to constrain the types to achieve things like this function must not do IO, or must not allocate memory etc.
If all the primitive operations have the correct mondaic types assigned to them, purity becomes constraining a type to have no side effects. I haven't really thought about the effect syntax, nor how a constraint on effects would look syntactically, but this achieves what you want with more fine-grained control about which side-effects to permit.
If operations are correctly typed and maybe with some syntactic spitshine, we can make monadic types look very simple, I'm all for just going with monadic types. We can probably make it so the user doesn't even realize he's using monadic types.
Lets assume we have monadic types, and that all functions are in some monad (as we want to allow imperative style statements anywhere). Further lets assume we have a monadic effect system, with effect inference. As such effects will propagate from the function use site to the definition (the effects on a function being the union of all effects in functions used in the function definition).
As long as primitive functions get the correct types, it should all work without the user even knowing. They only need to know if they wish to constrain effects, probably with some kind of type class. In order to do this the type system will need to provide some a 'set' kind of type, but I think we need that for union types already.
Having to import functions from JavaScript and give them a type seems like some boilerplate, but I don't think there is any other way. For example a simple primitive 'print' type function would have a signature like:
print(x : String) : [write_stdout] ()
A primitive input function would type like this:
input() : [read_stdin] String
Now you can use them like this:
doit = (prompt) =>
print(prompt)
return input()
The type of doit can be inferred, however you can give optional type annotation like this:
doit = (prompt : String) =>
doit = (prompt) : String =>
doit = (prompt : String) : String =>
doit = (prompt : String) : [write_stdout, read_stdin] String =>
All the above would be valid, but the type below would not:
doit = (prompt : String) : [] String =>
The empty brackets would force the function to be pure, and of course the definition is not, so it should fail type-checking.
So the assumption is all functions are in the effect monad, and therefore we can omit the effect constructor '[]' from the type signatures of functions.
I like that. A lot.
My understanding of a monad in this context it provides composition of functions that mutate some state (i.e. input and output the state type) with those that don't. The advantage over compiler-assisted access to globals, is we can have different state objects (e.g. different implementation of print) for different code paths. And I believe we can even compose monads in some cases, but they are less composable than Applicatives. I like the idea of fine-grained access to resources, as this also has security applications, e.g. Android apps need to declare which resources they access.
But separately we would still need a way to declare a function's inputs arguments and constructed references (collectively or individually) deeply immutable (which is not the same as JavaScript's const which merely prevents reassignment of the reference).
Technically in an imperative language where any statement can perform IO to any external service, every function is in a monad :-) The threaded state is the 'world' and return is the unit function, and the statement separator (newline or ;) is bind.
We need purity declarations, otherwise we model values separately from functions, which is a non-unified construction.
Note that the purity declaration for an immutable reference and a zero argument function can be unified to let.
Then we get an arbitrary split, some functions are pure and some functions are impure. I can only call pure functions from pure functions but I can call either from impure functions. This is how Haskell works and it as a real problem for a lot of people to work with. You want to put a print statement in a pure function somewhere and all of a sudden you have to rewrite half the program.
If you want an easy to use language that Java programmers will be able to use, we cannot do this. This would make the language feel more like Haskell than any of the type system features I want.
I think we want all functions to be impure and in the IO monad. We can then use constraints to prevent side effects where we don't want them, but the functions will still be impure.
The separation between function reference and result value is very important.
@keean wrote:
You want to put a
I thought you were planning to offer treading global state through pure functions with an implicit/inferred monadic system. So IO would be in the monad. Same as Haskell does it.
Seems to me we can't do your monadic idea unless we do it every where. But am I correct it will only add overhead to calls to functions which access the monadic state or will the performance of every function call suffer?
I think we want all functions to be impure and in the
IOmonad. We can then use constraints to prevent side effects where we don't want them, but the functions will still be impure.
If we are forced to have your monadic system every where, then why should all functions be impure and in the IO monad by default?
The separation between function reference and result value is very important.
I don't understand what you do you mean?
If we will have pure annotations on functions, then we also need const annotations on input arguments for impure functions that only call pure functions on those const inputs.
@keean seems to me silly that for example a length function will ever need to call print. That is what we have debuggers for.
Seems to me we can't do your monadic idea unless we do it every where. But am I correct it will only add overhead to calls to functions which access the monadic state or will the performance of every function call suffer?
There is zero implementation overhead, it is simply a type system change. I have pointed out before you can give 'C' functions a monadic type, do the type checking and then compile it using the normal C compilation method.
If we are forced to have your monadic system every where, then why should all functions be impure and in the IO monad by default?
Because we may want to change the function to include IO without having to change all the module type signatures.
I don't understand what you do you mean?
A program is a bunch of symbols that is executed to produce a result. It is important we can pass around the unexecuted function and then execute when we want. I think it is important that the notation is consistent no matter how many arguments a function has. Making an exception for zero argument functions is introducing special case inconsistent notation.
seems to me silly that for example a length function will ever need to call print. That is what we have debuggers for.
Debuggers should not make up for inadequacies of the language. Programs are rarely written in their final form and the ability to easily refactor is important.
@keean wrote:
Because we may want to change the function to include IO without having to change all the module type signatures.
I don't understand. What do modules have to do with it? I probably need to see a code example.
A program is a bunch of symbols that is executed to produce a result. It is important we can pass around the unexecuted function and then execute when we want. I think it is important that the notation is consistent no matter how many arguments a function has. Making an exception for zero argument functions is introducing special case inconsistent notation.
Afaics, syntax of zero argument functions is orthogonal to a purity annotation decision and discussion. @skaller and I enumerated optimizations and benefits of purity. For example also the following also applies to non-zero argument pure functions:
The following LOC would be a compiler error, because the result value of pure functions must be assigned:
size
Debuggers should not make up for inadequacies of the language.
What inadequacy? Purity annotation is an optional feature.
Readers please note that certain side-effects are not side-effects in our type system. More discussion about the relationship to IO monad.
You had disagreed with me about certain side-effects being inapplicable, but I (and @skaller) argued I think convincingly that the only side-effects that matter are those that our type system guarantees.
If we pass around the IO monad as external state, then every
print(x)will be an "impure" function w.r.t. to every function that also accesses the IO monad but if a new copy of the IO monad is returned instead of being mutated, then those functions are still pure functions because they don't modify external state nor depend on any state not provided by the inputs. This why Haskell is still pure even though it has side-effects to IO monad, because this IO monad state is a state which is passed along the function hierachy and so the ordering is explicit. That effects are semantically imperative (meaning that changing something in one function could affect expected semantics in some function far away, i.e. the locality of semantics is desirably forsaken), but the functions are operationally (operational semantics) pure and can be optimized as pure.
I wrote:
We can’t model everything with types, thus a typing system is always inconsistent (or otherwise stated can’t model all forms of errors nor allow all algorithms).
Thus even in a statically typed program, we must have dynamically typed features either explicitly or adhoc. So to characterize a program as unityped doesn’t mean it has less expressive power, only that it has less statically expressive power.
I don't think we need purity anyway, just side-effect control.
What do we gain by marking a function pure?
@skaller and I already explained that. I also explained that even a non-zero argument pure function can't be invoked without assigned the result value, so the compiler can catch this bug:
The following LOC would be a compiler error, because the result value of pure functions must be assigned:
size
@shelby3 okay well I think a zero argument function should be executed... it is not the same things as a value. Scala got this wrong :-)
@keean there is no reason to execute a pure zero argument function. That is nonsense.
And there is no reason to execute any arity pure function if the result value is not assigned.
@shelby3 It may fail due to lack of memory. A value is a value like '4' or '7'. A function has a value which is the set of symbols for example "4 + 7". Before you execute it is is "4 + 7" when you execute it, it returns "11". If it is a const function the compiler may optimise by executing it at compile-time. (By the way @skaller was saying the same thing).
To me it seems you want to save typing two characters () and that you are willing to mess the semantics up to do it.
refresh again.
We can analyse this further. The only time a pure function is really pure is when all the inputs are known at compile time (in which case you can treat it as a const). If any of the inputs to the function depend on IO then the pure function has to be lifted into the IO monad.
To put it another way, when we treat a function as pure and replace it with its value it means the input cannot change. If the inputs to a function change, its results will change to. You can see this in Haskell:
f x y = x + y {- pure function -}
g : IO Int {- impure function does IO -}
g = do
x <- readInt
y <- readInt
z <- return (f x y) {- lift f into the IO monad -}
return z
If we don't do this the program will go wrong, because the compiler will not know that the result of 'f' can change with time, and it will replace it with a single value that won't change even if we run g again and the user inputs different values, once f is replaced by a value it will always be the same value.
Of course if a function has no side effects, and no arguments, it must be a const value (IE the compiler can replace the function with its value at compile time). If this is the case you can declare it as a value instead, just do:
let x = 3 * 5 + 8
It seems there is no need to ever have a pure function with no arguments. The only useful zero argument functions have side-effects :-)
@keean don't forget that (which I pointed out before) a function which takes a callback of a zero argument function, would also accept a pure such function. And this is another reason to treat const values and pure zero argument functions as equivalent and also pass them as callback for (pure and impure) zero argument functions.
@keean wrote:
It may fail due to lack of memory.
...
The only time a pure function is really pure is when all the inputs are known at compile time
I already linked to were @skaller and I refuted that entire line of reasoning. I am not going to repeat it.
To put it another way, when we treat a function as pure and replace it with its value it means the input cannot change. If the inputs to a function change, its results will change to. You can see this in Haskell
You are conflating two orthogonal concepts. The value of the pure function never changes and no side-effects occur (that are modeled in the type system). The inputs select which element of the (lazily memoized) set of the function's value is presented.
An impure function isn't guaranteed to have the same result for any fixed input, i.e. the set of results that is the function's value is not constant.
To me it seems you want to save typing two characters () and that you are willing to mess the semantics up to do it.
No I want a system that is complete, consistent, and not corner cases. It appears to me sometimes you seem to want consistency by not being complete, which is a form of obscured inconsistency.
To make progress I suggest implementing basic stuff, when in doubt leave it out until there are actual uses cases to consider. So, do not put "pure" yet. Do not have => for functions and -> for functions with IO monad, yet.
These forums are not the best for technical discussions IMHO. For a start, you can't reply to someone as you can with email. We need an email list which tracks commits. I can write some test cases, but i would need commit access and a fairly clear specification of what is implemented and what it should do. As soon as possible, I think an FFI is required, and then a place to put a library of bindings to Javascript. Most of the work you can do with the language can then be done almost immediately by adding the required bindings and writing Javascript to bind to.
No matter what you think the advantages of Zen-fu are the primary one is the ability to leverage existing code, but access it in a better structured way (eg with type checking).
One thing I learned on the C++ committee is that the library drives the language. You add stuff you need to make the library work. So for example Felix has a restricted kind of constrained polymorphism where you can define a type set (a finite list of types), and constrain a type variable to that list. Why? Because that's whats needed to define addition of all 20 types of integers C++/Posix require in one line. (Just an example).
@shelby3 regarding monads and impurity: if we start with all functions being pure, then we need a way to manage impurity. If we consider an arrow is just a binary type constructor, we can take a type like this:
A => B -> C
Which would be a pure function that returns an impure function, and rewrite this:
A -> B -> M<C>
Where an arrow followed by a special type constructor M represents the impure action. In the above we are using -> to represent pure functions, and we can see the impurity represented by the extra constructor M.
At the basic level that's all there is to it. There are some subtle details, like the monad, as it has no decinstructor enforces that impure can call pure (via lifting) but not the other way around.
In this basic categorisation we can have a single monad which encapsulates all impurity, which Haskell calls IO but we could call whatever we like. We can then get into making more fine grained distinctions, but let's see how we get on with the basic 'impure' monad.
@keean during my incomplete (and possibly some mistakes) research for the language Copute which I was working on in 2011, I did write down my understanding of a State monad:
http://www.coolpage.com/copute/docs/
See also the example in Traversable and the conceptual description of imperative programming in Event.
So it seems what you want to do is as I quoted below?
Rationale
Makes the computation of state orthogonal to the state transitions of unlifted functions. Thus generally any kinds of orthogonal state can composed with any category of morphisms, without case-specific boilerplate.
The
State(aMonad) eliminates the boilerplate of threading some state across functions that don't access that state so as to compose these with functions that do access that state. This allows reuse of functions without having to code separate functions for each permutation of state that one might one to compose with. TheStatemonad is roughly analogous to a threadable scope for global variables, i.e. that state is encapsulated, so that state is only accessible to functions in the composition, and thus the functions are pure w.r.t. that state. Thus the state effects are transparent (the functions operate on that state via inputs and return value only), delimited, and composable.
So it seems to what you want to do is as I stated there?
A state monad only stores a specific bit of state. In the case of an impure function the monad represents all the impurity. Perhaps we could call it the World monad.
Some further details:
Using the State monad you can construct a state machine. Here the state is in the monad, an pure state transformation functions link one state to another on the clock tick (event update). With the state monad if you have multiple state machines, they can each have their own state space that is separate. This manages the combinational complexity blow-up when combining state machines (as we know for certain that the private state of state-machine one cannot affect state-machine two etc).
This leads to a problem with monads if you want to write a program that is in two monads at once (IE links two state machines together). The direction Haskell took was to have a "World State" monad called IO that conceptually stores the state of the world. As such IO is reading and writing state from the World state. This allows multiple state elements to exist in the same monad (the world monad). This is initially what I am proposing here, that we have one "built-in" monad. It does not need special treatment by the type system (which is one of the reasons this is considered a function model of impurity).
This is all we need to get the same functionality as the pure/impure arrows but in a more general way, as we can go further with this concept. For example we can solve the problem with state monads using monad transformers (the way Haskell does it), but this is a poor solution in my opinion and lead me to waste much time wrangling with the type system to understand and implement various seemingly obvious things. A better solution is a set monad where we can 'or' together multiple monads a bit like a union. But first lets decide if we want to use this model of impurity. On the whole type inference will make this painless for example:
f(x : Int) => 1 + 2
Would have an inferred type of Int -> Int, however
f(x : Int) =>
print(x)
1 + 2
Would have an inferred type of Int -> World<Int>. If we decide to call our "world state" monad World.
I have found the following helpful for me to better understand the essence of a Monad:
http://stackoverflow.com/questions/44965/what-is-a-monad/10245311#answer-10245311
http://stackoverflow.com/questions/2704652/monad-in-plain-english-for-the-oop-programmer-with-no-fp-background/2704795#answer-2704795
https://blog.jcoglan.com/2011/03/05/translation-from-haskell-to-javascript-of-selected-portions-of-the-best-introduction-to-monads-ive-ever-read/
http://blog.sigfpe.com/2007/11/io-monad-for-people-who-simply-dont.html
Thus, I understand that one use-case of a Monad is to enable the composition of functions which operate on some state with those that don't, and the former can call the latter but not vice versa. This can enable us to tag pure functions which for example access certain genres of state, such as the input stream since these functions will input and output the said stream state. Every time we modify this state we must make a new copy of it, else our caller's copy would be modified making our function not pure. So really the Monad has nothing to do with what enables us to access the said state with a pure function. The Monad is only enabling the additional said composition.
Thus this seems to do nothing to enable general imperative programming. For example, it doesn't enable us to operate on arrays.
Sorry I think we will also need impure functions. I never intended to create a programming language that forced purity and immutability where it is more efficient to use imperativity and mutability. Pure functions are not always the optimum choice. I've read they have a log n factor slower performance in general, in addition to making some algorithms obtuse. Where purity fits, it can be useful, but it shouldn't be forced every where.
Every time we modify this state we must make a new copy of it, else our caller's copy would be modified making our function not pure.
No this is not right. A monad is a type system concept. We can type check C code using monads, and then compile using the normal C compiler for absolutely zero performance cost :-)
Thus this seems to do nothing to enable general imperative programming. For example, it doesn't enable us to operate on arrays.
This misses the point, using a monad to represent impurity can be seen a simply a syntactic operation on types. For example:
Starting with
(A) => (B) -> C
A pure function that returns an impure function (using the arrows as you prefer them), we can apply the following substitution:
(a) -> b ==> (a) => W<b>
Using lower case letters for the substitution "meta-variables". Applying this to the above we get:
(A) => (B) => W<C>
Everything about the things you can do in the impure part of the function remains the same as with the impure-arrow, except we get some nice additional properties:
- What goes into a monad can never be got out (this is really the key propery of a monad as an algebraic concept). This is useful because it models the fact that an pure function cannot call an impure function (because then it would itself of course be impure). The monad models this directly, whereas using the arrows we have to introduce an ad-hoc check outside of the type system to do this.
So a monad is a closer model for impurity in functions than a different arrow, and there are no performance costs, because this only changes the types assigned to code, not the code itself.
Sorry I think we will also need impure functions. I never intended to create a programming language that forced purity and immutability where it is more efficient to use imperativity and mutability. Pure functions are not always the optimum choice. I've read they have a log n factor slower performance in general, in addition to making some algorithms obtuse. Where purity fits, it can be useful, but it shouldn't be forced every where.
Because the assumptions you made are wrong, the conclusion is also wrong, although your logic is impeccable. Unfortunately none of the references you linked to really seem to understand what a monad is at a deep level.
No this is not right.
Disagree. You will break the entire point of purity and immutability otherwise. A pure function which inputs a IO must return a copy of the instance as the output IO. This can be made fairly efficient, as Haskell has apparently done. For example, the inner workings of the IO monad can use an internal buffer for storing indices into its buffered input stream.
This misses the point, using a monad to represent impurity can be seen a simply a syntactic operation on types.
Sorry no. That isn't correct. You still have to maintain the rules of purity of the inputs and outputs of pure functions.
The only way it is correct is if you are allowing these to be impure procedures. Which means you can no longer call these procedures from other pure functions.
And in that case, we have impure procedures, which is my point that we will have both pure functions and impure procedures.
It is possible that our difference is merely a miscommunication (as it usually is because you don't seem to understand me and I don't seem to understand you, sigh). I also find that you don't explain things in a very intuitive way. I don't find you to be a clear communicator. You seem to talk in a private language of types. Talk to me in English please.
If seems you want to allow impure procedures. And you want to infer them?
The only way it is correct is if you are allowing these to be impure procedures. Which means you can no longer call these procedures from other pure functions.
That is correct, you cannot call an impure function/procedure from a pure one, and this is the very thing the monad enforces in the type system.
And in that case, we have impure procedures, which is my point that we will have both pure functions and impure procedures.
Yes this is true, from a certain point of view.
So please try to communicate your paradigm shift view to me in a way I can understand. Writing type signatures that don't mean anything to me, doesn't communicate anything to me.
If you can't explain it to me, you have no hope of explaining to most of the JavaScript programmers.
This comment of yours is gibberish to me. It means absolutely nothing to me. I know exactly nothing more than I knew before trying to read it.
This comment of yours is gibberish to me. It means absolutely nothing to me. I know exactly nothing more than I knew before trying to read it.
What is the best way to help you understand? I know you know what a type-system is, and I also know you understand about pure and impure arrows.
Consider that an arrow is just an infix binary type constructor, we can rename => in prefix form as Arrow<A, B> so what is special about the arrow?
refresh
Explain it using a Java example perhaps?
Explain it using English instead of types and arrows.
Eric Lippert seems to be able to explain Monads in a way that is much easier to understand.
See the 100s of upvotes on the comments at the bottom of this SO answer, to understand the attributes of why your elucidation will fly right over the head of most people who are not Haskell programmers.
Explain it using a Java example perhaps?
Writing monads in Java is very different from typing Java using monads :-)
Explain it using a Java example perhaps?
Writing monads in Java is very different from typing Java using monads :-)
I understand, but you'll have to learn how to understand your art as well as Eric Lippert does.
See the 100s of upvotes on the comments at the bottom of this SO answer,
This explains how to use monads, it does not explain what a monad is.
I understand, but you'll have to learn how to understand your art as well as Eric Lippert does
At this point should I get angry, and start complaining that I cannot work with you if you cant respect that I understand these things?
I didn't say you didn't understand these things. My point is that you if you want to communicate with those who don't think about types the way you do, then you need some way of explaining in English, which exhibits a mastery of understanding of the concepts and what the reader can comprehend. Eric Lippert is a master. You may understand your private language, but you may not yet be a master communicator of what you know and think.
You may understand your private language, but you may not yet be a master communicator of what you know and think.
Well, that is a criticism I can take :-P I have to eat now, but I will see if I can come up with a better explanation.
The important point is to understand that the same program may have different types in different type systems.
Consider that an arrow is just a binary type constructor, we can rename => as Arrow so what is special about the arrow?
The relevance of this does not register for me. Also I don't know what 'binary' means in this context.
The relevance of this does not register for me.
But you do get that Arrow<A, B> is no different from Widget<A, B> right. I don't want to get into a long explanation if we don't agree on the basics.
I could probably figure out what you are trying to communicate to me if I'm willing to give myself a headache. But I am thinking you should be able to make it more obvious for me?
The relevance of this does not register for me.
But you do get that
Arrow<A, B>is no different fromWidget<A, B>right. I don't want to get into a long explanation if we don't agree on the basics.
Do you mean Arrow<A, B> as an alias for A => B? Do you mean no different in the sense that a function type can be written in the format of Function<Input, Result>? Obviously you don't mean a Widget is a function?
Eat first.
Do you mean Arrow<A, B> as an alias for A => B?
Yes that is the first part.
Do you mean no different in the sense that a function type can be written in the format of Function<Input, Result>?
Yes, that too.
Obviously you don't mean a Widget is a function?
Sorry English thing, a "Widget" is sort of a generic word, lets call it Foo<A, B> instead.
I may be mistaken but I believe it is impossible in the Haskell do notation to store the value of an IO instance and then access it after weaving through some other operations. Thus you wouldn't need for those operations to be pure. I think this is essentially what you are trying to do somehow with types (which includes making it impossible access an instance of IO that was input to another procedure?), but I can't holistically comprehend what you are describing even though conceptually I think I know what you are trying to achieve.
See I can cut to the essence in a way that gives me a conceptual understanding. You don't describe the conceptual essence, but rather talk in terms of underlying details (e.g. types) and expect me to understand what the essence is from types. That is what I mean by not being a master communicator of your concept (even though you may be entirely correct and expert about the validity of your idea). Perhaps you need to acknowledge that do you have impure procedures in your concept but somehow are preventing any unsound interaction between the pure functions and impure procedures (which you have stated but I can't relate that to any example or code in mind)? And then communicate that clearly with examples and a syntax I can comprehend?
Most likely in order to explain your concept to me, you probably need to discover a different way of conceptualizing how you think about your own idea (even though the idea doesn't change).
Most likely in order to explain your concept to me, you probably need to discover a different way of conceptualizing how you think about your own idea (even though the idea doesn't change).
I'm working on it.
Perhaps you need to acknowledge that do you have impure procedures in your concept but somehow are preventing any unsound interaction between the pure functions and impure procedures (which you have stated but I can't relate that to any example or code in mind)?
I probably haven't been clear about this. Let us assume for now that there are pure and impure procedures/functions. But we are going to start from a completely pure language to which we want to add IO and mutation of objects etc.
We need a way to distinguish pure computations from impure computations. Pure computations are straightforward, so lets move on to impure computations. What we do is assume all functions are pure to start with, how can we have stateful computations?
One way is to have a variable representing the world, lets call the type of this World. We can then have a function that mutates the world:
f : (World) -> World
This satisfies the requirement for pure functions that the result only depends on the input, because we input the whole world)
We don't have to copy the world (that would be impossible anyway). So although we haven't changed anything about the mechanics of the language, we now can do IO and mutate arrays etc in a language that was completely pure.
Now this has some consequences we have to deal with, like for example the language is now unsound, but I want to make sure we are in agreement before moving forward.
We can then have a function that mutates the world:
f : (World) -> WorldThis satisfies the requirement for pure functions that the result only depends on the input, because we input the whole world)
We don't have to copy the world (that would be impossible anyway). So although we haven't changed anything about the mechanics of the language,
Disagree. If you don't copy the world, that is not a pure function, rather it is impure procedure. We have to get the foundational concepts correct, otherwise I can't understand you.
Just because you can't copy the unbounded state of the Turing-complete World, doesn't make your computation pure.
Disagree. If you don't copy the world, that is not a pure function, rather it is impure procedure. We have to get the foundational concepts correct, otherwise I can't understand you.
Nothing has changed, apart from passing the world in. For example lets take a simple function:
f(x) => x + 1
Now lets pass the world along too:
f(x, world) => (x + 1, world)
Now I didn't say this function was still pure, I said starting with a pure function. At the moment we haven't changed anything else, so the compiler is still treating everything in the function exactly the same way as before.
So temporarily forget you know what purity and impurity are, and assume you have a pure functional language and you have naively tried to add the world to a pure program.
refresh
@keean I think the key point is probably that if we can prevent the caller of f accessing a reference that saved the state of the World to an immutable reference before it was input to f, then it doesn't matter if f is impure. I think Haskell is effectively doing that with IO. Thus in effect f is pure.
The key point appears to be that the weaving of the state through the "impure" procedures is done such that no caller of these "impure" procedures can access an out-of-date reference to the state. Thus in effect these "impure" procedures are pure from the perspective of access.
Now you just have to explain to me how that is accomplished. I can't visualize it yet, even though I know that is what it must be doing.
The key point appears to be that the weaving of the state through the "impure" procedures is done such that no caller of these "impure" procedures can access an out-of-date reference to the state.
Yes, you can look up the "Clean" language which uses "uniqueness types" to do the same thing. Basically the above is unsound because world cannot be memoised. So we need to flag to the compiler not to memoise world and to always use the "real world".
But we also need to prevent saving an immutable reference to the World, then calling a function that modifies the World, then accessing said reference. Or we can say that pure functions can never call impure procedures, and thus even if they take the World as input, they can trust their immutable reference. Since impure procedures can mutate the World, then no problem if they save a mutable reference to the World.
Thus I come back to you are just asking for impure procedures. I still don't see why you need a monad.
But we also need to prevent saving an immutable reference to the World, then calling a function that modifies the World, then accessing said reference.
Yes, that is what uniqueness types do, they basically mean world has a unique type that cannot be used more than once. So:
print(String, World) -> World
print takes a string and the world, mutates the world, and returns a new world. In "Clean" as the world has a "uniqueness" type the old world cannot be used again, so anything else must use the new one.
https://en.wikipedia.org/wiki/Uniqueness_type
Now I am not suggesting we use uniqueness types, but they help understand what is coming next.
I need to sleep. But please explain more.
For later :-)
So what we need to do is to sequence access to the world so that we can only access the latest "version" but note there is no copying.
The monadic bind and unit functions look something like this:
bind(M<A>, A -> M<B>) -> M<B>
unit(A) -> M<A>
What is interesting is the type of bind consider we make the world a datatype:
data WorldMonad<World, A> = WorldMonad(World -> (World, A))
So the world monad is a function from World to World but also returns A the result. So in effect the WorldMonad is capturing the fact that world is passed to and returned from every impure function. Now scoping takes care of the rest, you can only access the world you are passed, and the world you return is the mutated one. I will go through how this plays out in the next post.
The next step is to derive the monadic bind operator, which would look something like:
bind(wm, g) => WorldMonad((world) =>
match wm
WorldMonad(f) =>
let (y, world1) = f(world)
match g(y)
WorldMonad(h) => h(world1)
)
So we can see that bind controls the sequence of passing the world so that the inital world gets passed to the LHS of bind, and the result of that plus the returned world get passed into the RHS. Bind threads the world through each monad, guaranteeing the sequence, and forwarding the results.
With infix operators we can write bind as >>=
We use bind in impure functions to replace function composition. So we cannot write f(g(h(28))) when f, g, and h are impure, instead we would write h >>= ((x) => (g >>= ((y) => f))). The bind operation ensures that the world is threaded through the impure functions, such that each functions can only access the most recent reference to World.
The properties of the monad ensure the world gets threaded so each impure function can only use the current state of the world and not a previous state of the world. It also ensures that only impure functions can call impure functions (because impure functions do not have the right type.
The final thing to note is that in a statement block, the monadic bind is the statement separator (so newline in our language) and unit is return (which lifts a value into the monad).
Tangentially on a small nitpick, I'd prefer you write as follows unless you are actually writing those types as functions of a typeclass definition:
bind : (M<A>, A -> M<B>) -> M<B>
unit : (A) -> M<A>
I proposed to elide the noise of : in typeclass definitions, but when writing those stand alone, it looks weird without the : because it as if you are defining a standalone function without the argument names and function body.
bind(wm, g) => WorldMonad((world) => match wm WorldMonad(f) => let (y, world1) = f(world) match g(y) WorldMonad(h) => h(world1) )
And so you acknowledge that f, g, and h are not pure if they are not copying the World (which is of course impossible to copy generally if it is unbounded Turing-complete).
We use bind in impure functions to replace function composition. So we cannot write
f(g(h(28)))whenf,g, andhare impure, instead we would writeh >>= ((x) => (g >>= ((y) => f))). The bind operation ensures that the world is threaded through the impure functions, such that each functions can only access the most recent reference toWorld.The properties of the monad ensure the world gets threaded so each impure function can only use the current state of the world and not a previous state of the world. It also ensures that only impure functions can call impure functions (because impure functions do not have the right type.
Excellent. Now you've explained in a way that doesn't make my brain explode due to inconsistency. And you did that apparently because I taught the teacher how to focus on the generative essence.
I've never seen anyone explain the IO monad properly this way! That is why it never made any sense to me. Now that I understand that the built-in functionality of the IO monad of Haskell is actually not using pure functions, then I can understand the damn point.
You see people who understand why some thing works, often fail to communicate the key generative essence to others who are trying to learn. That for me is what Einstein meant when he said (paraphrased), "you don't know something well enough until you can explain it to a novice".
Now someone needs to go write a blog about IO monad that teaches it this way.
The final thing to note is that in a statement block, the monadic bind is the statement separator (so newline in our language) and unit is return (which lifts a value into the monad).
Yes we can have our compiler do the bind operator >>= implicitly, which is also what Haskell's do notation does. And that is why I had cited this:
http://blog.sigfpe.com/2007/11/io-monad-for-people-who-simply-dont.html
Note it is written there:
We have to use
<-instead oflet ... = ...to get a returned value out of a command. It's a pretty simple rule, the only hassle is you have to remember what's a command and what's a function....
Note how we used
<-instead of let to get the result ofgetLine....
So how do you know what's a command and what's an expression? If it has any chance of doing I/O it must be a command, otherwise it's probably an expression.
...
so occasionally there will be commands that don't do any
IO. But not the other way round. [meaning never expressions that doIO]
So it is clear that Haskell's do notation is preventing storing an mutuable IO instance reference with let and pure expressions can never access the World in an IO instance.
And so you acknowledge that f, g, and h are not pure if they are not copying the World (which is of course impossible to copy generally if it is unbounded Turing-complete).
I probably wasn't clear on the point, I was trying to show how if your tried to thread the world through pure functions it would break the compilers assumptions. So the compiler needs to track which functions are impure.
So it is clear that Haskell's do notation is preventing storing an mutuable IO instance reference with let and pure expressions can never access the World in an IO instance.
Yes this is right. Actually the <- differentiates pure assignment from execution if an impure function. Consider:
let x = ask("what is your name?")
y <- ask("what is your name?")
z <- x
The first line assigns the monad on the RHS to x, but does not execute it. The second line executes the monad and assigns the result (your name) to y, the final line executes x and assigns your name to z.
Haskell has to do this because it assumed all functions behave like pure functions, and therefore they are replaceable by their result. But we don't have to assume that, because we are using a different notation for functions. Because we are using () for arguments, we can refer to pure assignment of the function, and execution of the function like this:
let x = () => ask("what is your name?")
let y = ask("what is your name?")
let z = x()
So assignment without execution requires a new lambda (as we have no way of supplying arguments without execution, but this does the same thing a different way). Assignment of the result after execution is the normal, and execution and assignment of the result of an impure nullary function requires the brackets to tell us we are executing it, not actually assigning the function itself.
The above let's people enter impure programs in a natural way into a system that has familiar syntax.
The remaining question us how to deal with pure functions? We could introduce different syntax or semantics for pure functions, but I would like to suggest that to suddenly have some functions you don't have to execute would be confusing. So I would suggest creating an identity monad, one that does nothing except wrap it's contents, something like:
data Identity<A> = Id(A)
And pure functions get put into the identity monad. This way you can handle pure functions exactly like impure functions, passing the function itself (as a function whose result is in the identity monad) or 'execute' it which is really just unpacking the result from the Identity datatype.
Thus I come back to you are just asking for impure procedures. I still don't see why you need a monad.
So I think perhaps I more or less understand what you are proposing and I want to compare the justification for it, to the tradeoffs it entails.
So the justification as compared to allowing impure procedures which can operate on any global state (e.g. print or getLine which do not explicitly input a state argument) is that we can control which state an impure procedure can (or more saliently can not) access with some optional annotation. Compared to the option of print or getLine which do explicitly input a state argument, the monadic approach would allows us to add the use of a new genre of state (a new monad type) to a procedure deep in the call hierarchy without needing to manually refactor to add new input arguments every where in the call hierarchy above the procedure we are editing.
But if we were to exclusively only allow monadic composition of impure procedures, then it would mean just to pass an array to an impure procedure, we would have to create a special monad type for that. And the problem that Monads don't compose so the complication of monad transformers which you mentioned.
Thus it seems to me that we need to offer impure procedure composition in the general form of g(f(h(x))) as well.
In other words, the monadic effects system is a way to control some effects but it is too cumbersome for modeling all imperative code.
So we need to think about how to combine two models for imperative programming, along with pure functional composition. This may or may not be too complex. Need to analyze.
The remaining question us how to deal with pure functions? We could introduce different syntax or semantics for pure functions, but I would like to suggest that to suddenly have some functions you don't have to execute would be confusing.
You are repeating a discussion that we had before. And I presume you remember that I expressed the idea of unnullary pure functions being "called" without the empty tuple ():
let x = length // x has a type `Uint`
And when we want to assign the function reference:
let f = length as () -> Uint
Or:
let f: () -> Uint = length
You seem to not like it, because you think it is inconsistent that unnullary functions don't need to be called, yet unnullary procedures need to be. I don't see how that is inconsistent? A procedure is not a function.
I also suggested another possible alternative consistent with our proposed syntax for partial application (makes no sense to partial application every argument, so obviously the below has a special meaning):
let f = length(_)
But if we were to exclusively only allow monadic composition of impure procedures, then it would mean just to pass an array to an impure procedure, we would have to create a special monad type for that. And the problem that Monads don't compose so the complication of monad transformers which you mentioned.
Yes, however if everything is in the world monad, you don't have this problem.
So a world monad is like having an impure arrow, except it takes care of the fact that a pure function can never call an impure function all in one abstraction.
In other words, the monadic effects system is a way to control some effects but it is too cumbersome for modeling all imperative code.
We haven't discussed monadic effects, I wanted to stick to the simple case if the world monad and why it's better than different flavour arrows.
However let's consider how we can have a composable effect system. We cannot use monad transformers because they don't compose. Let's start with the idea that we will split out IO effects like "ReadFile" and "WriteFile". We note that composing a tuple of monads is the same as composing each monad in the tuple. Tuples however have order (a,b) is a different tuple from (b,a). An order less tuple is a set. So we need a set of monads, do that they compose using set algebra (union, intersection etc). The only issue is the monad is a type constructor, so we need a set of constructors that all apply to the same type. Consider we have the monads:
data ReadFile<A> = ReadFile(InputState -> (InputState, A))
data WriteFile<A> = WriteFile(OutputState -> (OutputState, A))
Now we need to have a set of these that all apply to the same return value. We could write this as:
f : (Int) => {ReadFile, WriteFile}<Int>
Which is a function that reads and writes from a the filesystem, is passed an Int and returns an Int.
Using this system we can have as many different effects as we want, or just a whole "world" effect.
As we can always infer the effects from a function definition we can omit the effects from a type signature, or include them. Infact we can use type-classes to create constraints. For example the Pure typeclass can constrain a function so it is not allowed any effects:
f : (Int) => EFF<Int> where EFF : Pure
The default would be no constraints, so functions can do anything, but you can constrain for no IO, no memory allocation, or whatever effects we choose to have.
The only syntax issue is that EFF is a type variable, but it is the constructor, so I am not sure how we would write that?
You seem to not like it, because you think it is inconsistent that unary functions don't need to be called, yet unary procedures need to be. I don't see how that is inconsistent? A procedure is not a function.
Do you mean nullary functions (with no arguments)? There is actually no need for a nullary pure function, it is just a normal let definition:
let f = 5 * 3 + 2
Obviously a nullary impure function needs to be executed because it has side effects.
Do you mean nullary functions (with no arguments)?
Excuse my thought typo "unary". Yes of course.
There is actually no need for a nullary pure function, it is just a normal let definition:
We had this discussion already. Did you forget or are you just repeating the same points which I disagreed with? Please kindly acknowledge when you are repeating that which I already disagreed with, so I won't wonder if you can't remember and/or are ignoring me.
My point was/is that regardless of how we decide to define nullary pure functions (either as non-rebindable, immutable references or nullary functions), both can be treated equivalently at the use-site. Also a non-rebindable, immutable reference can also be assigned to a reference for a nullary function.
Obviously a nullary impure function needs to be executed because it has side effects.
I already wrote that a few minutes ago. Did you not see? (or my typo needed clarification?)
@shelby3 wrote:
yet
unnullary procedures need to be
My point was/is that regardless of how we decide to define nullary pure functions (either as non-rebindable, immutable references or nullary functions), both can be treated equivalently at the use-site.
If we have pure functions that do not require application/execution then the function is idistinguishable from its result. This means we already have a syntax for declaring nullary pure functions, it's like this:
let f = length * width
That is a pure function, and you can use the result like this:
let g = f + 1
We don't need another redundant way of writing pure nullary functions.
This means we already have a syntax for declaring nullary pure functions, it's like this:
let f = length * width
But that is not quite right, because it depends on whether length and width are immutable and let is not rebindable.
We don't need another redundant way of writing pure nullary functions.
I can agree, if we have a way of declaring that f is non-rebindable and transitively immutate or that both length and width are immutable (which are two ways of declaring the effectively the same semantics).
But if we support pure functions and nullary procedures, then it is also inconsistent to not support nullary (pure) functions:
f() => length * width
Where => indicates a pure function.
But that is not quite right, because it depends on whether length and width are immutable and let is not rebindable.
No, its right, if length and width are mutable, then the function is not pure! This is because it does not satisfy the memoisation rule. A pure function must be memoisable so if:
var width = 5
var height = 5
let f = width * height // f is 25
print(f)
var width = 6
print(f)
When we evaluate f for the print, its value is 25. If it is pure, its value cannot change, because we memoise the result, and don't recalculate it, so we just use 25 in the future. If width changes and we expect 30, we are in for a surprise because we will still get back 25 from the memoised result of the pure function. Remember a pure function always returns the same result with the same arguments.
If you want it to change with width and length, we need to re-evaluate the the function every time we call it, so it is impure (for the same reason the world is impure).
But if we were to exclusively only allow monadic composition of impure procedures, then it would mean just to pass an array to an impure procedure, we would have to create a special monad type for that. And the problem that Monads don't compose so the complication of monad transformers which you mentioned.
Yes, however if everything is in the world monad, you don't have this problem.
So a world monad is like having an impure arrow, except it takes care of the fact that a pure function can never call an impure function all in one abstraction.
Are you saying that the World monad is parametrized on the type of state we want to an impure procedure to operate on? So if our procedure inputs a mutable array and set then World<Array<T>, Set<T>>?
If yes, how do different parametrizations compose?
But that is not quite right, because it depends on whether length and width are immutable and let is not rebindable.
No, its right, if length and width are mutable, then the function is not pure!
No that was not quite correct, because you had no annotation for mutability (and rebindability) afaics.
Any way, you are agreeing that I am correct to point that out.
Are you saying that the World monad is parametrized on the type of state we want to an impure procedure to operate on? So if our procedure inputs a mutable array and set then World<Array, Set>?
That is skipping straight to composable effects :-). The world contains all mutability, so it doesn't need to compose. There is only one world.
The trick is we don't really get the array at all, what we get is a handle to the array that exists in the "outside" world. Consider the following:
getArray : (Int) -> World<ArrayHandle>
put : (ArrayHandle, Int, Int) -> World<()>
get : (ArrayHandle, Int) -> World<Int>
So the above is simply dealing with integer arrays to keep things simple. When you call getArray with a size, you get back an ArrayHandle, which is not the array itself but an identifier. This is just a normal value that you can copy about quickly (its really like a pointer). Now put and get will put and get to that array that exists in the outside world.
@keean I am fighting a headache right now, so please don't take any thing personally that might be less than optimally verbalized for avoiding acrimony. I just ate so normally about an hour or so before the yucky headache subsides. Let's keep plowing forward please.
No that was not correct, because you had no annotation for mutability (and rebindability) afaics.
Any way, you are agreeing that I am correct to point that out.
I get the impression we are talking past each other.
My point is a pure function captures the value of the variables when it is declared (not references), it doesn't matter whether they are mutable or not.
When you call getArray with a size, you get back an ArrayHandle
And guess what? Even though we have a pass-by-value language, we automatically get pass-by-reference for arrays (and other statefull objects)... which I think should make you happy :-).
Because we cannot get to the actual array we will need a copy primitive too:
copy : (ArrayHandle) -> World<ArrayHandle>
Now we have the equivalent of "malloc" and "memcpy" but for typed memory regions. Using these primitives in the "world" monad we can build any data-structure we like, just like you can in C.
That is skipping straight to composable effects :-). The world contains all mutability, so it doesn't need to compose. There is only one
world.
Then afaics there is no benefit to employing a monad?
My point is a pure function captures the value of the variables when it is declared (not references), it doesn't matter whether they are mutable or not.
We are having communication dissonance because you are assuming we've decided on a pass-by-value by-default language and I have not agreed to that. We have an open discussion on that in another thread which I need to come back to after we finish this tangential discussion on monads.
Because we cannot get to the actual array we will need a copy primitive too:
What appears to be (so far afaics) complexity of your proposal is really worrying me. But I will try to plow forward to understand the benefits and tradeoffs before offering my opinion.
Frankly I didn't understand your comment. There are too many concepts coming at me at once and it is fuzzy.
I can't yet fathom how this is going to easily adopted by JavaScript programmers. And I don't even see any great benefit yet to adding this complexity.
However let's consider how we can have a composable effect system.
...
Using this system we can have as many different effects as we want, or just a whole "world" effect.
This seems useful because it will enable knowing which impure interfaces a function employs. But why do we need monads? Instead we could explicitly declare the interfaces a procedure inputs as arguments. Is the only benefit of a monadic effect system that we don't have to write them and they can be inferred? Easier for refactoring?
Then afaics there is no benefit to employing a monad?
This is a way of typing a language into a consistent type system. We don't even need to change the language at all. For example JavaScript we would type every function in the IO/World monad because it does not have pure functions. The JavaScript programmer would not notice any difference to the code they type, but we would infer the monadic types... So there is a point, it makes the type-system work properly.
We are having communication dissonance because you are assuming we've decided on a pass-by-value by-default language and I have not agreed to that. We have an open discussion on that in another thread which I need to come back to after we finish this tangential discussion on monads.
It doesnt matter whether we have pass-by-value or pass-by-reference, for a function to be pure it must satisfy the following definition.
- A pure function is indistinguishable from its result, calling the function with the same arguments always produces the same results. The result of a pure function can be memoised, and the memoised value can be used everywhere the function is used.
As you can see this excludes the case you are thinking about.
I can fathom how this is going to easily adopted by JavaScript programmers. And I don't even see any great benefit yet to adding this complexity.
Actually we could apply this typing discipline to the existing JavaScript language and the JavaScript programmer would not even notice. We could make this a strict superset of JavaScript (like TypeScript) if we wanted, as the programmer would not need to know any of this stuff unless they use type annotations, or type constraints.
Most of these things can be explained in a simpler way to the language user, but when designing a language you need to know more, because you need to see how one feature affects another and how the system behaves as a whole.
This seems useful because we know which impure interfaces a function employs. But why do we need monads? Instead we could explicitly declare the interfaces a procedure inputs as arguments. Is the only benefit of a monadic effect system that we don't have to write them and they can be inferred? Easier for refactoring?
We need monads to give us a way of encoding the effects in the type system. Type systems are a kind of algebra, and we only have two types of objects to play with, type-constructors, and type-variables. We need to be careful we extend the type system with algebraic properties that preserve all the axioms of the type system, or we create a potentially unsound mess.
Also monads give us the containment we want. You can only call a "ReadFile" function from another "ReadFile" function, so monads ensure that the call graph obeys the set-semantics, so that effect permissions have to be handed down from the main-program (which presumably has permission for all effects). In other worlds the algebraic structure of a monad models the dynamic "inheritance" of effect permissions in the call graph.
As you can see this excludes the case you are thinking about.
It matters for the syntax and type system I am designing. We are experiencing dissonance because your design is so divergent from mine.
It matters for the syntax and type system I am designing. We are experiencing dissonance because your design is so divergent from mine.
Not realy, if you want to pretty print (A) -> (B) -> World<C> as (A) -> (B) => C you could do that when displaying the types.
You would have to find another way to make sure pure functions don't call impure functions if you want to implement using monads, but my system based on Monads would already do that.
As you can see this excludes the case you are thinking about.
It matters for the syntax and type system I am designing. We are experiencing dissonance because your design is so divergent from mine.
You cannot have a pure function where the return values changes for the same arguments. For a nullary function that means it must always return the same value.
What you seem to be thinking of where a nullary function is a value, and that value can change if properties referenced by that function change. This is not a pure function.
This seems useful because we know which impure interfaces a function employs. But why do we need monads? Instead we could explicitly declare the interfaces a procedure inputs as arguments. Is the only benefit of a monadic effect system that we don't have to write them and they can be inferred? Easier for refactoring?
We need monads to give us a way of encoding the effects in the type system. Type systems are a kind of algebra, and we only have two types of objects to play with, type-constructors, and type-variables. We need to be careful we extend the type system with algebraic properties that preserve all the axioms of the type system, or we create a potentially unsound mess.
You want to lift effects to monadic type constructors. I contemplated that this can also be accomplished with interfaces, which are function type constructors.
The features that benefit most from monads are best described in these three prior cited sources:
http://stackoverflow.com/questions/44965/what-is-a-monad/10245311#answer-10245311
Basically, each monad has its own implementation of the bind function. And you can write a bind function such that it does hoopy things between execution steps. For example:
- If each step returns a success/failure indicator, you can have bind execute the next step only if the previous one succeeded. In this way, a failing step aborts the whole sequence "automatically", without any conditional testing from you. (The
Failure Monad.)- Extending this idea, you can implement "exceptions". (The
Error MonadorException Monad.) Because you're defining them yourself rather than it being a language feature, you can define how they work. (E.g., maybe you want to ignore the first two exceptions and only abort when a third exception is thrown.)- You can make each step return multiple results, and have the bind function loop over them, feeding each one into the next step for you. In this way, you don't have to keep writing loops all over the place when dealing with multiple results. The bind function "automatically" does all that for you. (The
List Monad.)- As well as passing a "result" from one step to another, you can have the bind function pass extra data around as well. This data now doesn't show up in your source code, but you can still access it from anywhere, without having to manually pass it to every function. (The
Reader Monad.)- You can make it so that the "extra data" can be replaced. This allows you to simulate destructive updates, without actually doing destructive updates. (The
State Monadand its cousin theWriter Monad.)- Because you're only simulating destructive updates, you can trivially do things that would be impossible with real destructive updates. For example, you can undo the last update, or revert to an older version.
- You can make a monad where calculations can be paused, so you can pause your program, go in and tinker with internal state data, and then resume it.
- You can implement "continuations" as a monad. This allows you to break people's minds!
All of this and more is possible with monads. Of course, all of this is also perfectly possible without monads too. It's just drastically easier using monads.
Monads are typically used to solve problems like:
- I need to make new capabilities for this type and still combine old functions on this type to use the new capabilities.
- I need to capture a bunch of operations on types and represent those operations as composable objects, building up larger and larger compositions until I have just the right series of operations represented, and then I need to start getting results out of the thing
- I need to represent side-effecting operations cleanly in a language that hates side effects
We’ve composed two functions that take a number and return a number+string pair, and created another function with the same signature, meaning it can be composed further with other debuggable functions.
...
We’ve just implemented what in Haskell is called the List monad, which lets you compose functions that map a single item to a list of items.So what is a monad? Well, it’s a design pattern. It says that whenever you have a class of functions that accept one type of thing and return another type of thing, there are two functions that can be applied across this class to make them composable:
- There is a bind function that transforms any function so that accepts the same type as it returns, making it composable
- There is a unit function that wraps a value in the type accepted by the composable functions.
Afaics, a monadic effect system is really only necessary in a language that only allows pure functions and wants to force pure functional programming style and patterns.
Otherwise the main feature monads can provide for is that we can compose functions that don't operate on the mutable state with functions that do. And that the call hierarchy above the function accessing the said state can be inferred to have the monadic composition semantics. In other words, it lifts state composition from function arguments to monadic type constructors, for which unamplified functions can be implicitly lifted to.
Also monads give us the containment we want. You can only call a
ReadFilefunction from anotherReadFilefunction, so monads ensure that the call graph obeys the set-semantics, so that effect permissions have to be handed down from the main-program (which presumably has permission for all effects). In other worlds the algebraic structure of a monad models the dynamic "inheritance" of effect permissions in the call graph.
We can also accomplish this with interface arguments on function types, but then we can't compose these with functions which aren't lifted to the same types (same tuple of state and other arguments).
Inference isn't really the main distinction as we could also infer interfaces.
This is not a pure function.
That was my point. And please stop trying to say that I am wrong. I know damn well what I wrote was correct w.r.t. to the case where every object is not copied. Whereas you were assuming copying at the fixpoint. Please.
You are the one who doesn't understand both ways of looking at it, and thus you go on and on trying to defend what was a dissonance (where your interpretation was incorrect in my model and I didn't realize you were assuming a different model so I thought you were wrong). And I don't feel like explaining it, because it isn't important that you understand. I understand and this is not that important.
The important point is that type-constraints can only constrain based on what is in the type. So if there is no indication of what effects a function uses in its type, we cannot constrain those properties higher up.
In other words if we express effects as constraints on types, then we will need to introduce a new higher-level concept of constraints-on-constraints in order to be able to constrain the effects that we want to allow in certain parts of the program. Overall it is much more complex to add a whole new layer of complexity to the type system.
That was my point. And please stop trying to say that I am wrong. I know damn well what I wrote was correct w.r.t. to the case where every object is not copied. Whereas you were assuming copying at the fixpoint. Please.
You are the one who doesn't understand both ways of looking at it, and thus you go on and on trying to defend what was a dissonance (where your interpretation was incorrect in my model and I didn't realize you were assuming a different model so I thought you were wrong). And I don't feel like explaining it, because it isn't important that you understand. I understand and this is not that important.
I think you are not doing very well at explaining. If you can't get me to understand, what hope have JavaScript programmers got of understanding it?
However, if it is not that important, maybe we can come back to it another time.
I guess we come back to: Why do we want to have 'pure' functions in the language?
If the compiler can infer purity, then it can automatically make optimisations in the pure case. The programmer does not need to worry about purity annotations.