mnieper
commented
3 years ago Just to give one example: One way to model a/the exception system in Scheme is to have a parameter current-raise that stores the current raise procedure so that raise could be defined through:
(define (raise obj)
((current-raise) obj))(With-exception-handler would then dynamically rebind current-raise in the body.)
The type of the parameter object would have to be the type of raise, namely ∀a.a→⊥ as obj can be of any type. This would mean, however, the current-raise has a type of rank 1, which would not be allowed by HM in this context.
Classical HM does not support the variety of higher-rank types that System F does. On the other hand, HM has complete type inference, while System F is probably too verbose to be used in a practical way (but see [1]).
In HM, for example, we cannot give arguments to functions a polymorphic type. We have to investigate (for example by studying the libraries of R6RS and R7RS) whether we want such a thing in practise or whether HM types are plenty enough so that we can associate types to the all the library procedures under investigation.
--
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf