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

[mjd-phillylambda@plover.com (Mark Dominus)]

> >> 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.