How to determine if a F # function is clean?

Question

Suppose I have two F # functions:

let sq x = x*x let tm = DateTime.Now 

Obviously, sq is clean because it will always return the same value for a given input, while tm is unclean because it will return a different value each time it is called.

In general, is there a way to determine if a particular function in F # is clean or unclean without analyzing what it does, in other words, reading it line by line?

Alternatively, is there a way to annotate a function to tell the compiler that the function is clean or unclean when you write it?

Finally, when calling a function that is part of a common language runtime (such as DateTime), how can you determine if it is clean or unclean without trying to execute it?

Note: by “clean” I mean the definition from Wikipedia: http://en.wikipedia.org/wiki/Pure_function ( permalink )

In computer programming, a function can be described as pure if both of these statements about the function being performed are:

• The function always evaluates the same value of the result, given the same argument of the value). The value of the result of the function cannot depend on hidden information or the state, which can change as the program continues to run or between different program executions, and cannot depend on any external input from input / output devices.

• Evaluation of the result does not cause any semantically observable side effect or output, such as mutation of mutable objects or output to input / output devices.

Answer 1

F # does not provide any functions and tools to verify that the methods are clean, so the simple answer is that you must verify this property yourself.

Outside of F #, it should be noted that the Code Contracts in the library have the concept of pure methods (and they can be labeled PureAttribute ), but I'm not quite sure what is going on there. I think Code Contracts comes with a static controller that parses IL (and should work for F # too), but this is a pretty tricky task, so I expect it to be very limited. However, PureAttribute used for some BCL methods, so you can say that some standard .NET methods are clean.

Answer 2

From a technical point of view, your value of "tm" is not a function, but a value of the DateTime type and unchanged, so every time you evaluate this value after it is created, it will always be the same.

Answer 3

Given that both pure and inclusive functions can be defined in f #, I would be surprised if there was an algorithm that could check the f # code (function definitions) for checking purity - the program code for semantic properties is usually unsolvable by the theorem Rice.