Well, let's check out some fonts: _ is _ with look m. ^ is ^ with look m. That is probably enough. We'll add more as we need them. Here is a system that I think I understand. It is very like "neo-Russell" from a couple of summers ago, and (consequently) very like the system described in Hook's paper, except that it includes variables at least in a limited way. I shall leave out local names from products. At some point that may cause trouble; if it does, I am prepared to go back to it. StkType ~ prod [ rep : type ; new : [ ] _ var rep ; empty : [ ] _ rep ; _ : [ var rep , rep ] _ rep ; ^ : [ var rep ] _ rep ; = : [ rep , rep ] _ bool ; push : [ T , var rep ] _ T ; pop : [ var rep ] _ T ] One can think of this product as a cluster type for (implementations of) T stacks. It would be wonderful if I could write mkProd [ rep ~ TList$rep ; new ~ func [ ] var TList$rep { let v ~ TList$new[ ] in v _ TList$nil[ ] ; v ni } empty ~ func [ ] TList$rep { TList$nil[ ] } _ ~ TList$_ ^ ~ TList$^ = ~ TList$= push ~ func [ v : T , s : var TList$rep ] T { s _ TList$cons[ v , s^ ] ; v } pop ~ func [ s : var TList$rep ] T { let v ~ TList$hd[ s^ ] in s _ TList$tl[ s^ ] ; v ni } ] Of course, I can write this product construction (or something clearly equivalent to it) in Russell but its signature is prod [ rep : type ; new : [ ] _ var TList$rep ; empty : [ ] _ TList$rep ; _ : [ var TList$rep , TList$rep ] _ TList$rep ; ^ : [ var TList$rep ] _ TList$rep ; = : [ TList$rep , TList$rep ] _ bool ; push : [ T , var TList$rep ] _ T ; pop : [ var TList$rep ] _ T ] I would love to bind this to an identifier with the signature StkType above. To do so would require more than just a notion of conformable product types. There is no reasonable way to treat the two product types above as conformable, since in the second case there is nothing requiring rep and TList$rep to be the same -- the identity must be inferred from the right-hand sides of this particular product construction. There are two conclusions to be drawn from this little example. First, we are going to need the equivalence rule in type checking. We will have to accept programs like a polymorphic sort: let Ordered ~ prod [ rep : type ; new : [ ] _ var rep ; _ : [ var rep , rep ] _ rep ; ^ : [ var rep ] _ rep ; = : [ rep , rep ] _ bool ; < : [ rep , rep ] _ bool ] in func [ T : Ordered ; a : array[ T ] ] void { } ni This seems suspiciously like a "macro-expansion" interpretation of declaration/binding. I claim it isn't, really. It just uses provable equivalence of expressions to help deduce semantic type correctness. There is the hack of introducing functions named copy, guaranteed to be identity functions but not provably so, which allow us to recapture "name-equivalence" type checking if we want it. Second (and more "squishy"), we will need top-down, goal-directed type checking algorithms. The signature inferred for the above product construction out of context is not conformable with the signature StkType, but given StkType it is possible to deduce that the construction has that signature. My intuition says this facility is important. I should write more programs. Well, here is a program. I would like to get some intuition about recursive type definitions and about recursive data types. This will attempt to code simple ordered unbalanced binary tree insertion, deletion and lookup. code to sort a ΚΛ˜Ibody˜!IdisplayšΟmœ˜Lšœ˜K˜9K˜ι˜unit˜Icode˜ Nšœ œ ˜Nšœ œ˜Nšœœ˜Nšœœ˜Nšœœ˜Nšœœ˜Nšœœ˜N˜K˜——˜z˜˜N˜˜N˜1—N˜+N˜ N˜ N˜ ˜-N˜—˜$N˜5—N˜———šœ Οeœi˜y˜˜N˜ Nšœ œ˜Nšœ œ ˜Nšœ"œ ˜/Nšœœ ˜#Nšœœ˜&Nšœœ˜"Nšœœ˜N˜———Kšœ€ž œ™˜€K˜?˜|˜˜˜Nšœ ˜ Nšœ œ ˜Nšœœ˜Nšœœ˜Nšœœ˜Nšœœ˜—N˜˜,N™N˜—N˜———Kšœžœ†˜‹K˜χK˜ή—…— D%