Lambda the Ultimate

Operations like "dup" and "swap" in stack-based languages are special in that they return multiple results (unlike most other languages which simulate multiple results by returning tuples).

I find expressing the concept in a type system challenging (if anyone else has done it successfully I would definitely like to hear about it).

One of the core problems is that the type of a function like eval, which is supposed to execute any function:

  eval : (a (a -> b) -> b)

This makes a lot of sense when a function only has one argument and one result. I can reduce every function to an equivalent one having one argument:

  (a b -> c) = (a -> b -> c)

But I do not know how to reduce a function to having one result. This leads to specific problems with certain terms, which I go into more depth on my blog ( http://cdiggins.com/2006/12/09/type-ambiguity-in-cat-and-the-importance-of-formalization/ ).

The only solution I can think of is to creat another eval functions which returns two results:

  eval2 : (a (a -> b c) -> b c)

Any thoughts?

For an error recovery system that supports resume, I was thinking of packing the current continuation in the exception object. However, that raises an issue with freeing the resources: even though the program pointer escaped the context of the error, there is still a way to return there with "resume".

For example:

def foo(x) = 3 + (50 / x)
...
foo 0
catch
   e : DivisionByZero   e.resume 42   #the answer is 42
 | other                throw other

How do you normally deal with continuations that are returned from the current context?

CUFP 2006

The goal of CUFP is to build a community for users of functional programming languages and technology...

abstracts and slides

This may be a naive question from an unlearned youngster, but I'm wondering if there has been research into alternatives to exceptions as a means of detecting and dealing with runtime errors.

The practice of returning error codes is usually discouraged in favor of exceptions for good reasons. Exceptions are sure to be caught somewhere in some way, or else they can cause the program to die with perhaps a moderately useful error message, trigger a debugger in a structured way, etc. Exceptions that aren't being handled can be checked for (using a language with a type system that can do that sort of thing, anyway), and that's often a handy thing to be able to do. Error codes, on the other hand, are very arbitrary, can have overlapping ID numbers, don't carry extra information, etc.

Exceptions, though, seem to carry with them their own baggage and limitations. Sometimes that baggage is nothing more than perceived syntactic "ugliness," but I think there's a little more to it than that. Perhaps I'm just not well versed enough in PL theory (and perhaps real life experience) to really "get" it, but it seems slightly wrong/ugly (to me) that an exception usually takes you out of the normal flow of code and into a kind of mystical land of uncertainty where an error in one situation may lead to being caught in routine X, but the same error in another situation is caught in routine Y - leaving all of the state in between somewhat ambiguous. I realize that many languages have mechanisms for handling those situations (like "finally" blocks to clear up things before you leave the scope for good), but that all feels a bit like the tedium associated with manual memory management rather than the live-and-let-live approach of garbage collection.

For example, say a block of code is writing to an output file and it runs out of disk space. The write() call causes an exception. This exception may not be handled in the routine that was doing the writing on account that the original author may have figured it'd be best for the higher-level logic to decide what to do. Okay - so this exception is thrown and it's a low-level "disk full" kind of error. It ends up getting caught way high up in the logic tree where the programmer originally had called something like: myObject.save(). At that stage in the logic, the programmer should be thinking abstractly about his/her problem and not be so much concerned that the object is being saved to disk, a database, or whatever. But it turns out that now there has to be code there to catch rather specific errors like "disk full." Obviously that write() exception could have been caught earlier and transformed into something more general, but how far are you willing to go? When do you break down and do a catch( * ) { throw Exception('something bad happened') }? On top of all that, where does the application decide on how to proceed? Should it erase the output file on account that it's likely corrupted now and in a half-finished state? Or should it leave it there as-is? What if the application needs to ask the user? How do you pass the answer back down the chain from the UI to the business logic layer that does the actual work? (Note: This may be a badly engineered example, but I think it's a reasonably realistic one that reflects the kinds of problems that crop up in real code that's not been well engineered but can't be thrown away and rewritten from scratch due to time/budget/political pressures.)

Anyway, I'm interested in hearing about other approaches to handling runtime errors that may have popped up over the years and, perhaps, information as to why exceptions are the apparently preferred method of doing things by the mainstream (and even not-so-mainstream) languages. Is it simply because there hasn't been any better alternatives? Or are there much better reasons which I am simply missing the point of. :-)

eskimo: experimenting with skeletons in the shared address model. M. Aldinucci, 2003.

We discuss the lack of expressivity in some skeleton-based parallel programming frameworks. The problem is further exacerbated when approaching irregular problems and dealing with dynamic data structures. Shared memory programming has been argued to have substantial ease of programming advantages for this class of problems. We present the eskimo library which represents an attempt to merge the two programming models by introducing skeletons in a shared memory framework.

Based on some simple extensions to C, the library allows to work on large distributed structures following compositional functional semantics.

The basic idea under eskimo is to abstract both (dynamic) data structures and application flow of control in such a way that they are orthogonalized.

I'm trying to figure out how to type a function and include a set of axioms at the same time.

Here's a concrete example.. Let's say I decide to build a system which uses Natural numbers:

   Nat = Z
       | Succ( Nat )

Now I want to be able to add two Nats together in one of the system's modules so I define a function called Add for this purpose. Its type (pseudo-haskell):

   Add :: a -> a -> a

And a version which implements addition of Naturals (using rewrite rule notation):

   Add( x Z ) = x
   Add( x Succ( y ) ) = Succ( Add( x y ) )

Note that Add does not restrict the type of its arguments to Nat, since I may want to introduce a version which adds Int, or Real down the road. However, when I use Add in the system, I expect it to follow some basic axioms:

    Add( a b ) = Add( b a )
    Add( Add(a b) c ) = Add( a Add(b c) )
    There exists some Z such that: Add( a Z ) = a
    etc..

Basically, I want to include these axioms as part of the TYPE of Add.. If someone writes a version of Add which does not also fulfill the axioms, there should be a type error. I understand that this means a lot of tricky design to avoid bumping into the Halting Problem during type-checking, but I'm just trying to work out the framework first and maybe there's a side-step I can take later on..

My first pass goes something like this:

• For starters, each axiom can be given a name to use as an identifier.
  

     axiomX :: Add( a b ) = Add( b a )
     axiomY :: Add( Add(a b) c ) = Add( a Add(b c) )
  

• The axioms are attached to the function type like arguments to a constructor.
  

      Add :: a -> a -> a
  

  becomes:

      Add[axiomX axiomY axiomZ] :: a -> a -> a
  

• During type-checking, the set of axioms are checked alongside its usual type. Axioms can be matched in any order, like typical sets.
  

    Add[X Y Z] matches any of Add[X Z Y], Add[Y X Z], Add[Z Y X], ...
  

• Here's where things get messy...
  • If all axioms are identical, the types are equivalent.
  • If the required type contains more axioms than the supplied type, there is a type error (insufficient axioms to ensure correctness).
  • If the required type contains fewer (or different) axioms than the supplied type then the type in question MAY be compatible. For instance, it may include an axiom to improve efficiency or restrict the set of values, both of which would be compatible with the existing axioms. So we have to start comparing axioms to check for equivalency of terms (ie: Halting Problem).

Has anyone studied this before? Is there a name for what I'm trying to do?

Thanks!
--Bryan

I've been working on defining a "fold" operation for trees.

There was some helpful discussion in the past "Folding over trees", but I haven't been able to find anything beyond the XML-type examples suggested there.

My problem: I want to have more control of the traversal. That is, when a certain node is reached I want the possibility of skipping further descent, or reentering an already-traversed node.

So yeah, this isn't actually a "fold". Maybe its a "visitor with control"?


Basically I'm trying to cleanly separate
a) details of the traversal process specific to the data structure (how to get a child, etc.)
b) processing of the current node
c) control of the next step in the traversal

Olin Shiver's paper "The Anatomy of a Loop" (previously on LtU) discusses a general framework for separating these kinds of concerns.. But I'm looking for something a bit simpler.. (and am doing this in C++ besides)

So... any suggestions on general FP approaches to this kind of problem? [hopefully this isn't OT!]


I'm currently using something like the foldts used in the prior discussion, modified so that the seed IS the function (or equivalently the function is 'apply'). (is this a monad?)
These seed-closures then return an extra value indicating whether they want to continue
in the regular traversal order: (schemeish syntax here)

(seed 'fup node)   => (next-seed, reenter-children?)
(seed 'fdown node) => (next-seed, skip-children?)
(seed 'fhere leaf) => (next-seed, skip-the-rest-of-the-children?)

I'm seeking languages which implement following features:

1) Types are first class citizens and can be treated as ordinary values
2) Support of partial evaluation for symbolic computation

The idea I try to follow can be best described using a little example. Say you have typed variables x:even, y:odd which are not yet bound by values. One can state explicit type rules for an operation add like this:

add(x:even, y:even) -> even
add(x:odd, y:even) -> odd
...

and write down any kind of permutation of argument types.

But instead one might compute the types using a function:

type(x) = case mod(x,2) of
               1 -> odd
               0 -> even
          else
               `type(x)   --  returns unevaluated expression type(x)

with

mod(x+y,k:int) = mod(mod(x,k)+mod(y,k),k)  -- use pattern matching for decomposition
mod(x*y,k:int) = mod(mod(x,k)*mod(y,k),k)
mod(x:even,2) = 0
mod(x:odd,2)  = 1

Now one can compute z = x*x+y*y+3 and deal with z as a variable of known type and perform type guarded simplifications.

Maybe someone has a pointer where to find reading material ( or even language implementations ) that deal with related ideas?

My latest attempt to describe the Cat kind system with some kind of rigour is at http://www.cat-language.com/paper.html.

Here is an excerpt from the kind system description:

  kind ::==
    | type            the kind of all types
    | stack           the kind of all stacks

  type ::==
    | a               type variable
    | var             variant
    | int             integer
    | bool            bool
    | string          string
    | list            list
    | ∀ ρ . (stack, ρ) -> (stack, ρ)   function

  stack ::==
    | A               stack variable
    | nil             empty stack
    | type, stack     stack with a single type on top
    | stack, stack    stack with a stack on top
    | stack \ stack   stack difference operation

I'd be exceedingly greatful for any comments on the paper.

I recently posted an excerpt from a Ruby book I'm working on (it's a sidebar from a section on the Benchmark library), but I'm not sure if it's solid enough for publication (my math background isn't up to snuff). I'd love to see/hear what LtUers think about it.

Generally the idea is that benchmarking as currently provided by the library is insufficient -- doing one comparison run between options (even a large run) doesn't indicate anything about the statistical significance of the variation between run times of the two (or more) options. So I present a somewhat naive statistical model for doing those comparisons (and in the blog post encourage someone with better Ruby and Math chops to librarify the idea).

You can read the post at: Benchmarking, Lies, and Statistics.