Lambda the Ultimate

Are there any works connecting theoretical foundatins of OO, and coalgebras?

Yes indeed.

Bart Jacobs. Objects and classes, coalgebraically. In B. Freitag, Cliff Jones, C. Lengauer, and H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence, pages 83--103. Kluwer, 1996.

Bart Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming (ECOOP96), number 1098 in Lecture Notes in Computer Science, pages 210--231. Springer-Verlag, 1996.

Bart Jacobs. Coalgebraic Reasoning about Classes in Object-Oriented Languages. Electronic Notes in Theoretical Computer Science 11 (1998), pp. 1-12.

Unfortunately, I could not find copies of these online anymore. However, I have a copy of the first and the last, and I could probably find a copy of the second if someone wants me to email them. However, I'm not sure if it's strictly above board (the "secret paper-passing network" and so on), so I suggest you contact Jacobs about it first if you don't have access to a CS library.

How well all this connects to Charity, I don't know. [..] Is there any recent work on Charity? Can anyone share expereinces with using it?

No recent work, unfortunately, though they have a newer compiler. I'm not sure what's happening over there. There was a gap of several years with no papers, and then suddenly a release of the source code or something.

Anyway, coinductive datatypes in Charity model the "observations" aspect of OO programming, but not the dynamic binding. For that you need cofree coalgebras, as mentioned in Jacobs paper above. These things are not far from existential types.

I have it on authority from Jeff Lewis, who co-authored a paper on dynamic binding in Haskell, Implicit Parameters: Dynamic Scoping with Static Types, that the semantics for this is closely related to the one for the first-order binder which is used in Charity. There is a paper by Masahito Hasegawa which deals with a dual decomposition of the lambda binder of lambda-calculus: Decomposing typed lambda calculus into a couple of categorical programming languages. It treats the Charity binder and its dual, though in the more general setting of premonoidal categories.

Hasegawa's work is inspired by a paper of Jacobs and Hermida: Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi.

There is also work by Hugo Herbelin, for example A lambda-calculus structure isomorphic to sequent calculus structure, which I feel is very closely related. Also the extensive literature on explicit substitutions is relevant, but it's too much to get into here.

Of course I'm hoping to get some response from the functional people here explaining why named product of types is not a good idea.

data List = Nil | 
            Cons { 
              head :: Integer, 
              tail :: List 
            }

Cons 1 (Cons 2 Nil)
Cons { head = 1, tail = Cons { head = 2, tail = Nil }}

does that meet your need, or are you asking for something else?

My personal point of view is that encapsulation is a core issue, so I don't want field names to be visible. You access the data via access methods (and these are among the operations in your [bi]algebra, along with the constructors).

It's not just objects. Everywhere tuples are used, you have the problem of making the purpose of the data unclear, f.e. :

doSomething True True False

But naming each item makes it much more clear: (just making this up)

doSomething now:True recursive:True allowNothing:False

In the (co)algebra papers this becomes worse, because the authors seem to like vague tuple constructors and destructors (iota and pi with an accent to the left or right) which means you have no handles for understanding the formulas.

From a tuple (1,2) you can't see if it came from a sum or a product, but {tag=1, value=2} would make that clearly a sum.

data CalendarTime = 
  CalendarTime {
    ctYear :: Int,
    ctMonth :: Month,
    ctDay :: Int,	
    -- etc.
  }

In Scheme one could if one wished supply a parameter list to a constructor function as a series of pairs, e.g.:

(make-foo '((name myfoo) (value somevalue)))

(define make-foo
   (lambda (parameters)
      ((lambda (name value) <body of actual constructor function>)
       (get-field name parameters) (get-field value parameters))))

Perhaps the foo constructed by make-foo turns out to be '((name myfoo) (value somevalue)), which is not too opaque; and perhaps you have accessors/destructors called foo-name and foo-value that hide the implementation anyway. Come to think of it, there's nothing to stop your foo from having '((name = myfoo) (value = somevalue)) as its internal representation...

(...edited to undo antisocial side-effects of pre and font tags)

Everywhere tuples are used, you have the problem of making the purpose of the data unclear
Fumbling with CLEAN I started to comment field names beneath the data type definitions ;-) Eventually I realized that not only can CLEAN record types replace tuples, but record types are basically algebraic data types (with selection by name not position).

Is it that record types / named fields are a recent (and "unchallenging") addition to functional programming languages? Or is it the idea that it's better to have a small number of datatypes, rather than a large number of data types that require special functions?

I found this statement (on the Charity home page) rather arresting:

All Charity computations terminate (up to user input).

I don't know anything about Charity, but if you ask yourself what causes non-termination we can probably figure out what kinds of structures it rules out.

The most pernicious form of non-termination arises from an unconverging recursive loop. To take a classic example:

(define self-apply
   (lambda (x)
     ( x x )))

What happens if you call ( self-apply self-apply)? You get an infinite loop of calls to the function.

In a language with an appropriate type discipline, this function can't be defined. To see why, let's start by assigning it type A->B (it takes something of type A and returns something of type B).

But our definition has it applying to itself, so it would have to be of type (A->B)->B. But if it had this type, its self-application would have to be of type ((A->B)->B)->B, and so on. This means that it can't be assigned a valid type, and is ruled out by the type system.

This is one feature that the Charity type system must have to make the claim of non-termination.

Is there any type of useful program that it would be impossible to write in a language that ensured that its computations terminated?

This depends on your definition of "useful". ;-) There may be programs with such a potential "hole" that do wonderful things if you can avoid stepping in the hole. Whether losing these to the type checker is a worthwhile sacrifice or not probably depends on how concerned you are about "holes" in programs, and how well you believe you can tap-dance around them.

Would such a language even be Turing complete?

So long as it has some representation of "bottom" (loosely speaking, the "value" of a non-terminating function or undefined value), I think the answer is yes.

So long as it has some representation of "bottom" (loosely speaking, the "value" of a non-terminating function or undefined value), I think the answer is yes.

I disagree. It seems like a turing complete language that always terminates or catches the non-termination violates the halting problem.

You'll notice the proviso in the original claim about Charity: All Charity computations terminate (up to user input).

This suggests there are still inputs that may cause non-termination, and you can't tell which ones have this property a priori, so the halting problem is intact.

Perhaps the claim might be better worded "this language guarantees that all non-terminating conditions that can be statically eliminated are."

In a language with an appropriate type discipline, this function can't be defined.

Bang goes your Y combinator, then (well, maybe not, as in Haskell it looks like y f = f (y f)...)

OK, I'm going to cheat and pinch the example given in The Little Schemer, since it's fresh in my mind. Define a function which takes a list, whose every member is either a non-numeric symbol or a list index, and a list index. If the member indexed by the supplied index is a non-numeric symbol, terminate returning that symbol. If it's a list index, pass the list and that index back in to the function. This function will terminate for '(2 6 5 3 end 4), wherever you start in the list, but will never terminate for '(4 end 6 3 1 5) unless you start on the second member.

Now for a compiler to know, given the list supplied to the function as part of the program (rather than user input, which falls under the escape clause), whether evaluation of that function will terminate or not, it needs to be able to distinguish between lists that contain circular sequences of indices and lists that eventually reach a termination point. That's not a problem - it's certainly not the halting problem, for instance - but I am intrigued as to how any type system can be used to determine both that this distinction must be made and how to make it.

My understanding of this is that you don't have a single Y combinator as you do in Scheme, but rather a parameterized "family" of combinators. Less convenient maybe, but the necessary effect is still there.

example given in The Little Schemer

Can you give the page ref? I couldn't find it. (Though I vaguely recall this example...)

given the list supplied to the function as part of the program (rather than user input, which falls under the escape clause)

I'm not sure it does fall outside of the escape clause. User input is a somewhat ambiguous term; it can mean literally IO from outside the system, or it can mean simply input fed to a function. The example you give works precisely because it IS data that is fed to "dumb" function that knows nothing about the structure of what's passed to it.

So that's the easy way out, but there might be a way to handle this using lazy evaluation and referential transparency. (BTW, I have no idea if Charity actually does this; I skimmed the docs and couldn't quickly find the answer ;-) ).

Let's say that there is strict rule of lazy evaluation and memoization of results. So once f(x) is evaluated, the program remembers what the value was and subsequent calls just return the value without recalculating it. Now the example you give is going to be a recursive function something like:

(define index-recurse
  (lambda (index list)
    ( if ( equal? 'end (list-ref list index))
      #t
      (index-recurse index list))))

Since the list is constant and the index will be the same when the process "loops". The strict laziness and referential transparency principle would require that that last call simply return the previous incomplete evaluation and "terminate", i.e. stop evaluating and return "bottom".

This could be bolstered by a number of other conditions on well-typed functions and some enforcement of totality on the function (e.g. making sure all valid cases were handled).

This is all mad speculation, but you could see how this could conceivably be handled.

(Now my curiosity is piqued; I'll have to read those darned Charity papers after all... ;-) )

I doubt it. What does "statically eliminated" mean?

Ok, I know what it means, I just mean you need to specify what system is being used to do so. "X is provable" is ill-formed; we need to know what system is meant. Similarly, "X is unprovable" or "X halts, but this can't be shown" is meaningless without a specified system.

I can see now how laziness + memoization would supply a way out for a certain set of cases, including mine. I'm still wondering whether there isn't a way to beat the system, though. It does seem like a very strong claim!

The start of chapter 9 of TLS introduces a function called "looking", which is what I based my example on.

Would such a language even be Turing complete?

No, Charity is not Turing-complete. I think what is meant by "terminates up to user input" is that a program may block on user input, so if an input action is never completed then obviously the program will never terminate. I am almost positive that it is not the case that some inputs could cause a program to diverge, as Marc suggested.

However, you can write Ackermann's function in Charity, so the complexity bound is quite high.

You would be justified in claiming that Charity is not a programming language, since the usual definition of "programming language" demands Turing-completeness.

Dominic wrote: Define a function which takes a list, whose every member is either a non-numeric symbol or a list index, and a list index...

What you defined here is a algorithm which may not terminate on all inputs, ergo it is not definable in Charity.

OTOH, your algorithm is not very good. Your list is just a representation of a graph, and the function you probably want is the one which decides if its input has cycles. That is a decidable problem. For example you can do it by doing two depth-first traversals and one graph transposition, and I'm fairly confident this can be done in Charity. Such a function would have type list(a) -> bool, so the type system doesn't have to distinguish between "cyclic" and "non-cyclic" list-representations of graphs.

Sjoerd wrote: Of course I'm hoping to get some response from the functional people here explaining why named product of types is not a good idea.

A product of two types is always "named", namely by the projections. When you write (x,y) you are saying, "Give me a tuple, consisting of x and y, so that fst will return x and snd will return y." The projections fst and snd are not usually mentioned when you construct them because they're implicitly tied to the constructor (,), so it would be superfluous. You could, of course, allow the user to mention them, using record label syntax like Bryn showed. But that is just syntax.

Here is an observation which may clarify why products are always named, if you think carefully about it. Instead of building my tuple of x and y with the syntax (,), I could define a function with a different name:

pair y x = (x, y)
first (x,y) = y
second (x,y) = x

and now write pair y x. Now the components are in a different order, and y is labeled with first while x with second. pair is not a constructor in the Haskell sense, but it is a constructor in the categorical sense, because it is equal to (,). Furthermore, first and second are projections of the product. It just so happens that first is equal to snd.

If you think carefully about this, you will see that products are not ordered in any sense; they're always named, but the names are functions, so there is a notion of equality between names. The usual notion of a "name" is something without equality, just a member of a set, but here it is more complex.

From a tuple (1,2) you can't see if it came from a sum or a product, but {tag=1, value=2} would make that clearly a sum.

Writing (1,2) for a value of a sum is abuse of notation, which some authors use liberally. You shouldn't read too much into it.

BTW, on your webpage you write:

Now the constructors and destructors are defined together. The storage spaces Cons provides are in effect named. This is for me the most important reason why Object Oriented style works.

The thing is, your semi-Haskell version above and the OO version below do not define the same thing. The Haskell head and tail functions are partial, while your OO counterparts are total.

I think you are missing the fact that head and tail are not destructors for the List type. The destructor for the list type is foldr, which is total.

Darn, Frank, you made me have to do some research. ;-)

The claim of guaranteed termination seems to rest on a result by Hagino in his thesis that any program constructed with his Categorical Specification Language normalizes.

The thesis seems well-written and interesting, but will take some time to digest. ;-) At this point, I'm mainly interested in finding out what is given up to get the termination property.

At first glance, it looks like the trick is that all operations that can be defined within CSL are morphisms (necessarily total); it is as though you are programming "using the type system only".

I guess this is what elminates its Turing completeness, and ensures termination, since it can't express arbitrary partial functions.

Is that more like it, Frank? ;-)

As a simple example, think of enumerating the elements of any infinite r.e set. This process is recursive, i.e., Turing machine expressible. But it does not terminate.

Someone asked if such languages are at all interesting. Well, you can express a large range of algorithms that are guarnateed to terminate. A simple example is to think of all the things that are expressible as folds (length, sum, reverse etc. etc.) All these are guaranteed to terminate. If we restrict our attention to specific domains (think DSLs), then obviously there are cases where termination is easly guaranteed. Wadler, in this paper, talks about languages without the fix point operator, which exhibit this sort of termination behaviour. It may be worth your time to check what he has to say.

Some here tried to imagine an "almost" Turing complete language. They should check this related LtU thread.

A nice introduction to questions of this sort, well worth reading even if you are familiar with real CS theory, can be found in chapter XIII of Goedel, Escher, Bach by Doug Hofstadter: "Bloop and FlooP and Gloop."

I don't think this at issue. I had interpreted their proviso "up to user input" as being something like the condition in: "This certificate guarantees the bearer immortality within his lifetime". ;-)

Clarification from Frank and closer inspection of some of their literature (for such a bold claim, they didn't bother to put the evidence front and center) showed that, in fact, they are claiming that non-terminating (i.e. partial) functions cannot be expressed, and therefore Charity is not Turing complete.

The question then becomes what constraints do they place on representations so that they can guarantee this, and what "interesting computations" are left. (In the Charity case, it seems to be strong constraints on the construction of data.)

Another interesting question is for specific kinds of non-termination problems (e.g. the list index follower previously mentioned) what ways there are of eliminating non-terminating implementations. In other words, distinguishing (in specific cases) between non-termination that is inherent to the "function" (e.g. find the maximal element of N) and non-termination that is a property of the algorithm (e.g. a graph recursion that was too silly to check for cycles.)

I think this is analgous to strong typing. The typing system can be guaranteed to halt, i.e. find a type for a given expression, without preventing the whole language from being Turing complete. This typing system may eliminate an arbitrarily large proper subset of possible programs (implementations) that would not terminate, but so long as the language allows the expression of arbitrary partial functions on its domain types, I think it will remain Turing complete.

It's not at all a bold claim. Most typed functional languages have core languages based on typed lambda-calculi which are provably terminating. Simply typed lambda-calculus and System F are typical examples. To turn these things into a programming language one usually just adds explicit recursion or letrec, and lots of syntactic sugar.

Charity isn't based on lambda-calculus, but is otherwise analagous. It's based on a core language (categorical combinators) which is probably relatively easy to prove termination for but, instead of adding recursion and sugar, they only added sugar.

In the Charity case, it seems to be strong constraints on the construction of data.

And the operators associated with them. (Algebraic) datatype definitions in Charity are not very different from ones in Haskell, but whereas Charity has a fold construct for each datatype Haskell forces you to define it for yourself using recursion. So Charity short-circuits the step where you get a proof obligation for termination. Of course, you can do non-well-founded recursion in Haskell also, which is what gives the extra power and the possibility of divergence.

what ways there are of eliminating non-terminating implementations

Lazy evaluation is one way of doing this. It's an old maxim that "more programs terminated under call-by-name than call-by-value."

The typing system can be guaranteed to halt, i.e. find a type for a given expression, without preventing the whole language from being Turing complete.

Of course! That is what Haskell's type system does. The price you pay is that there are no set-theoretic models.

Well, your right... once you know what they are actually claiming. ;-)

The glib three lines on their front page give an erroneous impression, and finding out what they really meant required some digging around in their papers. (And I wouldn't have done that if you hadn't set me straight. ;-))

The price you pay is that there are no set-theoretic models

You just reminded me to find the paper on that topic by Reynolds that Wadler mentions in "Theorems for free". (Though I'm not sure when I'll be able to read it; the papers seem to be piling up ;-) )

Bart Jacobs. Objects and classes, coalgebraically. In B. Freitag, Cliff Jones, C. Lengauer, and H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence, pages 83--103. Kluwer, 1996.

Bart Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming (ECOOP96), number 1098 in Lecture Notes in Computer Science, pages 210--231. Springer-Verlag, 1996.

Bart Jacobs. Coalgebraic Reasoning about Classes in Object-Oriented Languages. Electronic Notes in Theoretical Computer Science 11 (1998), pp. 1-12.