Lambda the Ultimate

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.

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 .

http://en.wikipedia.org/wiki/Intuitionistic_logic

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

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 .

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.