Ricordo di aver letto da qualche parte che Hindley Milner era una restrizione sul sistema-f. In questo caso, qualcuno potrebbe fornirmi alcuni termini che possono essere digitati in system-f ma non in HM.Quali sono alcuni tipi e/o termini in system-f che non possono essere espressi in Hindley Milner
Qualsiasi cosa implichi un polimorfismo di livello superiore (vale a dire "di prima classe"). Ad esempio:
lambda f : (forall A. A -> A). (f Int 1, f String "hello")
Questa funzione avrebbe il tipo (forall A. A -> A) -> Int * String, che non esprimibile in HM, dove tutti i regimi di tipo polimorfici devono essere in "prenessa" forma (cioè il quantificatore può verificarsi solo all'esterno, non annidato).
Non sai cosa intendi, quell'espressione non è una funzione. Le definizioni (rilegato via let) possono essere polimorfiche con HM, ma i parametri di funzione non possono. –