Lambda the Ultimate

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.

The PVS Specification and Verification System from SRI is being released as open source.

Also coming with version 4.0 is the PVS wiki.

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?

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?)

A Syntactic Approach to Type Soundness (1992) Andrew K. Wright, Matthias Felleisen.

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features.

This paper does a good job of explaining the foundations of type soundness. It has been previously discussed on the forums. I'm posting it here since I'm just discovering it for the first time, and I think it would be useful for other neophytes.

I am using the "[Redux]" tag to denote front page posts which revisit older papers, tutorials, or overview paper directed at less experienced members of LtU. Feel free to send me any suggestions for the series at cdiggins @ gmail.com.

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