"Determinism" of types?

Hi everyone,
I've been learning a small amount of type theory lately. I've noticed, as I'm sure most people have, that types in the typed lambda calculus always seem to be "determinable", I'm not sure what the correct term for it is. What I mean is this: a type is a ground type, or an arrow type, such that when applied to a term of the correct type, the type on the right of the arrow is also "determinable". For example, the following types are determinable:

Boolean (because it is a ground type)
a -> a
a -> b -> a

But these are not:
a -> b

Could someone point me in the right direction as to what to call this property, or if it even necessarily holds, and better yet, how to *prove* that it holds? Thanks!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Maybe you're just finding that in simply lambda calculus (among others) there are inhabited and uninhabited types: a type is inhabited if you can find a term having this type. The fact that there are uninhabited types is called consistency: it shows that the logic formalized by your type system is non-trivial: i.e. some statements are not true. Proofs of (relative) consistency are among the most interesting, and possibly the hardest in type theory, see the wikipedia page for more info.

Isn't a -> b inhabited by your definition?

Or does the term fun f x => f x not count?

Doesn't count

Doesn't count. It has the type forall a b . (a -> b) -> a -> b.

One way to read it is that for all a's and b's, no matter what a and b are, if you have a function from a to b and you have an a then you'll get a b. Read as logical implication : (a implies b) implies that a implies b, or, in other words, if a implies b then a implies b.

forall a b . a -> b says that for all a's and b's, no matter what a and b are, if you have an a then you'll get a b. Just try to write an actual function like that. Read as an implication : a implies b no matter what a and b are. So a -> b is the type that proves anything based on anything!

In a turing complete language, there is a way create a term with type a -> b. In Haskell

> convertAnything :: a -> b
> convertAnything = convertAnything

So the type checker doesn't prove that the infinite loop isn't really capable of doing the impossible. Thus I can now write nonsense like finding the square root of a string

> stringSqrt :: String -> Float
> stringSqrt string = sqrt $ convertAnything string

Any attempt to actually run the program will diverge, of course.

I think namin meant to write

I think namin meant to write "fun f x = f x", which is a recursive definition, and the SML analogue of convertAnything (except that convertAnything can be given an even weaker type convertAnything :: a).


That's what I meant.


Yes (assuming you mean "fun f x = f x"), forall a b.a -> b is inhabited in ML. That's why you can't use arbitrary ML programs (or Haskell programs) directly as proofs, without any extra information about termination (and lack of side effects).

If I understand correctly ,

If I understand correctly , then "a->(b->a) is determinable" is equivalent to "I can construct an expression that has polymorphic type a->(b->a)" . This is true , the expresion is (\x -> (\y -> x)) .
I can't do the same for a -> b . Every statement of the kind "x is determinable" coresponds to a theorem x in intuitionistic logic .
a->(b->a) is determinable iff "a implies (b implies a)" is true in intuitionistic logic .

Let a ∧ b denote the product type (in Haskell it coresponds to (a ,b) ), and a ∨ b denote the sum type (in Haskell it coresponds to Either a b ) . Then , the following hold :

# THEN-1: φ → (χ → φ)
# THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
# AND-1: φ ∧ χ → φ
# AND-2: φ ∧ χ → χ
# AND-3: φ → (χ → (φ ∧ χ))
# OR-1: φ → φ ∨ χ
# OR-2: χ → φ ∨ χ
# OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
are determinable types .

Inference rule : If φ and φ → ψ are determinable types , then so is ψ
Nothing else is a determinable type .


Thanks for the help

Thanks for the help. So it all comes back to predicate calculus?

I guess what I wanted to know is that the type of any expression in the typed lambda calculus can be determined at any part of the evaluation. For example, ground types can always be determined during evaluation. For the type a->a, if we apply it to some other term, then we can get the resulting type of the evaluation (a will be bound). But if we apply some hypothetical term with the type a->b, then we cannot deduce the resulting type (b will not be bound).

The reason why I want to know this is because I'm trying to design some different evaluation semantics, where the order of evaluation depends upon the type. I'd like to prove then that the type can always be determined.
Thank you for the help so far.


So it all comes back to predicate calculus?

Only if you want to. If you give types intuitionistic logic meaning, yes, otherwise, no. Not all type system for PL abide the correspondence.

Related discussion

This discussion is about something similar: Non-standard type theories for FP.

I'm not sure how similar though.


Depends what you mean by typed lambda calculus . If , for example , you are using Hindley–Milner type system (used by Haskell) or something weaker , then you can not construct terms with undetermined types , and every term is always given the most general correct type at compile time , via the Hindley–Milner type inference algorithm (if a term can not have a correct type , the compiler sends a specific error) . If , however , you are using a stronger type system , things might not be decidable without explicit typing .

Actually this is not always true

Consider type functions and their use in multi-parameter type classes.

The intuition here is that the types associated with the arguments and results constitute a relation, and there must exist a deterministic function from the known elements in the relation to the missing types. While it is usual to proceed from parameters to results, the actual resolution can occur in either forward or backwards fashion so long as the result is deterministic. There are examples in multi-parameter type classes in which resolution proceeds from result to parameter!

Might have a look at Mark Jones work on functional dependencies in Type Classes with Functional Dependencies.