cdiggins.com

Mockingbird is a mnemonic for the M combinator in combinatory logic which is defined as M = SII in the SK calculus and M = \a.aa in the Lambda calculus.

Interestingly I tried to figure out the type for this combinator using the type inference feature of SML 98 and F# and ran into an error. When I posted a query to comp.lang.functional I recieved some very illuminating responses.

In summary the issue resolves around the purposeful limitation of many type inference algorithms to infer recursive types.

For those who insist on recursive types inferred O’Caml is capable of doing it using the -rectypes option. The result yields:

# fun a -> a a;;
- : (’a -> ‘b as ‘a) -> ‘b =

Thanks to Andreas Rossberg and Benedikt Schmidt for their helpful explanations.

For more information see: http://cristal.inria.fr/~fpottier/publis/fpottier-appsem-2005.pdf 

I am still wrestling with establishing the correct types for the classic combinatory logic combinators (i.e. S,K,I,W,B,C,M, etc.). So far I am torn between two approaches to implementing these combinators, one being the method used by Brent Kerby in his paper The Theory of Concatenative Combinators (http://tunes.org/~iepos/joy.html) where

[A] i == A
[B] [A] k == A
[C] [B] [A] s == [[C] B] [C] A
…

And an alternative system where:

A i == A
B A k == A
C [B] [A] s == [C B] C A
…

I have posted the problem on Lambda-the-Ultimate.org ( http://lambda-the-ultimate.org/node/1922 )

Any thoughts or ideas about which system I should choose would be much welcome.

Given a function and a value on the top of the stack, currying will generate a new function which automatically substitutes the value for the first parameter. The curry function in Cat can be defined from the primitive operations as follows:

define curry : (('A 'b)->('C) 'b)->(('A)->('C))
{ quote swap cat }

I am currently hard at work on the formalization of the Cat type system. The current goal is to provide an implementation of the typed SK calculus using a handful of Cat primitives. Progess is slow and steady.

One interesting new development, is a proposed change in how type variables and stack variables are expressed. Previously the type of a function like swap would have been:

dup : (a:any b:any) -> (b a)

Taking a cue from ML, the new notation is:  

dup : (’a ‘b) -> (’b ‘a)

This is significantly less confusing and much more convenient. For interest’s sake here are the types of the SK combinators in Cat:

K : (’a) -> ((’b)->(’a))
S : (a (’a)->(’b) (’a)->((’b)->(’c)) -> (’c)

Note that in Cat, all functions are parameteric on an implied row variable. In other words, these are not completely accurate expressions of the type. I found out the hard way that the actual types are more sophisticated:

K : (r ‘a) -> (r (s ‘b)->(s ‘a))
S : (r ‘a (s ‘a)->(s ‘b) (t ‘a)->(t (u ‘b)->(u ‘c)) -> (r ‘c)

Sandro Magi posted a link to the cat-language mailing list today to the paper: The Logical Approach to Stack Typing (2003) by Amal Ahmed and David Walker. Here is the abstract:

 Abstract: We develop a logic for reasoning about adjacency and separation of memory blocks, as well as aliasing of pointers. We provide a memory model for our logic and present a sound set of natural deduction-style inference rules. We deploy the logic in a simple type system for a stack-based assembly language. The connectives for the logic provide a flexible yet concise mechanism for controlling allocation, deallocation and access to both heap-allocated and stack-allocated data.

This is an interesting paper, and related to Cat in that it provides a type-system for a simple stack-based language.

Andreas Rossberg summed up the Cat type system very elegantly today at Lambda-the-Ultimate.org. As Andreas says its very simple. Here it is in all of it’s glory:

(programs)  p ::= empty | x | i | [p] | p p
(types)     t ::= a | int | (r -> r)
(rows)      r ::= A | r t
(schemes)   s ::= forall a1..anA1..Am.t

--------------------- (EMPTY)
T :- empty : (r)->(r)

T(x) = forall a1..anA1..Am.t
------------------------------------------ (VAR)
T :- x : t[t1/a1]..[tn/an][r1/A1]..[rm/Am]

--------------------- (CONST)
T :- i : (r -> r int)

T :- p : t
--------------------- (QUOTE)
T :- [p] : (r -> r t)

T :- p1 : (r1 -> r2)    T :- p2 : (r2 -> r3)
-------------------------------------------- (COMPOSE)
T :- p1 p2 : (r1 -> r3)

I will in the future go into more detail about what all this means, once I have fully digested it.

Apparently YubNub has been around for a while, but I am only just discovering it now since someone added a command for searching PLRE.org, the programming language research engine. The idea of YubNub is that it allows people to create custom command-line search commands.

To search the PLRE from YubNub you simply need to type in “plre” before your search term, as in “PLRE diggins“ 

There are thousands of other command-line options to choose from. Some example which may interest programming language researchers:

• amazon christopher diggins searches amazon 
• g christopher diggins searches google 
• lucky christopher diggins uses the Google “I’m feeling lucky” feature
• ltu diggins searches Lambda-the-Ultimate.org
• scholar diggins searches Google scholar
• citeseer diggins searches Citeseer
• ls research lists all of the research oriented commands
• oeis 1 2 3 5 7 searches the Online Encyclopedia of Integer Sequences

There is also a toolbar project called RubNub for using YubNub from your Firefox browser.

In response to suggestions from Lambda-the-Ultimate.org members Matt and Mario B. I am pretty much all but decided to go with a new annotation for the Cat type system.

The new proposal is that brackets will only be used to surround function terms, and types will be presented from right to left where the rightmost type represents the top of the stack. So for example the following

eval : ((A:any*) -> (B:any*) A) -> (B)

Will now be written as:

eval : (A (A:any* -> B:any*) -> B)

I have run into some problems though with ambiguitiues in the type system. I won’t get into it in detail for now, but to say that the term [dup] dip eval appears to have an ambiguous typing. This appeared when I tried to construct a derivation tree :

dup : (a:any -> a a)
-------------------
[dup] : ( -> (a:any -> a a))   dip : (A c:any (A:any* -> B:any*) -> B c)
------------------------------------------------------------------------
[dup] dip : (a:any c:any -> a a c)   eval : (D (D:any* -> E:any*) -> E)
-----------------------------------------------------------------------
[dup] dip eval : (a:any (D:any* -> E:any*) -> a a E)

At this point there is ambiguity since D may be one of the following:

D = nil | a | a, a | X, a, a

In other words, D may match nothing, the type a, two instances of type a, or more. Depending on what is matched by D will affect the output type of the function.

To be specific consider if D matches nothing then the production (a a E) is correct, but if D matches (a) then the production should be (a E).

I don’t have a solution, but I have some useful observations. First, if I used the following instead of eval:

eval1 : (a (a:any -> b:any) -> b)

This alleviates the confusion, but I don’t know how to best leverage this.

This leads me to my next observation: perhaps I could simply treat all n-ary functions as unary functions, which are curried, in the style of Haskell and ML. So in other words there is an equivalency between (x y -> z) and (x -> y -> z). This could be useful.

This is where I currently stand, I will have to spend some time thinking about the type rules to find an easy way out of this pickle.

Interestingly this corresponds to behaviour in the compiler which I attributed to bugs in my code. The silver lining is knowing that my code was probably correct, and the problems lie in the type system.  

Well if nothing else this has definitely taught me the value of formalizing the semantics of type systems.

Cat uses the opposite convention to express types than Forth uses for stack effects. I have had a couple comments that the method to express types in Cat is somewhat unintuitive.

For example:

define f : ()->(char int) { 42 ‘q’ }

I was wondering if anyone else has an opinion on the subject? Is there any value in the current method I use, or should I stick to following the Forth convention?

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

I would be most appreciative of any feedback.