Lambda the Ultimate

I am still working on a formal description of the Cat type system.

You might want to check out this thread.

What kinds of programs would fail to receive a type in your system? For example, your (A:any*)->(B:any*) type looks at first glance to match any arbitrary function without side-effects (and possibly even any WITH side-effects; again I can't tell from the description how it might detect that side-effects occur).

If all programs (not just some well-formed subset of programs) can be typed, then your type system is equivalent to an inconsistent logic, which isn't usually considered useful.

I will grant that if the types were explicitly written, this might still serve as a useful hint to programmers who come later of the intent of a given program, but you clearly state that you want inference. So I have to confess, I'm not sure why you want to have a type system at all for Cat.

Not all programs can be typed. Any well-typed Cat program without side-effects will indeed match (A:any*)->(B:any*). Some programs fail to be typed, because they violate the typing rules of primitive operations:

For example the primitive add_int has the following type:

define add_int : (int int)->(int);

So the following program:

define bad { "string" 42 add_int }

Can not be typed.

How about:

define mystery : (A:any*)->();

define strange_adder { 1 2 3 4 mystery add_int }

What will strange_adder's type be?

strange_adder : (int int)->(int)

The mystery function must be a clear_stack. The star parameter when used alone in the consumption of a function (rather than a function parameter) is interpreted as a greedy consumer of stack values.

Even if the type system is unsound, propagation should be able to cut down on typing a lot. The type system still doesn't seem as useful, though.

One thing that might cut through all of this quite quickly is to implement a very small evaluator for a Cat core, in a language like SML. Expressing the core evaluator in a typed lambda calculus should give immediate insights into some of these questions. That would have the added benefit of communicating the core language semantics to many LtU readers quite quickly.

That sounds like a very good idea. It would definitely lend clarity to my reasoning. Thank you!

Great!

BTW, I've previously implemented a toy Joy interpreter, and the eval function was as simple as (in SML):

(* eval : stack -> stack *)
fun eval (Prim f :: s) = eval (f s)
  | eval s = s

Afaict, this implements correct Joy semantics. Everything on the stack is either a primitive function, or a self-evaluating value, including lists (a.k.a. "quotations").

This used a value datatype like this:

datatype value =
  | Prim of (stack -> stack)
  | Var of string
  | List of value list (* a reverse stack *)
  | Int of int
  (* etc *)

withtype stack = value list

If you want to be strict, you could have a separate term type which is the type of the elements in a quotation (list), and a value type which is the type of values on the stack. But the only difference between the two is that quotations don't contain primitives, and the stack doesn't contain variables (at least, I don't think it can observably do so in Joy). Sharing a common value type simplifies things a little.

From a type perspective, there's nothing special about the above: ints would just be ints, not functions. But if you implemented a term/value distinction, I could imagine pretending that all terms are functions which push values onto the stack. You could translate the constant term 42 into the function (fn s => push 42 s), for example, which as you say has type ()->int. But those functions wouldn't normally exist on the main stack, they'd only exist (nominally) in quotations, and as such, their types are really at a different level than those of ordinary functions in the language.

I still don't see what this would achieve, though. My implementation of Joy's "i" operation, which pushes the elements of a quotation onto the stack, looks like this:

fun push_elems (l, s) = foldl push_elem s l

and push_elem (Var v, s) = push_elems (lookup v, s)
  | push_elem     (x, s) = x :: s

IOW, pushing of variables is special, since it pushes their value(s) onto the stack, but all other values are pushed as is. The use of the same representation for quoted values (terms) and actual values is convenient. Introducing some kind of meta-level functions here seems to add complexity for uncertain benefit.

If you want to be strict, you could have a separate term type which is the type of the elements in a quotation (list), and a value type which is the type of values on the stack.

I should rephrase that. If you're developing an interpreter for purposes of clarifying the semantics, you do want to be strict, and it's important to make this term/value distinction at the type level. In the Joy case, it would statically enforce that functions intended to work on the stack vs. on quotations are not confused with each other, for example, and in general it will improve the explanatory power of the interpreter.