Open daira opened 8 years ago
:+1:
PRS are always welcome. Understandability is more important than accuracy in this document so if you can think of a good, simple wording I'm sure it'll get pulled
Feel free to assign this to me.
@daira Thank you, please feel free to do a PR.
Untill now I understood that referencial transparency and purity were the same thing, but it turns out a function can be referentially transparent and have side effects, so it is not pure.
Any reason why Referencial Transparency is so far below purity and side-effects? I think the right order of jargons helps alot, and as I understand that purity = referential transparency + no side effects
purity should be last shown of these three.
I am new to these concepts and haven't used any strictly functional language yet, so feel free to ignore me.
A side effect is an operation which is not pure. The purity implies the referential transparency (see the confluence of the lambda calculus). A function can also be observationaly pure, but with side effects inside. For example :
function sum(a, b) {
let s = a;
s = s + b;
return s;
}
We do a mutation s = s + b
, so a side effect. However, the function sum
is observationaly pure as it always returns the same result given the same arguments, and does not modify its environment.
Interesting classification of effects done in this paper
but the basic effects defined in Koka are
total
,exn
,div
,ndet
,alloc<h>
,read<h>
,write<h>
, andio
. Of coursetotal
is not really an effect but signifies the absence of any effect and is assigned to pure mathematical functions. When a function can throw an exception, it gets theexn
effect. Potential divergence or non-termination is signified by thediv
effect. Currently, Koka uses a simple termination analysis based on inductive data types to assign this effect to recursive functions. Non-deterministic functions get thendet
effect. The effectsalloc<h>
,read<h>
andwrite<h>
are used for stateful functions over a heaph
. Finallyio
is used for functions that do any input/output operations.alias total = <>
alias pure = <exn, div>
alias st<h> = <alloc<h>, read<h>, write<h>>
alias io = <st<ioheap>, pure, ndet>
Add totality definition http://alvinalexander.com/photos/totality-rule-functional-programming
The definitions of purity and side effects are ambiguous. For instance, suppose we have a function that reads, but does modify, state that is reachable from its inputs. Is that a "pure" function? Typically it wouldn't be considered to be pure, but it does not have side effects as-defined, and whether it should be considered to return a value that only depends on its inputs is unclear (since the definition doesn't say that the inputs must be stateless values).