Barb Knox
2008-01-20 20:22:01 UTC
Re: <http://www.jucs.org/jucs_10_7/total_functional_programming>
cases that a trivial inference system will cover. Something along the
lines of Hindley-Milner, for example, should fully suffice (though one
may have to adapt H-M to get the distinction right).
Right, but one of the main points of the paper was that this is really
enough for almost everything that's actually interesting. In
particular the language can express any function that's provably total
in second order arithmetic, which encompasses just about everything in
mathematics outside of set theory.
One interesting point which I hadn't come across before is on p 766:
| Theorem: For any language in which all programs terminate, there are
| always-terminating programs which cannot be written in it - among
| these are the interpreter for the language itself.
The proof is simple yet interesting; I'm surprised this didn't come up
in the comp theory classes I took.
[added comp.theory, comp.edu]
I think the idea of codata combined with totality is that a program
operating on codata is guaranteed to work its way through each element
of even an infinite data stream. I.e. for any N we will eventually
get to the Nth element.
Well, sure, but being structural, this covers just all those simpleoperating on codata is guaranteed to work its way through each element
of even an infinite data stream. I.e. for any N we will eventually
get to the Nth element.
cases that a trivial inference system will cover. Something along the
lines of Hindley-Milner, for example, should fully suffice (though one
may have to adapt H-M to get the distinction right).
enough for almost everything that's actually interesting. In
particular the language can express any function that's provably total
in second order arithmetic, which encompasses just about everything in
mathematics outside of set theory.
| Theorem: For any language in which all programs terminate, there are
| always-terminating programs which cannot be written in it - among
| these are the interpreter for the language itself.
The proof is simple yet interesting; I'm surprised this didn't come up
in the comp theory classes I took.
[added comp.theory, comp.edu]
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------