3 ms·
> It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Well no. This is computer science 101. Anything that can
by anon291 3y ago
> It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'.
Well no. This is computer science 101. Anything that can compute anything useful (ie. Turing complete or lambda-calculus-complete... they're equivalent) cannot be said to produce an answer in finite time (or at all really). In FP parlance, we say that such functions are a 'bottom' value. The notation 'Int -> Int' in a language like haskell is a function that takes an Int and returns an Int, if it terminates.
In a total language, you're guaranteed to have an Int after invoking the function within a finite amount of time, even if that time is greater than the age of the universe. But it will eventually return an answer. Whereas a haskell program may truly never terminate.
Here is an example of a haskell program that is syntactically correct and well-typed but is actually a bottom, despite the type signature claiming in returns Int
f :: Int -> Int
f x = f x
- FrustratedMonky 3y agoGuess, that is what I was asking. If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. Because if there are no outside interactions inside the function, it's 'pure', then the Int->Int is guaranteed. Doesn't using only pure functions, equate to this Total Functions.
- deleted 3y ago[deleted]
- FrustratedMonky 3y agoThis might be one of those 'sloppy' definitions. From random search, seems like some people assume this : Pure=Total "A pure function must be total Firstly, a function must be total, this means that for each input that is provided to the function there must be a defined output."
- anon291 3y ago> If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. The function above is pure. In fact, all functions in Haskell are, even those returning IO.
- FrustratedMonky 3y agoThen they are also 'total' by some definitions. So they would match the criteria of the original post? By some definitions, to be 'pure' includes being 'total'. Guess, back to original question. The ideas in this paper from 2004, seems to have been incorporated into more common languages like Haskell in 2024.