Re: [Qi] Fwd: book deal goes through with printer

["Jonathan Tran" <jonnytran@gmail.com>]

I hadn't heard of total functional programming before. But it looks
very interesting. Thanks.

On Fri, Sep 19, 2008 at 11:52 AM, Mark Dominus
<mjd-phillylambda@plover.com> wrote:
>
>
>> >> Don't know if any of you guys are following Qi,
>
> I wasn't, but I will now.  Thanks for the pointer.  Using sequent
> calculus is a really clever idea.
>
> I'll also ask the Penn library to obtain a copy of the book.
>
>> That is, in fact, one aspect of Qi that is invisible in most other
>> languages: the type-system in Qi has the halting problem.
>
> Lately I've been reading a bunch of papers about languages that go in
> the other direction, and which aren't subject to the halting problem
> at all.
>
> This turns out to be unexpectedly useful.
>
> Such languages can't express every possible algorithm, but it's not
> that important, because in typical programming contexts we only write
> functions that are guaranteed to halt anyway; this is the usual
> definition of "algorithm".
>
> One example is the paper "Total Functional Programming", by D. A. Turner.
> http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf
>
>         Abstract: The driving idea of functional programming is to
>         make programming more closely related to mathematics. A
>         program in a functional language such as Haskell or Miranda
>         consists of equations which are both computation rules and a
>         basis for simple algebraic reasoning about the functions and
>         data structures they define. The existing model of functional
>         programming, although elegant and powerful, is compromised to
>         a greater extent than is commonly recognised by the presence
>         of partial functions. We consider a simple discipline of
>         total functional programming designed to exclude the
>         possibility of non-termination. Among other things this
>         requires a type distinction between data, which is finite,
>         and codata, which is potentially infinite.
>
> Turner's initial point is that the presence of _|_ values in languages
> like Haskell spoils one's ability to reason from the program
> specification.  His basic example is simple:
>
>        loop :: Integer -> Integer
>        loop x = 1 + loop x
>
> Taking the function definition as an equation, we subtract (loop x)
> from both sides and get
>
>        0 = 1
>
> which is wrong.  The problem is that while subtracting (loop x) from
> both sides is valid reasoning over the integers, it's not valid over
> the Haskell Integer type, because Integer contains a _|_ value for
> which that law doesn't hold: 1 /= 0, but 1 + _|_ == 0 + _|_.
>
> Before you can use reasoning as simple and as familiar as subtracting
> an expression from both sides, you first have to prove that the value
> of the expression you're subtracting is not _|_.
>
> By banishing nonterminating functions, one also banishes _|_ values,
> and familiar mathematical reasoning is rescued.
>
> Also:
>
>        http://en.wikipedia.org/wiki/Total_functional_programming
>
> Sorry, that turned out to be a much longer digression than I expected.
> I did not mean to distract attention from Qi.
>
> I wish Professor tarver had not written his web pages in white text on
> a black background.
>
>