I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type application in a term afterward.
For example, identity function is defined like below in Haskell.
id :: forall a. a -> a id = \x -> x
But in lambda calculus which is adopted as Haskell's core language, this represents
id = ΛT. λx:T. x (
ΛT is a type abstraction).
And following function
foo :: Int foo = id 3
is translated into
foo = id @Int 3 in the core language (
@Int is a type application)
Inserting type abstraction looks simple (just inserting
ΛT in the place corresponding to
forall a.), but type application is complicated because you have to decide not only where to apply the type but also what type to apply.
Although visualization of type application is discussed on this web page, I have not been able to find any document that describes an implicit insertion algorithm of type abstraction/application. It would be great if you could just give me a hint of the algorothm.