Can you write polymorphic list functions such as cons, nil and reverse on the STLC?
To elaborate the question, in order to write cons, in Haskell, you need polymorphic types:
cons : ∀ a . a -> List a -> List a
There is no such thing as ∀ on the STLC, so I'd think it is obvious that polymorphic list functions are impossible, i.e., you need to write a new definition of cons for each specialized list type. But what if you leave the type annotation out, and instead have this:
cons = ...
a = cons 1 []
b = cons "" []
The inferencer can identify that cons : Int -> List Int -> List Int on the first case, and cons : String -> List String -> List String on the second case - no forall needed. Under this point of view, looks like polymorphic list functions aren't a problem on the STLC - you just can't annotate their types.
No, it is not possible to write polymorphic functions on STLC. In the definition of STLC there's no universally quantified types. In order to represent polymorphic lists you need some language with type abstraction, like System F.
In your question you mixed (please correct me, if I understand it wrong) the STLC with an inference algorithm for it. If you want polymorphic types, you need a language with type abstraction and application (in order to have type instantiation).
Type inference algorithms (like the ones used by Haskell or ML) consider a restrict version of System F, that is usually called Mini (or Core) ML. Such restrictions are motivated by the undecidability of type inference and checking for System F (details here). More details about this can be found on: