Lambda the Ultimate

I have updated the abstraction rule, I forgot the substitutions. The implementation is using union-find to update the variables in place, so its easy to miss out.

Your edit doesn't seem to address my concern. You seem to have a rule ABS which handles the case where the body imposes a single type constraint on x, and ABS' where the body imposes no type constraints on x. What do you do when the body imposes several type constraints on x, as in \f. f (f 2) ? My understanding is that f (f 2) will have constraints {f: Int -> a, f: a -> b} |- b, and this is a case we'd like to handle (by unification).

If there are N occurrences of x in M, then there are N-1 unifications needed to check everything is monomorphic,after which we delete x from M.

Oh, I see. The rule means pick an arbitrary (x : t2) in M1, if several apply. Is there a reason you don't combine ABS and ABS' like this?

M1 |- E1 : t1  
--------------- ABS
M |- \x . E1 : t

where
    SUBS = empty-substitution-list
    a = fresh
    for i = 0 to count(x in M1):
        SUBS = SUBS append (a unify x(i))
    M = SUBS(M1 - x)
    t = SUBS(a -> t1)

And not that it matters, but doesn't this have an off-by-one error looping from 0 to count?

No, that looks good to me. I have updated the original. I kept the 'x' above the line for consistency with the other rules (and I think it has to come from somewhere).

Just realised we need to apply the substitutions so far to 'a' and 'x(I)' otherwise unifying the fresh variable 'a' each time does nothing (it will unify with anything). I missed this as I am using union-find to implement the substitutions in my code, which automatically applies the substitutions so far on variable dereference.

I just wanted to get something up quickly for discussion and review. When I have more time I will have a go at MathJax. Its certainly easier to find the ASCII characters on the keyboard. Its WYSIWYG and fast. I experented with using Unicode in my language for type reporting, but decided it should output types exactly as you would type them, and typing Unicode was much slower and harder than just using -> as arrow for example.

In the first rule

N
------------- LIT
{} |- N : Int

There is an antecedent

N

. Is your type proof supposed to stop there? Wouldn't just

------------- LIT
{} |- N : Int

Be better?

I read that as: given a literal N we derive the typing {} |- N : Int, but in my derivation trace from the type inference I don't have anything. I guess I was trying to be consistent with the VAR case where you have x above the line.

Would it be better to change both VAR and LIT to have nothing above the line?

You're expressing the inference rules with respect to a sequent logic. I just don't know what happens when you arrive at the literal though I guess one could reconstruct the original term from it. But if there is no reason I wouldn't do it.

I think it sounds reasonable, so I will update.

Well then you have to take it off ABS, too. :)

I assume you mean remove the 'x' from above the line. I agree it needs to be consistent. Less characters is better as long as the meaning is clear.

My understanding is that id would be defined as \x . x and put in the polymorphic environment. He has a polymorphic variable introduction rule which from what I remember generalises the type from the polymorphic environment. So it did not seem compositional for let bindings, but I might be misunderstanding something. I don't see the use of multi-sets (intersection types in the context) in his work. In my opinion to be fully compositional requires you not to have any environments either poly- or mono-morphic, only constructive contexts.

System C doesn't seem to really have principal typings, according to Wells' definition - the polymorphic environment is threaded top-down, not constructed bottom up. Your system is very simple and, if it's not flawed in some way, nice.

Well. I have not posted because I don't get yet what you're aiming for. You've shown you can 'type' two derivations for specific terms, one is "x x" and the other was something like "\x \y -> z x + z y". You've shown that they are typeable by not unifying one step further than most typing schemes do. You haven't given a correctness or soundness proof.

Assuming the typing scheme is correct I just don't have any clue what it buys you? What problem did you solve? (As it stands it just seems to, loosely speaking, omit a unification step. Okay...?)

(And then there is the point that most abstract academic typing schemes often are far simpler than what is actually used in a programming language. What is your aim?)

Namely, HM doesn't have principal typings. This means HM type inference isn't compositional, it's harder to produce good error messages, etc. See well known papers like Jim's What are principal typings and what are they good for? and Wells' The essence of principal typings. That you can do this by "skipping a unification step" makes it more interesting, not less.

Things that it would be nice to see done carefully:

- Generalize the declarative rule system for HM to multi-set contexts.

- Show that this generalization is still sound.

- Show how the inference procedure for "rank 0 intersection types" corresponds to valid deductions under this generalized HM.

- Show that the produced typings are principal.

I'm still waiting to hear where the flaw is that would prevent one of those steps from going through. None of them looks particularly hard to me, but maybe I'm missing something.

I am sorry. I just don't see it. I somewhat get the difference between a principal type and a principal typing, and in some sense the unfinished type checker for my language relies on that. (I don't care about types for terms as long as the body of a definition typechecks. I can do that since the code doesn't rely on the types of the terms, in sharp contrast to other languages.) But I need to see where omitting this unification step would help me.

In the example "x x" has a principal typing where x is bound to two separate types. In some sense, it tells you: "We can type everything as long as we don't type fully."

It needs to give you something back and I don't see what it gives you back apart from that you'll just accept all terms as well-typed.

(I mean. I like the joke but I don't see much more than a joke?)

I find the notation quite confusing but if I understand his system correctly, then yes it may have principal typings for some sense of 'principal typings', but I'm not sure that this is the same as what the literature calls 'principal typings'. In "What are principal typings and what are they good for?" Trevor Jim writes that the advantages of principal typings are error messages (errors don't contain irrelevant information) and separate compilation (signatures of modules can be inferred). I don't think this system has those advantages. As far as I understand it, it would happily produce a context where x : int and x : string, and it will only later produce an error when the variable is bound in either a let or a lambda. So while this may be a nice way to formulate HM, I don't think it's all that different. I may have completely misunderstood what's happening though.

Informally, I think they mean this. (Hope I got it right.)

• A language has the principal type property iff for all typeable (sub-)terms the most general type can be derived.
• A language has the principal typing property iff a typing derivation exists for all typeable terms. Such that a principal type exists for all (sub-)terms somewhere.

People thought having the principal type property would be helpful. I somewhat, in cases fully, disagree with that. I mostly consider it an old-fashioned idea.

People thought having the principal typing property would be helpful. Yeah, a principal typing needs to exist somewhere for any term, I guess. But maybe that's just a superfluous observation on any typing scheme which works; like a soundness guarantee. Do you really expect people to write type schemes which specialize a type in a random direction?

And maybe Keaan has shown that it isn't even a soundness guarantee. I still don't see where his scheme is useful.

it would happily produce a context where x : int and x : string

That's a good point. So that's a good follow-up question -- when you get to a module boundary or when you're trying to assign blame for an error, is the question of whether a set of constraints has a solution decidable? I'm guessing it's not, though you could certainly report egregious incompatibilities like x:int and x:string.

HM is decidable because for each variable either:

1. The type is known, usage is polymorphic (in a let).
2. The type is unknown, usage is monomorphic (in a lambda).

So I doubt that checking whether the constraint set has a solution is decidable, because it essentially amounts to the case where the type of the variable is unknown, but usage can be polymorphic.

You can type more if you just force people to type all declarations correctly. That's good practice anyway. (Can HM typecheck any definition where the derived type is bisimilar to it's own definition? Though there are extensions with nu experssions, I guess...)

And I have never seen a real-world example where the let-rule makes that much sense that you would even want to include it; if I ever get interested again, I'll throw it out of my language. ("id"? Seriously? Nobody writes function local definitions over multiple types.)

# let rec f = fun x -> (1, f);;
Error: This expression has type 'a -> int * 'b
       but an expression was expected of type 'b
       The type variable 'b occurs inside 'a -> int * 'b

I wanted that f has type

type t = unit -> int * t

That's a seriously good type you'll desperately want to be able to express in a strict language to implement a form of laziness. It defines a lazy infinite list of ones you get by 'pushing the button' on a function.

(Haskell/ghci, for good measure, omitting unit since it is lazy:

let f = (1,f)
<interactive>:2:12:
    Occurs check: cannot construct the infinite type: t1 = (t0, t1)
    In the expression: f
    In the expression: (1, f)
    In an equation for `f': f = (1, f)

)

#include <stdio.h>
#include <stdlib.h>

typedef struct T {
    int fst;
    T*  (*snd)();
} T;

T* f (void) {
    T* t = (T*) malloc(sizeof(T));
    t->fst = 1;
    t->snd = f;
    return t;
}

int main(int argc, char *argv[]) {
    T* p = f();
    T* q = p->snd();

    printf("%d, %d, ...\n", p->fst, q->fst);

    free(q); free(p);

    return 0;
}

See? ML and Haskell don't even have their basics covered. Sheer incompetence.

Anyway, I'm sure you're aware that C doesn't win...

data T = T Int (() -> T)

f () = T 1 f

main = let T one g = f () in print one

I am aware of the wrapping trick. You can trick both ML as Haskell into giving a bisimulation proof. Ocaml has -rectypes too.

But I am annoyed they don't have that feature central. It's standard practice and hints that HM just look at types wrong; though you could omit it for speed. Putting it differently, HM ain't that great without well-typed definitions. Wasn't it able to derive principal types right? It types too much and you don't know what you payed for.

It's more luck that both typing schemes get it right than anything else. An unintended feature.

(Anyway, laziness. This is better:

Prelude> data T = T Int T deriving Show
Prelude> let f = T 1 f
Prelude> f

Why "f = T 1 f" but not "f = (1, f)"?)

There is a reason why -rectypes isn't the default: it allows to type many programs that turn out to be mistakes (eg. writing "let f x = x x" instead of "let f x = x+x"), and programmers find this has bad usability. With your T definition, you gave a recursive type definition yourself, so the intent is clear.

Yeah. That's what I meant that HM types too much sometimes. But disallowing them has a lot to do with ML's proposition that since you have a typing system with principal types it's therefore good not to type function declarations explicitly. HM principal types is nice, it gives you a slight guarantee you will be able to type complex bodies, but has no role except for the REPL.

Anyway. It isn't even clear (well, not to me) why HM sometimes manages to give bisimulation proofs (there are various manners of guaranteeing that,) or does it, and it isn't clear what HM drops in terms of expressiveness (to me, again.)

I didn't check "f x = x x". I just assume that problems like that will be caught if f has a type.

That actually gives back an interesting type in ocaml with -rectypes.

# let f x = x x ;;
val f : ('a -> 'b as 'a) -> 'b = <fun>

Not what one would expect.

I allowed recursive types at first, but I am considering disallowing them. In any case that discussion has nothing to do with the type system. We can choose to allow recursive types independently of the system, and my type inference code by using regular tree unification with a post loop check can allow, disallow, or warn about them.

What in God's name did you make think that?

At least in this case. Recursive types or not the rules above are the same. So its trivial to enable them or disable them, providing you use regular tree unification (like prolog-II). So I can have a compile time flag to enable them. Whether they should be enabled by default is a discussion relevant to my particular language and implementation, and not to the type system rules here.

To be clear, it is a discussion I am interested in, but I want to focus on the type system rules here. I am interested in comparing to HM and intersection type system like System-I and system-e.

I tried to hack this in Scala for fun.

type T = Int => (Int, T)
error: illegal cyclic reference involving type T
       type T = Int => (Int, T)
                             ^

Okay. But can do

def f (n: Int):Any = (n, f _)
f: (n: Int)Any
f(1)
res0: Any = (1,)

But then

f(1)._2(1)
error: value _2 is not a member of Any
       f(1)._2(1)

Hmmm. I wanted to cast it but couldn't figure out how.

So I tried it the C manner:

class T { var fst:Int = 1 ; var snd:Int => T = (n:Int) => new T }
defined class T
var f = new T
f.snd(1).snd(1).fst
1

Ah. Did it.

"Write elegant code that works the first time it is run," they told me. Puh.

A code module provides a bunch of polymorphic function definitions, and requires a bunch of monomorphic types in a multi-sets. Requirements in the context may be multiple for one variable (its a multi-sets).

I can see that I am going to need a polymorphic environment for the definitions provided by a code fragment but that would be restricted to a rule for importing modules or somehow joining two code fragments.

Its perfectly valid for a module to require a definition of x : string and x : int, but no other module may be able to provide a definition of x that is compliant.

If a module required f : string -> string and f : int -> int it is easier to see that a module providing f : a -> a would satisfy that requirement.

So read the context as a set of requirements which we are deferring deciding if they are satisfiable or not until we have seen the possible definitions.

We could for example have a module providing overloaded definitions of x one int and one string. I don't see a problem with that.

Don't forget intersection type systems like system-i and system-e are accepted to have principal typings and do exactly this: x :: String ^ Int.

I think it makes no sense to talk about principality here. Because principality only is an interesting property for non-deterministic type systems -- in a deterministic system all (correct) derivations are trivially principal.

That doesn't mean that you can't find an equivalent declarative formulation of your system that would have principal typings in a non-trivial manner (and for which your current algorithm would compute those). But you have to define it (which shouldn't be particularly hard).

Another problem I see is that your claim of compositionality is at least questionable. Because in this system you cannot classify a variable in the environment without knowing how often it will be used. How would you define an initial language environment independent of a concrete program? Or somewhat equivalently, the interface of a module? As far as I can see, you wouldn't be able to describe either with the type language you have. That's not modular.

It seems like the only way to fix this issue would be reintroducing HM-style prenex-universals -- essentially, they express an infinite "rank 0" intersection, which is exactly what is needed to avoid the problem.

Your point on the principality of deterministic type systems is true, but I think the implicit non-deterministic type system is just HM with a tweak to support multi-set contexts. It looks like any model of HM will also model this modified system, so I don't see much work to do.

I'm possibly misreading your second point, but I wouldn't think that that you ever need to introduce explicit quantifiers. Isn't it good enough for all quantifiers to be implicitly over the entire context? Instead of writing {f: forall a. a -> b}, isn't it enough to have a context { f: a -> b, x: b }? The quantification over a is implied by dint of its absence in the rest of the context. Is that not good enough? HM doesn't come with constructs for declaration and external definition, either, out of the box. I don't see it being that hard.

I think the implicit non-deterministic type system is just HM with a tweak to support multi-set contexts.

Yes, I assume it's not hard, but a little more then a tweak (the system splits multi-environments in a way more reminiscent of linear type systems, and there is no weakening; term-level substitution and associated meta theory would become more involved; potentially complicating operational semantics as well; etc).

It looks like any model of HM will also model this modified system

If by model you mean semantic model, then I don't think this is true. For HM you can construct a parametric model, I don't see how that would be possible here -- it's just intersection of monomorphic types.

Instead of writing {f: forall a. a -> b}, isn't it enough to have a context { f: a -> b, x: b }?

No, because there is no polymorphic instantiation in the system. All "instantiation" happens beforehand at definition site in the let-rule -- and that needs to know the number of use-sites to multiply the binding accordingly. For an initial environment or at module boundaries you neither have a let, nor do you know how often something is going to be used.

That is, the system cannot cope with separating use site from definition site -- polymorphic intro and elim is tied to the let-rule, and that needs to see both sides. Hence, the system effectively requires whole-program checking, i.e., it is not modular.

We can easily add first class polymorphism. If you have a type annotation in a lambda abstraction, you can generalise that similarly to the let rule.

$$
\newcommand{\app}[0]{\hspace{2pt}}
\newcommand{\rule}[2]{\frac{\array{#1}}{#2}}
$$

Yes, I assume it's not hard, but a little more then a tweak (the system splits multi-environments in a way more reminiscent of linear type systems, and there is no weakening; term-level substitution and associated meta theory would become more involved; potentially complicating operational semantics as well; etc).

The declarative rules I had in mind were very much a small tweak to HM. Let me write it out, and maybe you can explain why it's busted. Copying the presentation at Wikipedia, let me go through how the rules would change. The Var rule is the same, but the context is allowed to be a multi-set:
$$
\rule{x: \sigma \in \Gamma}{\Gamma \vdash x : \sigma}
$$

The App rule is the same, but the context is allowed to be a multi-set:
$$
\rule{\Gamma \vdash e_0:\tau \to \tau' \qquad \Gamma \vdash e_1:\tau}
{\Gamma \vdash e_0 \app e_1 : \tau'}
$$

The Abs rule is the same, but the context is allowed to be a mult-set:
$$
\rule{\Gamma, x:\tau \vdash e:\tau}
{\Gamma \vdash \lambda x. e:\tau \to \tau'}
$$

The Let rule is where the biggest change is needed. The context is a multi-set and we're allowed to work with intersections:

$$
\rule{\Gamma \vdash e_0:\sigma_1 \qquad ... \qquad \Gamma \vdash e_0:\sigma_n \qquad \Gamma, x:\sigma_1 ... x:\sigma_n \vdash e_1:\tau}
{\Gamma \vdash \text{let } x=e_0 \text{ in } e_1:\tau}
$$

The Inst rule is the same, but the context is allowed to be a multi-set:

$$
\rule{\Gamma \vdash e:\sigma' \qquad \sigma' \sqsubseteq \sigma}
{\Gamma \vdash e:\sigma}
$$

The Gen rule is the same, but the context is allowed to be a multi-set:

$$
\rule{\Gamma \vdash e:\sigma \qquad \alpha \not\in \text{free}(\Gamma)}
{\Gamma \vdash e:\forall \alpha. \sigma}
$$

I don't see any reason why a semantic model for HM wouldn't work for the above "multi-HM", as well. I was also thinking it would be straightforward to show that an inference in his system would correspond to some valid deduction in this (multi-HM) system. And I would expect that the resulting typings would be principal.

EDIT: Maybe the issue is that this doesn't count as a principal typing. Like if you start from this typing:

$$
\lambda x. f \app x : \{ f : a \to b \} \vdash a \to b \\
$$

It implies the following typing:

$$
\lambda x. f \app x: \{ f : \forall c. c \to c \} \vdash d \to d \\
$$

But you have to instantiate c to d before substituting, to get there. So does it count as a principal typing?

I agree it seems kind of backwards to pull back 'id: Int -> Int, id: String -> String, id: (a, b) -> (a, b), etc.' from everywhere to the definition of 'id' rather than giving 'id' a polymoprhic type 'forall a. a -> a' and checking that it's used correctly throughout the program. I don't see any reason that a hybrid approach wouldn't work, pushing polymorphic bindings forward into let-bodies instead, but I'm less enthusiastic about this type system than I was yesterday. It still might be a useful way to look at things.

So I should describe the type system as above, and present the original definition as an algorithm for deriving principal typings compositionally in this type system?

There are implicit quantifiers where you place them.

I think the property of compositional principal typings is useful, but that probably requires further work to show.

Question: Why does the let rule change at all? Collecting the uses of 'x' in the body and then generalising the RHS and unifying with each use in the body is the same as putting the RHS in the polymorphic environment and using the polymorphic-var rule. The environment when viewed top-down is polymorphic and does not have multiple entries for a multi-set.

So is this not a new type system, but an algorithm for producing principal typings for HM? Where these types differ from HM, there are no possible HM types (for example you cannot type the body of a let in HM, without knowing the polymorphic RHS type.

So is this not a superset of HM producing exactly the same types where one exists in HM, but defining types (typings) for the code fragments that are untypeable in HM, and thus providing principal typings for HM? The model would be normal HM with a top down polymorphic environment, and top down monomorphic environment both normal sets not multi sets.

Edit: there is a kind of polarity going on here, a top-down polymorphic environment and a bottom up multi-set context are kind of duals of each other. The required definitions of a code fragment can be propagated upwards using a multi set monomorphic context, and polymorphic definitions can be propagated downwards. There are two extremes, the HM algorithm W way where the poly environment is propagated down from the definition all the way to the use site via the poly-var rule, and my original presentation where the uses are propagated all the way up to the definition site. It seems possible to pick any node in the tree between definition and use, and bisect the two allowing type checking and error reporting to be done from the "viewpoint" of any node between definition and use.

Question: Why does the let rule change at all?

I don't see how you would type the following without generalizing the let rule:

let f = \x. g x in (f 1, f "bob")

We want to end up justifying this typing:

{ g: Int -> a, g: String -> b } |- (a, b)

I'll think harder about it later.

If a declarative rule is supposed to show no preference for direction, then is there a problem with the definition of HM? The polymorphic environment is implicitly top down. The hypothesis is that the bottom-up monomorphic multi-set context is the dual of the top-down polymorphic set environment. To not imply a direction of information flow the rules should use neither. But what should they use? Is the direction of information flow so fundamental that the attempt to write declarative rules is a fundamentally flawed idea?

To save the declarative definition do we need to have a single thing that viewed top-down is a set of polymorphic definitions and viewed bottom up is a multi-set of monomorphic requirements?

Would it be enough to reformulate HM with both a polymorphic-set environment, and a monomorphic multi-set context for each rule, and then add rules for moving a type-variable fron one to the other?

In your Let rule $$
\rule{\Gamma \vdash e_0:\sigma_1 \qquad ... \qquad \Gamma \vdash e_0:\sigma_n \qquad \Gamma, x:\sigma_1 ... x:\sigma_n \vdash e_1:\tau}
{\Gamma \vdash \text{let } x=e_0 \text{ in } e_1:\tau}
$$ you have several variable on the right that share a polymorphic
type scheme. My understanding of the discussed system is that
duplicated variables (or the intersection types) only carry
monomorphic types.

So that would rather be split in two rules $$
\rule{\Gamma \vdash e_0:\sigma \qquad \Gamma, x:\sigma \vdash e_1:\tau}
{\Gamma \vdash \text{let } x=e_0 \text{ in } e_1:\tau}
$$

$$
\rule{\Gamma \vdash \sigma \sqsubseteq \tau_1, \dots, \tau_n
\qquad \Gamma, x:\tau_1, \dots, x:\tau_n \vdash e:\tau'}
{\Gamma, x:\sigma \vdash e:\tau'}
$$

Is this a valid derivation with HM + modified let and new rule?

1: x : a |- x : a                               [Var]    (x : a in {x : a})
2 |- \x.x : a -> a                              [Abs]    (1)
3 |- \x.x : forall a . a -> a                   [Gen]    (2), (a not in free {})
4: id : a |- id : a                             [Var]    (id : a in {id : a})
5 |- let id = \x.x in id : a                    [Let']   (3), (4)
6 |- let id = \x.x in id : forall a . a -> a    [New]    (5)

I almost commented about this, but I think the let rule could just be:

$$
\rule{\Gamma \vdash e_0:\tau_1 \qquad ... \qquad \Gamma \vdash e_0:\tau_n \qquad \Gamma, x:\tau_1 ... x:\tau_n \vdash e_1:\tau}
{\Gamma \vdash \text{let } x=e_0 \text{ in } e_1:\tau}
$$

The reason being that you're only going to instantiate a polymorphic type at finitely many places, and so you could always just expand each polymorphic type into the monomorphic types at which it's used. I left the stronger version just to make it obvious that it's a generalization of HM.

Ultimately, this is equivalent to the following rule for typing let, that does not require multi-contexts:

$$
\rule{\Gamma \vdash e_1 : \tau_1 \qquad \Gamma \vdash e_2[e_1/x] : \tau}{\Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : \tau}
$$

I have seen this formulation of let-polymorphism in literature, but don't recall where. Of course, the problem with this is that the typing rules are no longer inductive on the syntax, which can render some bits of meta theory hairy.

(Note that you need the extra premise on \(e_1\) to ensure that it is well-typed even if \(x\) is unused. You'd probably need something similar in your rule.)

Require n ≥ 1 in my rule.

If we assume that the environment is loaded by an outer 'let' then this algorithm produces exactly the same types as HM (ignoring the context part of the typing).

The issue is this algorithm can type some terms that HM cannot, although that is limited to terms like 'x x' where there is not a polymorphic definition for 'x' in the environment.

As the HM rules are declarative, and don't specify the order in which operations happen, the is no need to change the rules for the types which exist in HM.

For types that don't exist it is sufficient to simply allow multiple types for a variable in the environment.

I am not sure which algorithm you are referring to now. Can you clarify?

If you are talking about a HM-like system but with a let-rule like above instead of polymorphic types, then I don't believe it can type anything that plain HM can't. In particular, "x x" can only type-check if x is let-bound with an appropriate definition.

By this algorithm I was referring to the one posted at the top, optionally with the Def and Link rules replacing Let.

Is HM+multiset environment+modified let rule, sufficient to describe this algorithm declaratively?

Is HM+multiset environment+modified let rule, sufficient to describe this algorithm declaratively?

I don't think this is the correct way to put it - the declarative type system doesn't describe your algorithm at all. I think the hope is to be able to say things like this:

- Multi-HM rules are an extension of HM (every HM deduction remains valid).

- In a given environment, a principal types remain principal in multi-HM.

- The rank-0 algorithm is consistent with respect to multi-HM (that is, everything the rank-0 algorithm deduces can also be deduced in multi-HM).

- The multi-HM system admits principal typings for every term, and the rank-0 intersection algorithm computes those principal typings.

Andreas made a point about completeness in another subthread, but I don't know that the situation is too much different than the situation with algorithm W, which infers a type like (\x. x : a -> a) but not (\x. x : forall a. a -> a), because it only generalizes at let-bindings. It seems to me that if you prove principality, then you've proven practical completeness.

I thought he already has shown that he can 'type' "x x"? Which prompted me to believe he'll be able to type anything.

I still want to know what this system will accept and reject. (A type system for an FP language, somewhere, is just something where you decide between what you'll accept and reject, where HM, whatever that is, is a relatively fast solution. And that still isn't clear here.)

For complete programs (that is ones with definitions for all variables) it will type exactly the same set of programs as HM (with or without recursive types as required).

All this does is type more incomplete program fragments and give them (I would argue) principal typings. The advantage to typing more program fragments is composability of typings, the ability to give better error messages.

There are really two separate changes here, one to give typings instead of types (which is to allow modules to be first-class) and have the contexts of those typings to be multi-sets (which makes them principal and compositional).

- (Well, that didn't make sense)

HM for example cannot type "x x" but it can type "let x = \y.y in x x". So my point is both will give exactly the same type for the (any) complete program. So all we can do is give a typing to "x x" we cannot run that as a program without the definition of "x" and we cannot give "x" a definition that would be not allowed in HM.

This is all about composability and principality, not about typing more programs. This will type precisely the same set of complete programs as HM.

But implementations of HM also need to carefully disambiguate between monomorphic variables which may, or may not, become bound in a polytype. How does your system do that? (Ah well, guess it's somewhere in the context rules. No idea.)

The multi-set context allows it to defer the decision of whether a variable is mono-type or poly-type until that variable is defined. As it is compositional it processes the AST from the bottom up, and deferring the decision until the variable is either abstracted (mono) or let bound (poly).

In reality this would probably be a module boundary (where an explicit type would be given in the interface/record) rather than the original definition.

The coin dropped. I don't really see it all in your proposed scheme but maybe you should elaborate the rules somewhat more.

HM for example cannot type "x x"

As stated, that's incorrect. Of course HM can type "x x" under an appropriate context.

but it can type "let x = \y.y in x x".

...and that contains a subderivation for typing "x x".

Since it does something bottom up with intersection types up I don't understand yet. How would it type:

g = \f. \x. \y. (f x, f y)

[g : {} |- (a -> b) -> a -> a -> (b, b)]

Where square brackets represent a polymorphic environment introduced for definitions. Note: the polymorphic environment is exporting definitions from fragments.

Didn't you have a tool? Ah well. I think I somewhere get it and it isn't what I wanted for my language. Then again, there's no good solution to that typing. (I know what I want but it becomes too complex too easily.)

Here's a better example than the one I gave earlier:

let x = y in (x x)

The way vanilla HM would type such a term is that it would know the polymoprhic type of y going in. It would then transfer that polytype to x (in a round about way), and type the body of the let. But as we know, (x x) doesn't have a principal typing in HM. Thus, there is no single polytype that would be a suitable choice for x to produce a principal typing for this let expression. That means that if you want a derivation of the principal typing { y:a, y:a -> b} |- b, then you can't use the vanilla HM Let rule.

double post

That looks like a fine system, but it is richer. I doubt that Keean's algorithm would be complete for it. Specifically, your let rule inserts polymorphic types into the environment (and you have separate gen & inst rules), whereas in Keean's system, there are only monomorphic types.

(Also, in both the let and the abstraction rule you would seem to need to remove x from the original Gamma in the premise, otherwise you'd overload the inner binding with potential outer ones. Or have a side condition enforcing alpha-renaming.)

So a parametric HM-style model would probably be adaptable to this (it's still not the same, because the presence of multi-environments changes the model). But that doesn't imply anything about Keean's system.

I don't fully understand what you are getting at in your edit. Are you observing that you cannot easily map between the monomorphic and polymorphic environments of both systems?

I agree that a hybrid approach would probably work, but is it appealing? It seems like you would merely end up relaxing (and thereby complicating) the HM type system to multi-contexts / intersection types, just for the sake of being able to technically claim "principal typings" of an inference algorithm. There doesn't seem to be any added value for the type system as such (i.e., it doesn't type any more programs). In that situation, I'd rather accept that the inference algorithm does not derive typings, but, say, "proto typings" (being multi-maps) or whatever you want to name them, which can be related to actual typings (proper maps) in a fairly obvious manner.

I doubt that Keean's algorithm would be complete for it.

Well, you can automatically generalize any type that's not in the context. Is it complete? I don't know.

(Also, in both the let and the abstraction rule you would seem to need to remove x from the original Gamma in the premise, otherwise you'd overload the inner binding with potential outer ones. Or have a side condition enforcing alpha-renaming.)

I noticed that but assumed that the comma operator shadowed the old bindings. Doesn't the Wikipedia version (vanilla HM) have that same issue?

I agree that a hybrid approach would probably work, but is it appealing?

Yeah, I don't know. I was thinking that when reporting errors, you could try reporting the error "both ways" and maybe that would produce some insight for the programmer.

Well, you can automatically generalize any type that's not in the context.

Hm, not sure what you mean.

I noticed that but assumed that the comma operator shadowed the old bindings. Doesn't the Wikipedia version (vanilla HM) have that same issue?

Well, HM is not using multi-sets, so doesn't have to distinguish between shadowing and overloading. For multi-sets, you need a non-shadowing comma. (Just a notational nitpick.)

maybe that would produce some insight for the programmer.

Perhaps, but that seems to be an implementation concern. It shouldn't require messing with the definition of the type system itself.

I just meant that you can automatically apply the generalize rule when it applies.

Perhaps, but that seems to be an implementation concern. It shouldn't require messing with the definition of the type system itself.

Well, the body of a let isn't well-typed on its own in HM. So if the problem is with the polymorphic definition, then you can't really use the HM rules to infer a type for the body. The idea would be to use the inferred type of the body to help you pick a polymorphic definition (dual to what we usually do).

You have to pick a polymorphic definition that generalises the RHS, and which then can be instantiated to each use in the body. Presumably the rules could be kept separate allowing you to pick the polymorphic type from the RHS or body? The Gen rule seems the same as standard. The Inst rule could be changed to allow instantiation over a set of types.

I think it would be good to add a polymorphic context, as I described further down, allowing Let to be split into Def and Link. This will allow any code fragment to generate both a monomorphic multi-set of requirements, and a polymorphic set/multi-set of definitions. I posted some proposed rules for Def and Link.

Intersection type systems claim principal typings, so I still don't see the problem.

Maybe a Polar type system is a good starting point, allowing the lets to be split into definitions (def module A {x = ...; z = ...}), and uses (def module B {y}) that can be linked (use module A in module B renaming {}). One which allows quantifiers downward and intersection types upward, and then restrict it to rank-1 intersection types in the context?

Its modular in that any two code fragments can be typed independently. In code fragment A you have a polymorphic function definition, say in a modular library you import. In code fragment B you use functions from the library

Each can have type inference independently, which is what compositional typing is about. If you have an environment providing top down typing information its no longer compositional. You simply apply the let rule for every top level polymorphic function defined in A to B as the body.

You simply apply the let rule for every top level polymorphic function defined in A to B as the body.

Which is exactly the problem I'm alluding to: this means you need both A and B, so there is no separate type checking of them as "modules". (See also my reply to Matt.)

On the technical side, "linking" is not just substitution in this system. You need to insert a let and its additional typing step to make it work.

On the practical side, the user would have to write down typings, not types to specify module boundaries. Not only does that leak implementation details, it also is highly brittle wrt changes (esp since the system does not even have weakening).

Edit: thinking about it a bit more, linking could still be defined as substitution, but it would require a non-standard substitution lemma that essentially mirrors what the let-rule is doing. That lemma, and the definition of well-formed substitution itself, would be somewhat involved, because they have to deal with typings, multiplicity, lack of weakening, etc.

I think I need to split the let rule in half to make this work nicely. So the definition half of the let populates a polymorphic environment (the lack of this is just that I haven't needed it yet rather than philosophical). The body part of the let would work as before with a multi-sets monomorphic context. Then the two would be tied together in linking by applying the let rule to each variable in the body requirements.

The monomorphic requirements multi-set would be for the whole module, not for each function (you can merge them together). If this were given as an explicit polymorphic definition then the let rule can be finalised inside the module.

It seems the purpose of header files has been forgotten. Most linking systems need the type of the imports at compile time (to create the environment). This system can compile the body truly in isolation by producing a requirements list. The idea is this would all happen by type inference.

Where you explicitly want a module interface you would specify the polymorphic types of the functions in a module interface definition and import that into both the implementation and the code that wants to use it.

Just because the formulation makes its principality obvious, does not make it not principal. You may not find it interesting, but I consider obviousness an admission that it is principal. I consider nondeterminism in a type system a problem.

As for compositionality, the environment is not compositional by definition. It is a global top level table. How is a global table compositional, you have to type the whole program to populate the environmentm. The environment is the problem.

Just because the formulation makes its principality obvious, does not make it not principal.

Sure, but you could take any random screwed-up typing algorithm, declare it the "definition" of a type system, and claim principality. So it is not a useful property by itself, and says nothing about the quality of that system.

I consider nondeterminism in a type system a problem.

Why? Non-deterministic formulations are typically far simpler, more declarative, and have much simpler meta-theory, which is why they usually are the standard approach. See HM vs W for an example. Non-deterministic formulations are only a problem if they don't allow an effective algorithm (and this is where principality becomes relevant).

Basically, it's about separation of concerns. You don't want to do soundness proofs relative to an algorithm. It's much easier with a more declarative formulation.

the environment is not compositional by definition. How is a global table compositional, you have to type the whole program to populate the environmentm. The environment is the problem.

I don't follow. The environment is not a global table! It specifies a scope, and can be extended locally. That and the weakening property is what makes it compositional.

The environment is an abstraction. It describes exactly what you need to know about a bunch of definitions to check all uses of these definitions.

Composition allows two fragments to be independently typed, and then the type of the composed single fragment depends only on the types of the two separate fragments.

If a function is defined in fragment A, and you cannot type fragment B without that type being in the environment that is not composable. To be composable you must be able to type B without any knowledge of A and vice versa.

It is still important that the type system gives a single most general type to any code fragment, and summerising that without expecting everyone to read derive this from the type system rules seems useful.

I think you are still missing the point: Most general relative to what? If there is only one type that the system can derive, than it is trivially the most general type, no matter what it is. Every deterministic type system is principal. It does not say anything.

Are you saying that deterministic is a stronger claim than principal (as in all deterministic systems have principal types or typings, but not all systems with principal types or typings are deterministic)?

So I would be better off claiming a type system with "compositional deterministic typings".

The point is that there are some type systems that do not have principal types or typings, and I wish to distinguish this type system from those. This type system has all the good properties of principality, and that should be noted. Should I expect everyone to know deterministic > principal?

Consider someone wanting a type system that is both compositional and has principal typings, I think this type system would fit their needs, and I would want them to find it when googling those terms. Perhaps it would be best to qualify the kind of principality as in: "compositional, deterministic principal typings"

I wonder if I could use the non-deterministic rules from a rank-1 intersection type system with the rank-0 restriction?

I think you are right, showing the spitting of M2 is a great idea. I did have the deletion of 'x' incorrectly at the end in my code.

I also think you have fixed the loop. Unifying with t2 is clearly wrong. Checking the source, this is what I am actually doing, so I obviously made an error tying to transcribe it to the notation at the beginning.

I have just realised that you must apply the substitutions from previous iterations in the current iteration. As I am using union-find variables to do the substitutions in my code this happens automatically when you die reference the variable name in unification etc. The easiest place to see this is in the abstraction rule where unifying the fresh variable a with exact type does nothing.

Yes,this is similar, and it is good to see that I am not the only person thinking along these lines. Their type system definition may be useful in describing this one better. One key difference is that Camarao and Figueiredo seem to use least-common-generalisation in the VAR rule, so there are differences in the approach

For one thing, you need to handle the case where (const 1 (foo 'bar')) is reduced to 1, removing constraints on foo from the environment. (e and e' might not have the same free variables, and even if they do, you need to show that the constraints are compatible).

Also, I don't think you're going to get out of doing something non-trivial with your environment. You can rephrase things as typings in an empty environment, but then E isn't empty, so how are you able to appeal to your algorithm producing HM types?

I don't understand what Keean is doing here:

1) empty |- (E |- e : t)

A double turnstile? Looks to me you need to define the lambda calculus the type checking rules and the reduction rules first.

Mind you, I have no experience with subject reduction proofs. I glance over them but I am both too thick as well as too precise to make much sense out of them.

If it's important then it should be in a teaching guide somewhere, otherwise ask someone who did it more often. Looks like an undergraduate exercise to me but I have no idea about the invariants they keep to make proofs like these work.

I don't understand this either:

(const 1 (foo 'bar')) -> 1

How are you going to reduce a record, is it, to 1? (Ah! 'const' is a Haskell idiom.)

There probably shouldn't be a double turnstile as empty == E... but as E is part of the typing produced I wrote it separately, but it will always be empty as the environment is empty, hence no free variables.

So my point was for any term where the environment is empty, the type produced by my algorithm is exactly that produced by algorithm-W. So as you only have to show (2) is derivable from (1) for cases with the empty environment, then the proof of subject reduction is identical to the proof for HM.

Maybe it would be clearer if I can show a step-by-step transform from algorithm-W to my algorithm.

As we start with an empty environment we have to show two equivalences:

1) let x = ... in x ... x ... x

Show that 'x' on the right is an instance of the type scheme of x on the left. This is trivial as it is exactly what the algorithm does.

2) \x . x ... x ... x

Show that all the types for 'x' on the right unify with each other (hence are monomorphic) and that is the type of 'x' on the left. This is trivial because this is what the algorithm does.

Really the above seems so obvious, i don't see what further is needed? I probably just need to explain it better.

Well. Abstractly, without understanding the type inference algorithms, you'ld need to show that a bisimulation exists between the steps the two algorithms take. Some relation with a number of invariants.

I don't know whether that implies you can do without a subject reduction proof for your specification. Been years since I thought about bisimulation proofs.

Hmpf. You're too much of a mathematician. Why not start small and do a subject reduction proof first? Rome wasn't conquered in a day. At least you'll better know how all the stuff works.

But the environment has to be empty for both e and e'? Is it not sufficient to show (2) is derivable from (1), with both the environments empty?

For (const 1 (foo 'bar')), how about:

let x = foo 'bar' in 1

(let x = (f true) in 1) : |- 

var ---------------------------------------
f : {f : a} |- a

var ---------------------------------------
true : |- Bool

f : {f : a} |- a
true : |- Bool
app ---------------------------------------
(f true) : {f : (Bool -> a)} |- a

lit ---------------------------------------
1 : |- Int

(f true) : {f : (Bool -> a)} |- a
1 : |- Int
let ---------------------------------------
(let x = (f true) in 1) : |- Int

So nice try but, it passes that test :-) anything else? Maybe I should offer a bounty for finding a term for which it fails subject reduction?

I wasn't arguing that your system doesn't have subject reduction. I was providing a counterexample to this:

Trivially E must be the same as we cannot reduce free variables (and E only contains the free variables in 'e').

My other comment was addressing this:

Trivailly as the environment is empty, the algorithm will give the same type to any expression as HM (where it is typeable in HM).

Which environment is empty? Are you only attempting to prove that subject reduction holds when E is empty? That's the only case where an appeal to having the same types as HM would make sense.

I thought that subject reduction required the environment to be empty? If this is not the case then what I said makes no sense. However Oleg said I only needed to show:

Subject reduction only says that given
        empty |- e : t
and     e --> e'
then the judgment
        empty |- e' : t
must be derivable. There may be other judgments
        empty |- e' : t'
with t' /= t that are also derivable. Subject reductions has nothing
to say about them.

So that implies we cannot know anything about 'const' from the environment, and infact we cannot know whether it ignores its second argument or not. So what is wrong with the following:

((const 1) (f true)) : |- 

var ---------------------------------------
const : {const : a} |- a

lit ---------------------------------------
1 : |- Int

const : {const : a} |- a
1 : |- Int
app ---------------------------------------
(const 1) : {const : (Int -> a)} |- a

var ---------------------------------------
f : {f : a} |- a

var ---------------------------------------
true : |- Bool

f : {f : a} |- a
true : |- Bool
app ---------------------------------------
(f true) : {f : (Bool -> a)} |- a

(const 1) : {const : (Int -> a)} |- a
(f true) : {f : (Bool -> a)} |- a
app ---------------------------------------
((const 1) (f true)) : {const : (Int -> (a -> b)), f : (Bool -> a)} |- b

Looking at it informally, in a strict language we would evaluate 'f' even if 'const' throws the result away (which we cannot know), removing 'f' is an optimisation. As such it does not seem a problem that this still requires 'f'.

Haskell would give:

:t const 1 (f True)
Not in scope: `const'
Not in scope: `f'

If we start with an empty environment.

And Oleg is always right.

Looks like the confusion boils down to that you need to start with an empty environment for a subject reduction proof over an abstract LC but that environment isn't always empty during a type derivation; a fact you need during the subject reduction proof.

You seem to be shifting goalposts. The quote I was responding to talked about E being the unchanged because it only referred to free variables which couldn't be reduced. Now you seem to be arguing that we only need to address the case of E empty. But that seems like it might be true... every program is eventually deployed in a completed context.

The notion of subject reduction comes from computational logic, where you usually consider full normalisation. In that situation, you reduce under binders and hence have to be able to deal with non-empty contexts in the proof.

In conventional programming languages you typically have weaker reduction relations that do not operate under binders. Hence, subject reduction proofs (these days rather called Preservation in the PL world) only need to consider empty environments (unless you have a store, like e.g. with lazy reduction).

More importantly, however, Preservation is just half of soundness anyway, and normally pretty boring if you have set up things right. Progress typically is the more interesting proof.

The notion of subject reduction comes from computational logic, where you usually consider full normalisation. In that situation, you reduce under binders and hence have to be able to deal with non-empty contexts in the proof.

Yeah, I was thinking you could maybe choose the --> relation to allow for reduction under binders, but still restrict attention to closed programs. Then use the fact that things correspond to HM types for closed contexts (a fact that shouldn't be too hard to proven) to borrow the fact that HM allows reduction under lambda without doing that work in a general context for this system. But I wasn't sure this would work out, so I slapped 'maybe' into my answer and moved on. I'm trying to extricate myself from this thread so I can get work done today :).

Indeed, if types with an empty environment are the same for my algorithm as algorithm-W, that gives a method for proving subject-reduction, and gives some indication that it might hold.

- Progress says that (closed) well-typed terms are either reducible or values.

So if we define well-typed as having an empty-context (which seams reasonable as something with undefined free variables cannot be run) then the same thought as above applies - this produces the same types as HM (for well-typed terms).

Essentially the difference is that an ill-typed term may be combined with another term and result in a well typed term.

So it would seem that simply stating that any term with a non-empty context is ill-typed would reduce the terms that have to be considered in preservation and progress to the same terms as HM (and would give them the same principal types as algorithm-W).

I don't understand how you can reduce a free variable? We don't know whether the variable is monomorphic or polymorphic?

The second seems to be the stronger argument in any case - we only need to deal with 'E' empty, and as such it is the same as HM. So for all the cases we need to deal with for subject reduction, it is the same as HM (or algorithm-W for HM).

Edit: I think the answer to how can you reduce a term with free variables is to simply define these as ill-typed. Now the set of well typed terms is the same as HM, and the types produced by my algorithm are the same as algorithm-W.

You may be interested in a Jeff Vaughan proof of correctness of HM. That's already nontrivial.

My point wasn't that proving HM was trivial, but that this algorithm might be trivially related to HM, we only need to consider the cases where the environment is empty, and therefore 'E' the context is empty, and in those cases my algorithm produces the same types as algorithm-W. In other words we can just borrow the proof for HM, as for all well-typed terms the types are the same.

No idea what you're talking about since I don't really understand anything of the subject. (Well, I could implement HM but that's beside the point.)

Man I have no idea. Specify an LC, a reduction system, do the soundness proofs, and see whether you can relate both derivations abstractly. I don't think you have another choice.

The paper was meant as a start of that exercise. It specifies an LC but doesn't give reduction rules and the HM soundness proof is incomplete but it may be a start.

If the HM proof is incomplete, why should I bother? After all people used HM without a complete soundness proof?

There is too much hand waving in the proof that he can claim to have proven HM correct. Which you shouldn't do if you want to learn how to do a proof of equivalence between your algorithm and HM.

HM is simple to prove correct by embedding in System F: you show how to translate a well-typed ML program into a well-typed System F program. If you also have given a dynamic semantics for HM, you must show that it coincides with System F's (and that is not necessarily trivial); if you defined your semantics by type erasure, you just have to prove that the translated System F term erases to the same untyped term.

Can your system be translated into System F? I suspect you may need a known-correct system with intersection types to translate arbitrary derivations.

translate a well-typed ML program into a well-typed System F program

ML programs are defined relative to a 'patched' together LC with imperative features. It should turn out to be pragmatically impossible to relate it to F unless you restrict to an ML over a pure LC.

Theoretically, very abstractly, they might turn out to be related somewhere but the above statement cannot be true.

By ML in this context I only referred to a program term along with a typing derivation in the Hindley-Milner (or Hindley-Milner-Damas) type system. You're right that it's often taken to include references (and sometimes exceptions) (it depends on the context), and in that different setting you would translate to System F with references (and exceptions).

Enough for what? You can make any type system compositional in this sense by delaying the actual type checking/inference. For example you can represent the "type" of a term as the term itself, and only check it when you are high enough up the AST to have enough information to do the checking. The question is what practical advantages does that give?

The very notion of 'compositional' typings is that the type of a composite subprogram is a simple function of the types of its components. How can that possibly be construed as suggesting typings of the fragments - the components - does not matter? Or am I misunderstanding your question?

I think we can't readily avoid considering 'the environment' in type systems for languages that express recursion through the namespace. If we instead expressed recursion with fixpoints we could work without environments. (This restriction is very useful to support streamable code.)

I am trying to understand exactly what I need to show in order to prove soundness of the type system. Oleg's comments seemed to imply that I only need to deal with the empty environment for subject reduction (unless I am misinterpreting them).

If your language has nice uniformity properties, then considering only empty environments should be sufficient - i.e. because `let` expressions (which locally extend the environment) are sufficient to model toplevel definitions and ad-hoc environments.

If your language lacks uniformity - i.e. due to second-class structures or features (multimethods, FFI, plugins, database tables, type providers, etc.) - then I expect your typings will generally include a non-empty environment of typing assumptions. This is my intuition.

Do you know which assumptions Oleg was making?

Well I only have simple lambda calculus at the moment, so assuming uniformity makes sense.

However as the type system has principal typings, it should allow first class modules, which might allow plugins to be treated in a uniform way?

Sure, if modules/plugins/etc. are first-class then their construction (or perhaps destruction) will be formally associated with the type system, and thus subject to the normal soundness proofs.

Well I only have simple lambda calculus at the moment, so assuming uniformity makes sense.

Hmm. You're fitting the language to the LC, not the LC to the language (which you don't seem to have developed, yet.)

Maybe just seeing it as an experiment would be better.

However as the type system has principal typings, it should allow first class modules, which might allow plugins to be treated in a uniform way?

Whether you can model an abstract module system is a property of the typing system. I don't think HM is sufficiently complex for that.

As an addendum. My bet is that a subject reduction proof also assumes an empty context as a means of stating an invariant, avoiding open terms. HM also doesn't allow for certain proofs like the cyclic types I discussed before, but you may not care about that.

Everything is an experiment, and from discussion comes greater understanding. I have a plan in terms of language features and how the type system will work. However there are many interdependent features and I am trying to keep the discussion to one point.