cdiggins.com

I recently found an old interesting discussion on type theory between Tim Sweeney and Frank Atanassow at

http://lambda-the-ultimate.org/classic/message6587.html

I find it provides some useful insights in to type theory appropriate for autodidacts.

The level-0 primitives of Cat can be used to implement a small but non-trivial (read useful) typed concatenative language. From the recently updated Cat specification: 

(sorry about the screwed up apostrophe characters, blame Wordpress)

The Cat equivalent of Joy’s “i” combinator has up to now been “eval”, but unfortunately this made everyone assume it was similar to the Lisp or JavaScript “eval” operator. I am going to have to rename it to “apply”. This makes sense because it is essentially the function application operator. There is a very interesting discussion on the subject at Lambda-the-Ultimate.org.

I was going to announce version 0.13 of Cat which is now live and has a ton of new features (and extensive new documentation, for example http://www.cat-language.com/primitives.html ) but I think I’ll make the change from ”eval” to “apply”, fix some problems with partial-evaluation and optimization and wait to announce the next release which will be the official 1.0 beta release.

Cyclone is a type-safe dialect of C with tons of great features like algebraic types, pattern matching and type inference! Calling it a dialect is a disservice I think, since it is so much better.

There is an easy to read Doctor Dobbs article online about Cyclone at (DDJ no longer requires registration, yay!): http://www.ddj.com/dept/cpp/184401896

What confuses me is why I don’t hear more about people using Cyclone? Perhaps just insufficient marketing? It looks like an extremely significant language.

It is a curious little fact the boolean operations of: “and”, “or”, “not”, “xor”, and “nor” can all be defined using only one operation: “nand”. Nand can be defined in Cat as “and not”.

true true nand == false
true false nand == true
false true nand == true
false false nand == true 

For a fun mental exercise try to define the various boolean operators in terms of only “nand”. For extra points, what other operators can be used to define the whole set of boolean operators (hint: construct a nand with it).

Here is a fun programming puzzle:

Define a while loop in Cat using the following primitives (they might not all be needed):

“if”,”compose”,”swap”,”dup”,”pop”,”eval”, “dip” and “qv”

To solve the same problem but using Joy instead then use the following combinator:

“ifte”,”cat”,”swap”,”dup”,”pop”,”i”,”dip” and “unit”

Hint: the Y combinator is “dup eval”.

MetaCat is a term rewriting macro language for Cat, in other words it is Cat + macros. It can be used to describe the operational semantics of the primitive functions, but its primary role (at least for now) is for expressing optimization strategies.  The MetaCat macros were inspired by Manfred von Thun’s rewriting system for Joy.

The CVS revision #175 now has working new macro functionality (enabled by calling #oz on a quotation), but the graphics and recursive function are temporarily disabled due to other improvements to the code base. It may take another week for the official release of version 0.13.0.

Anyway, here is a sneak peak of how the macros in MetaCat are defined:

// No-op reductions
macro { noop } => { }
macro { id } => { }
macro { swap swap } => { }
macro { dup pop } => { }
macro { not not } => { }
macro { pair unpair } => { }
macro { cons uncons } => { }
macro { qv eval } => { }

// Simple optimizations
macro { dup swap } => { dup }
macro { dup eq } => { pop true }

// Identities
macro { $b $a swap } => { $a $b }
macro { $a pop } => { }
macro { $b [$A] dip } => { $A $b }
macro { true [$B] [$A] if } => { $B }
macro { false [$B] [$A] if } => { $A }
macro { [$A] eval } => { $A }
macro { $a qv } => { [$a] }
macro { [$B] [$A] compose } => { [$B $A] }

// Boolean primitives
macro { true not } => { false }
macro { false not } => { true }
macro { true and } => { }
macro { false and } => { pop false }
macro { true or } => { pop true }
macro { false or } => { }

// Reduction based on the property of commutativity
macro { swap and } => { and }
macro { swap or } => { or }
macro { swap add_int } => { add_int }
macro { swap mul_int } => { add_int }
macro { swap add_byte } => { add_byte }
macro { swap mul_byte } => { add_byte }
macro { swap add_dbl } => { add_dbl }
macro { swap mul_dbl } => { add_dbl }

// Short-circuit boolean evaluation
macro { and $a and } => { and [$a] [false] if }
macro { or $a or } => { or [true] [$a] if }

I am attempting to explain the type inference algorithm I used in the Cat interpreter (TypeInferer.cs). I know it is somewhat cryptic, but hopefully it makes enough sense to those particularly interested type inference to be useful. Remember in Cat ‘A is a stack variable and ‘a is a type variable.

Given a program, represented as a sequence of functions with known types: (’A -> ‘B) (’C -> ‘D) (’E -> ‘F) etc. (always possible because every program can be expressed as a series of primitive functions with well-defined types).

• To compose two functions (’A -> ‘B) and (’C -> ‘D) the result is a new function of type: (’A -> ‘D) (call this the result type)
• You now need to express the variables of ‘D in terms of variables in ‘A. To do so you need to find unifying variables. You also need to replace variable with concrete types when they are known.
  • We start with a basic constraint equation: ‘B = ‘C
  • This generates a set of constraint equations:
  • If ‘B = ‘R ‘x and ‘C = ‘S ‘y then ‘R = ‘S and ‘x and ‘y.
  • If both sides are functions: (’R -> ‘S) and (’T -> ‘U) then we generate new constraints from the equations: ‘R = ‘T and ‘S = ‘U. 
  • If both sides of an equality are variables, generate a unifier associated with both sides.
  • If one side of an equality is a variable, but the other isn’t then we will replace all instance of the variable with the type.
• Recursively replace all variables in the result type with the unifiers
• Compose the result type with the type of the next function, until no more functions are left

Below is a real example of the Cat interpreter for inferring the type of [swap 12 add_int swap] using the #t command.

// swap, 12
Before unification:
('S0 't1 't2 -> 'S3 int)
'S0 't2 't1 = 'S3Constraints:
'S3 = 'S0 't2 't1Unifiers:
'S3 = 'S0 't2 't1
Type: ('S0 't1 't2 -> 'S0 't2 't1 int)// swap 12, add_int
Before unification:
('S4 't5 't6 -> 'S7 int)
'S4 't6 't5 int = 'S7 int int

I’ve just released a version 0.12.1 of Cat which now has a preliminary version of the inference engine. The type inference engine is still experimental but preliminary tests are promising. The type inference command is “#t”. This command pops a flat (i.e. non nested) quotation of exclusively primitives from the stack and will then tell you the type, and show the steps of constraint unification is used to arrive at the result. To see some examples in action look at “tests.cat” or type in “test_types”.

Even though the type inference feature isn’t completely finished, the initial results are superb, with the inference engine being able to handle non-trivial cases like: “eval eval”, “dip dip” or “dup dip”. If I am not mistaken, I don’t believe that even Haskell can handle those kinds of inference cases.

Other changes with the new release include:

• restored the “#exit” command
• added a “#save” command for saving transcripts
• exit session transcripts are automatically saved in the default windows temporary folder using a unique name

A special thanks to Scott Prouty for giving Cat such a great workout and making so many helpful suggestions.

In other news, Gabor Greif is continuing work on his implementation of a statically typed Cat interpreter using Omega.

Kind of random, but I just found the full text of the first computer book I ever had online:

http://www.atariarchives.org/basic/

Not exactly my idea of how to write an effective introductory programming book.