Ben Rudiak-Gould wrote:
Lennart Augustsson wrote:
What do you mean when you say the interface is pure?
If your module is really pure then there should be an implemenation of it (which could have really bad complexity) with the same observable behaviour that uses only pure Haskell. Is this possible?
Really? I agree with the converse of that statement, but I don't think it goes both ways. To me a function or module is pure when you can use it without compromising the equational properties of the language. I don't think Data.Dynamic or Control.Monad.ST satisfy your criterion for purity, but I would call them pure (after discarding the functions marked unsafe in the latter).
Agreed, there can pure functions that cannot be written with the pure primitives, but then you have a proof obligation. An "easy" way to prove it is to provide an equivalent implementation that uses only pure functions. As far as I remember Control.Monad.ST can be written purely. And I think the same is true for Data.Dynamic. -- Lennart