8 ms·

Total Functional Programming (2004) [pdf]

89 points by leonidasv 3y ago

lynx23 3y ago
20 year old paper. People interested in total functions should probably have a good look at Idris.
FrustratedMonky 3y ago
Isn't this handled by 'purity' of functions? It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Isn't that all also solved by pure functions? And is incorporated into functional languages at this point?
- gpderetta 3y ago
  the big Idea is that the language is non-Turing complete and termination can be proven (and co-data is used for non-terminating programs).
  - zarathustreal 3y ago
    I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal
    - anon291 3y ago
      Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.
      - zarathustreal 3y ago
        I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
        anon291 3y ago
        Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
        zozbot234 3y ago
        But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.
- tromp 3y ago
  No; purity is an orthogonal notion. Haskell functions are pure in that given the same arguments, a function always produces the same output. But Haskell functions can be partial; for some arguments there is no output, or the output is undefined. Turner proposes a language for pure total functions.
- 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 ago
    Guess, 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 ago
      This 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.
- lynx23 3y ago
  No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.
  - FrustratedMonky 3y ago
    Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
    - lynx23 3y ago
      Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.
  - justincredible 3y ago
    [dead]
btreecat 3y ago
> to make programming more closely related to mathematics Why is this taken as a given to be a good thing? Our hardware has state. Any IO is a side effect, so what's the non trivial use case for "pure functions" all the way down? I think FP paradigms can be useful in specific problem domains, I'm skeptical of the general utility (vs resource spend) of strong FP languages.
- llm_trw 3y ago
  Because a stateless program can execute in only one way for any given inputs. A stateful program can execute in 2^n different ways for each bit of state for any given inputs.
  - mrkeen 3y ago
    > 2^n If it only computes from an expression to an expression. I think the bound might be higher if you use imperative statements (/effects). You can fill the whole 2^n output space by calling random(). But in addition to that, the program might also delete an arbitrary file, or deadlock, etc.
- diggan 3y ago
  As you say, you cannot make a 100% side-effect free program, unless it doesn't do anything at all. But I do think it's valuable to aim for as side-effect-free as possible, and concentrate the statefulness into certain part(s), rather than spread out all over the place, which is the typical way typical.
  - btreecat 3y ago
    Practicing software architecture should generally lead you to minimize side effects and efficiently manage sections of state small enough to fit into your working memory IMO. FP can be used to get you there, but it strongly optimizes for readability of experts in most cases which harms readability in general, as there are always fewer experts. At least that's been my experience with FP languages in the professional space. People often underestimate the benefits of good tooling, a large community, and deep candidate pool.
agentultra 3y ago
I like how Lean4 handles totality. You can tell the compiler to trust you. Or you can provide a proof. The latter is more useful while the former is sometimes pragmatic.
llmzero 3y ago
In page 2, there is the theorem: Theorem ∀n in Nat.f n (fib p) (fib (p+1)) = fib (p+n), I think it should be for all p in Nat (fib p) + (fib (p+1)) = fib(p+2), otherwise there is something mysterious here.
- mayoff 3y ago
  The fib' function (the more efficient version of fib) is defined using f. So the goal is to prove that f computes the same thing as fib (given the appropriate arguments to f and fib). Hence the theorem needs to use f on at least one side of the equation.
JonChesterfield 3y ago
A few comments have cheerfully reproduced the stock objection that a program with no side effects does nothing and is thus useless. By extension functional programming is useless and it's all pointless. I'd like to counter that a function from vector of bytes to vector of bytes can be pure, terminating, implement some algorithm of great commercial interest and map exactly onto a program that reads said vector of bytes from stdin and sends them to stdout. If you're really generous, it can write two vectors of bytes, and tie the other one to stderr. That covers such useless academic things as your compiler.
- kstrauser 3y ago
  I guess that depends on whether you consider write(2) to have side effects. No, really, I've been in the room when people debated whether that was pure enough. It's an interesting exercise to talk through, at least.
  - mrkeen 3y ago
    Even taking write as an effect (which I do), that doesn't stop it from being a trivial attachment to an otherwise pure artifact. IO in -> pure stuff of interest -> IO out The purity is in no way compromised by being IO-adjacent.
  - JonChesterfield 3y ago
    I think that's an aliasing question. If write is sending bytes to somewhere else, it's pure. In exactly the same way that returning a value type from a function is pure, or passing a value type to some other function is pure. Since they're all the same thing. A unix process is a function in a literal sense. If you've aliased read and write to the same thing then mutation is back with us and sorrows return. Vaguely tangential, it's totally possible to write a program that uses read() to copy all of stdin to its own address space allocated with brk(), does whatever maths it wants, then sends some of the result back out with write(). Three syscalls, useful userspace program, no libc involved.
- jrvarela56 3y ago
  This talk [1] made me conclude something along these lines. You need side-effects to make anything useful, just make sure they're segregated in a specific place in your program. This makes it easier to make most of the program pure and make it clear where the dangerous stuff happens. [1] Boundaries by Gary B. from Destroy All Software https://www.youtube.com/watch?v=yTkzNHF6rMs https://www.youtube.com/watch?v=yTkzNHF6rMs
munchler 3y ago
I appreciate this article. It's clear, easy to understand, and uses theory to propose practical improvements to FP. Some minor nitpicks: > In total functional programming ⊥ does not exist. That doesn't seem right. In total FP, we can still define a ⊥ type that has no values. I think the problem here is that the author uses ⊥ to indicate both a type and a value of that type (e.g. f ⊥ = ⊥), which is confusing. > 0 / 0 = 0 Surely it would be better to use a Maybe type for this instead? 0 / 1 = Just 0 0 / 0 = Nothing The same approach also addresses the difficulty of hd: hd :: List a -> Maybe a hd (Cons a x) = Just a hd Nil = Nothing F# has this function, and calls it "tryHead", rather than just "head".
- lgas 3y ago
  > Surely it would be better to use a Maybe type for this instead? > > 0 / 1 = Just 0 > 0 / 0 = Nothing This would make it impossible to compose mathematical expressions of more than one operation without discharging the Maybe which would get ugly fast.
  - munchler 3y ago
    But that's the true nature of division. Unless one can prove that the denominator is non-zero, then the computation is not well defined. Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.
    - trealira 3y ago
      It seems like it would be more practical to create non-zero integer/other number types, and only those can be used as denominators. But it would also be nice to not have to make a custom subtype every time you needed something with a specific property.
      - munchler 3y ago
        Agreed. I think this is where dependent types become useful, but that is a whole can of worms.
pmcjones 3y ago
Did anyone notice the fib function on the first page? It doesn't terminate: fib :: Nat->Nat fib 0 = 0 fib 1 = 1 fib (n+2) = fib (n+1) + fib (n+2) The last line should be fib (n+2) = fib (n+1) + fib (n). The published version seems to have the same problem: https://pdfs.semanticscholar.org/82b4/ea72b89270c528006dd2532aef43eec463c3.pdf https://pdfs.semanticscholar.org/82b4/ea72b89270c528006dd253...
082349872349872 3y ago
See also discussion (2007) at http://lambda-the-ultimate.org/node/2003 http://lambda-the-ultimate.org/node/2003 (which mentions http://pll.cpsc.ucalgary.ca/charity1/www/home.html http://pll.cpsc.ucalgary.ca/charity1/www/home.html )

89 points by leonidasv 3y ago

20 year old paper. People interested in total functions should probably have a good look at Idris.

Isn't this handled by 'purity' of functions? It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Isn't that all also solved by pure functions? And is incorporated into functional languages at this point?

gpderetta 3y ago
the big Idea is that the language is non-Turing complete and termination can be proven (and co-data is used for non-terminating programs).
- zarathustreal 3y ago
  I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal
  - anon291 3y ago
    Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.
    - zarathustreal 3y ago
      I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
      - anon291 3y ago
        Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
      - zozbot234 3y ago
        But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.
tromp 3y ago
No; purity is an orthogonal notion. Haskell functions are pure in that given the same arguments, a function always produces the same output. But Haskell functions can be partial; for some arguments there is no output, or the output is undefined. Turner proposes a language for pure total functions.
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 ago
  Guess, 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 ago
    This 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.
lynx23 3y ago
No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.
- FrustratedMonky 3y ago
  Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
  - lynx23 3y ago
    Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.
- justincredible 3y ago
  [dead]

btreecat 3y ago

> to make programming more closely related to mathematics Why is this taken as a given to be a good thing? Our hardware has state. Any IO is a side effect, so what's the non trivial use case for "pure functions" all the way down? I think FP paradigms can be useful in specific problem domains, I'm skeptical of the general utility (vs resource spend) of strong FP languages.

llm_trw 3y ago
Because a stateless program can execute in only one way for any given inputs. A stateful program can execute in 2^n different ways for each bit of state for any given inputs.
- mrkeen 3y ago
  > 2^n If it only computes from an expression to an expression. I think the bound might be higher if you use imperative statements (/effects). You can fill the whole 2^n output space by calling random(). But in addition to that, the program might also delete an arbitrary file, or deadlock, etc.
diggan 3y ago
As you say, you cannot make a 100% side-effect free program, unless it doesn't do anything at all. But I do think it's valuable to aim for as side-effect-free as possible, and concentrate the statefulness into certain part(s), rather than spread out all over the place, which is the typical way typical.
- btreecat 3y ago
  Practicing software architecture should generally lead you to minimize side effects and efficiently manage sections of state small enough to fit into your working memory IMO. FP can be used to get you there, but it strongly optimizes for readability of experts in most cases which harms readability in general, as there are always fewer experts. At least that's been my experience with FP languages in the professional space. People often underestimate the benefits of good tooling, a large community, and deep candidate pool.

agentultra 3y ago

I like how Lean4 handles totality. You can tell the compiler to trust you. Or you can provide a proof. The latter is more useful while the former is sometimes pragmatic.

llmzero 3y ago

In page 2, there is the theorem: Theorem ∀n in Nat.f n (fib p) (fib (p+1)) = fib (p+n), I think it should be for all p in Nat (fib p) + (fib (p+1)) = fib(p+2), otherwise there is something mysterious here.

mayoff 3y ago
The fib' function (the more efficient version of fib) is defined using f. So the goal is to prove that f computes the same thing as fib (given the appropriate arguments to f and fib). Hence the theorem needs to use f on at least one side of the equation.

JonChesterfield 3y ago

A few comments have cheerfully reproduced the stock objection that a program with no side effects does nothing and is thus useless. By extension functional programming is useless and it's all pointless. I'd like to counter that a function from vector of bytes to vector of bytes can be pure, terminating, implement some algorithm of great commercial interest and map exactly onto a program that reads said vector of bytes from stdin and sends them to stdout. If you're really generous, it can write two vectors of bytes, and tie the other one to stderr. That covers such useless academic things as your compiler.

kstrauser 3y ago
I guess that depends on whether you consider write(2) to have side effects. No, really, I've been in the room when people debated whether that was pure enough. It's an interesting exercise to talk through, at least.
- mrkeen 3y ago
  Even taking write as an effect (which I do), that doesn't stop it from being a trivial attachment to an otherwise pure artifact. IO in -> pure stuff of interest -> IO out The purity is in no way compromised by being IO-adjacent.
- JonChesterfield 3y ago
  I think that's an aliasing question. If write is sending bytes to somewhere else, it's pure. In exactly the same way that returning a value type from a function is pure, or passing a value type to some other function is pure. Since they're all the same thing. A unix process is a function in a literal sense. If you've aliased read and write to the same thing then mutation is back with us and sorrows return. Vaguely tangential, it's totally possible to write a program that uses read() to copy all of stdin to its own address space allocated with brk(), does whatever maths it wants, then sends some of the result back out with write(). Three syscalls, useful userspace program, no libc involved.
jrvarela56 3y ago
This talk [1] made me conclude something along these lines. You need side-effects to make anything useful, just make sure they're segregated in a specific place in your program. This makes it easier to make most of the program pure and make it clear where the dangerous stuff happens. [1] Boundaries by Gary B. from Destroy All Software https://www.youtube.com/watch?v=yTkzNHF6rMs https://www.youtube.com/watch?v=yTkzNHF6rMs

munchler 3y ago

I appreciate this article. It's clear, easy to understand, and uses theory to propose practical improvements to FP. Some minor nitpicks: > In total functional programming ⊥ does not exist. That doesn't seem right. In total FP, we can still define a ⊥ type that has no values. I think the problem here is that the author uses ⊥ to indicate both a type and a value of that type (e.g. f ⊥ = ⊥), which is confusing. > 0 / 0 = 0 Surely it would be better to use a Maybe type for this instead? 0 / 1 = Just 0 0 / 0 = Nothing The same approach also addresses the difficulty of hd: hd :: List a -> Maybe a hd (Cons a x) = Just a hd Nil = Nothing F# has this function, and calls it "tryHead", rather than just "head".

lgas 3y ago
> Surely it would be better to use a Maybe type for this instead? > > 0 / 1 = Just 0 > 0 / 0 = Nothing This would make it impossible to compose mathematical expressions of more than one operation without discharging the Maybe which would get ugly fast.
- munchler 3y ago
  But that's the true nature of division. Unless one can prove that the denominator is non-zero, then the computation is not well defined. Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.
  - trealira 3y ago
    It seems like it would be more practical to create non-zero integer/other number types, and only those can be used as denominators. But it would also be nice to not have to make a custom subtype every time you needed something with a specific property.
    - munchler 3y ago
      Agreed. I think this is where dependent types become useful, but that is a whole can of worms.

pmcjones 3y ago

Did anyone notice the fib function on the first page? It doesn't terminate: fib :: Nat->Nat fib 0 = 0 fib 1 = 1 fib (n+2) = fib (n+1) + fib (n+2) The last line should be fib (n+2) = fib (n+1) + fib (n). The published version seems to have the same problem: https://pdfs.semanticscholar.org/82b4/ea72b89270c528006dd2532aef43eec463c3.pdf https://pdfs.semanticscholar.org/82b4/ea72b89270c528006dd253...

082349872349872 3y ago

See also discussion (2007) at http://lambda-the-ultimate.org/node/2003 http://lambda-the-ultimate.org/node/2003 (which mentions http://pll.cpsc.ucalgary.ca/charity1/www/home.html http://pll.cpsc.ucalgary.ca/charity1/www/home.html )