I am building an extended run-time type system for Javascript and have some trouble implementing parametric polymorphism.
I am already able to type polymorphic first order functions:
const append = Fun("append :: [a] -> [a] -> [a]", xs => ys => xs.concat(ys));
append([1,2]) ([3,4]); // [1,2,3,4]
append([1,2]) (["a","b"]); // fails
There is state shared between the sequential function calls that enforces all as in the type annotation to be bound to the same concrete type.
However, things get much harder as soon as I try to type higher order functions:
const apply = Fun("apply :: (a -> b) -> a -> b", f => x => f(x));
const id = Fun("id :: a -> a", x => x);
apply(id) (2); // 2
The problem is that a/b of the function argument are not the same as those of the higher order function, because each function (a proxy with an apply trap behind the scene) has its on scope to bind type variables to concrete types. As a result the following unwanted implementation of apply with an explicit type cast doesn't fail:
const apply = Fun("apply :: (a -> b) -> a -> b", f => x => f(x) + "");
const inc = Fun("inc :: Number -> Number", x => x + 1);
apply(inc) (2); // "3"
Intuitively I tried to maintain state between all involved functions but this gets messy quickly.
Another approach is to adapt the type annotations of higher order functions according to those of their function arguments. Function arguments are frequently monomorphic like inc but sometime polymorphic like id as well. To stick with my example here are examples for both scenarios:
apply :: (a -> b) -> a -> b
apply f x = f x
inc :: Int -> Int
inc x = x + 1
:t apply inc -- Int -> Int (a becomes Int, b becomes Int)
id :: a -> a
id x = x
:t apply id -- b -> b (a becomes b, b remains b)
It seems as if all I need were two simple substitution rules for my type annotations - no additional state necessary. I know that my reasoning is rather simple. The question is if it is too naive in order to obtain reliable parametric polymorphism. Am I oversimplifying things?