How to tell if an F# function is pure?

Question

Suppose I have these two F# functions:

let sq x = x*x

let tm = DateTime.Now

Clearly sq is pure in that it will always return the same value for a given input while tm is impure 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 pure or impure 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 pure or impure when you write it?

Finally when calling a function that is part of the common language runtime (such as DateTime) how can one tell if it is pure or impure without trying it?

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

In computer programming, a function may be described as pure if both these statements about the function hold:

1. The function always evaluates the same result value given the same argument value(s). The function result value cannot depend on any hidden information or state that may change as program execution proceeds or between different executions of the program, nor can it depend on any external input from I/O devices.

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

Answer 1

F# does not provide any features and tools for checking that methods are pure, so a simple answer is that you have to check this property yourself.

Outside of F#, it is worth noting that Code Contracts library has a notion of pure methods (and they can be marked with PureAttribute), but I'm not entirely sure what is the checking story there. I think Code Contracts come with static checker that analyses IL (and should work for F# too), but this is quite difficult task, so I would expect it to be quite limited. However, the PureAttribute is used on some BCL methods, so you can tell that some standard .NET methods are pure.

Answer 2

Technically speaking your 'tm' value is not a function, but value of type DateTime and it is immutable, so every time you evaluating this value after creating it will always be the same.

Answer 3

Given that it is possible to define both, pure and inpure functions in f#, I would be well surprised if there was an algorithm that can check f# code (function definitions) for purity -- checking program code for semantic properties is generally undecidable by Rice's theorem.