Typing Problems

The question is what problem I am solving by looking at other type inference algorithms.

1. Traditional HM style inference allows for the introduction of non-constructive types.
2. Traditional HM style inference leads to strange awkward fixes such as the monomorphism and value restrictions.
3. Impredicative HM style inference is awkward, I am not convinced that such modalities are needed.
4. Impredicative HM style inference in the general case is undecidable.

I need to elaborate on these points with examples.

1) might be minor. The introduction of non-constructive types might not be a problem since the general excuse for that could be that they cannot be instantiated except with non-terminating terms. Still, I guess the theoretical consequence is that such a type system is inconsistent. I need examples for that.

2) is major. I don't dig the value restriction and think it is nonsense; or rather, a poorly fixed bug of a typing system. Again, I need examples.

3) is just a conjecture.

4) is a major problem though some claim to have solved it.

Question is if and how a shift to type-constructors and constructive types would allow a fix of this. Generalizing what I am doing, I am going for a type system in which universally quantified types like ∀α.∀β. α → β are forbidden but we do allow constructive types such as ∀α.∃f. α → f(α), possibly interpreted as ∀α.∃f.(Λβ → f(β)) α, in the hope that only type arguments need be derived from the term and most 'logical' quantifiers can be used without a real restriction on where they occur in the type and can be dropped/made implicit.

Not sure I am solving any problem here.

Awkward Types

As I stated in the previous post, I am rethinking some assumptions of HM-style inference. An example on how I want to fix HM and another awkward example.

A main novelty of another typing system is that I think some of the problems stem from not differentiating between argument types and result types. I would like to see a bigger role for type constructors in the type system for the Hi language.

An example, the type σ → τ can be understood to be a propositional formula according to the constructive interpretation of types. For such a type, in the simply typed lambda calculus, a term should be constructed or assumed which constructs values of type τ from values of type σ. Dropping the propositional interpretation, I would rather see that such a type is interpreted, possibly denoted, as σ → f(σ); instead of moving the blame for proving the validity of a type to the term, I would like to work with types which are correct from a set-theoretic assumption, concentrate on what they denote, and type-check and derive properties accordingly.

It still begs the question whether there is anything wrong with naive HM inference and whether this small shift in interpretation would change anything fundamentally. A non-trivial example type which exposes what would change:

(σ → γ) → σ → (τ →γ) → τ → γ 

Let's look at the above type constructively. The propositional interpretation is that we should be able to construct a value of type γ out of the antecedent. Concretely, we have the choice to construct that value by combining the function of type σ → γ with a value of type σ, or similarly combining terms with types τ → γ and τ.

Let's change our view to the type-constructor interpretation of the above, making constructors explicit the type denotes

(σ → f(σ)) → σ → (τ →g(τ)) → τ → h where h = f(σ) = g(τ)

Here we now have a number of surprising choices.

One, we could chose to reject this type, since we cannot assume that a general constructor can be found which generates an equivalent type h = f(σ) = g(τ) for arbitrary σ and τ. Another possible interpretation of that is that the proof, the choice which would be made at the term level in a constructive calculus, hasn't been made explicit in the type.

Second, we could derive σ = τ and f = g, and interpret that type as

(σ → f(σ)) → σ → (σ →f(σ)) → σ → f(σ)

Lastly, another choice is to derive that f and g cannot depend on σ and τ, therefor they are Skolem constants and the valid interpretation of that type is

(σ → f()) → σ → (τ →f()) → τ → f()

(I would prefer this. It feels like a restricted approach which exposes that type variables which are normally universally quantified can be approximated with argument types, and existential types can be approximated with unknown Skolem functions. Not sure.)

Beyond awkward.

(Possibly, it is sufficient to forbid type variables at result positions, have the programmer make type constructors explicit, and check the validity of those? In the end, I guess the original example type is an example of a type which should be rejected, or made impossible to denote, by a type system which makes the constructors explicit. I.e., there should not be a valid translation for that type when made explicit since there is no interpretation which validates that type according to a type-constructor semantics.)

(I could have written this post differently and just expose that, hey, look there are types which make sense from a constructive point of view, but possibly do not make sense from a set-theoretic/type-constructor point of view. Moreover, by making the type constructors explicit, the proof burden associated with a classical propositional type is moved to the type - what remains is a validity check of the term.)

(Making sense of it all. I should rewrite this post, make clear I want to type-check with type constructors, show what the difference is w.r.t. traditional HM-inference, what problems that approach solves, and make explicit which choices one can make in the typing rules. My assumption at the moment is that type checking with type constructors could be a good alternative to impredicative typing.)

What's Wrong with Hindley-Milner?

Almost all students of CS learn basic type theory. In that setting, usually type systems are studied for lambda calculi where the starting point is the simply typed lambda calculus. Type systems are usually developed with an emphasis on a number of academic invariants, such as normalization, and the Curry-Howard correspondence.

I sometimes doubt the assumptions used and the usefulness of some of the type systems developed - especially within the context of the Hi language. As far as I am concerned, such a thing as normalization is only interesting in the context of long-term studies where programming languages are developed where well-typed programs terminate, a thing I am not very interested in within the pragmatic choices of a functional programming language which should work today. Moreover, from a programmer's point of view, as far as I am concerned, the only interesting property of the Curry-Howard correspondence is that it shows that you need a prover, or 'proving power,' to show that programs are well-typed.

Given those observations, I have a certain amount of distrust towards impredicative type systems which were originally developed within the context of types for logical statements, but now are implemented in functional programming languages. Are programming language developers progressing in the right direction, or are they progressing in a certain direction because of a lack of imagination at developing more pragmatic typing systems?

In that context, I would like to rethink the assumptions of Hindley-Milner based typing systems and go back to the only interesting property for type systems for programming languages: A well-typed program labels terms such that all values compute correctly.

But, there are an enormous amount of typing systems. Only experts know how to value them, I am not that big an expert, so the only option I have is to go back to simple examples and hope that I can make some sense of them and show where the theoretical pain lies.

A simple example:

      def f: (α → β) → α = f

Note that most Hindley-Milner based systems for functional programming languages will accept the above function.

I am interested in this particular example since it shows three things.

1. One, normalization is a non-issue, from that respect it is well-typed. A pragmatic type system should not care about normalization.
2. However, it shows a type for a function which I think should be rejected since one cannot construct a value from the domain of a function; a naive Hindley-Milner type derivation of the term can trick the type system in believing that all is okay. 
3. Lastly, it shows that this is not a problem of impredicativeness, but more a problem on what we believe a type denotes, and how to manage the unification of type variables.

The problem at the moment is that I have ideas on how to tackle this, but lack the oversight and vocabulary to correctly work towards a solution.

Not sure anymore. Possibly it is sufficient to keep HM style inference, but restrict the declared types to constructive types with a simple validity check.