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.)