Typing vs. Subtyping


Is typing superfluous when we are given a sufficiently expressive
subtyping system?  Considering subsystems of the ST type system of
C.Raffalli [1,2], the answer is "yes or no", and can be related to the
problem of being able to define singleton types, and to prove that
types representing singletons in an adequate semantics are effectively
singletons.  The problem is solved in [2] for beta-eta-equivalence
classes, but can we do better (i.e. can we give weaker relations)?  We
will show some work related to this question.

References:

[1]System ST toward a type systemfor extraction and proofs of 
programs.C.Raffalli A.P.A.L 122 (2003) 107-130, Elsevier.

[2]System ST beta reduction and completeness. C.Raffalli LICS 2003.