Comment définir une fonction d'ordre supérieur qui applique une fonction polymorphique à un type spécifique

Question

Si je définis

fun id x = x 

alors naturellement id est de type 'a -> 'a

Bien sûr, id 0 évalue à 0, ce qui rend Sens parfait.

Depuis ce sens parfait, je devrais pouvoir résumer par une fonction:

fun applyToZero (f: 'a -> 'a) = f 0 

Avec l'espoir que applyToZero aura le type ('a -> 'a) -> int et applyToZero id évaluera à 0

Mais quand je essayer de définir applyToZero comme ci-dessus, SML/NJ donne un message d'erreur impair qui commence:

unexpected exception (bug?) in SML/NJ: Match [nonexhaustive match failure] 
    raised at: ../compiler/Elaborator/types/unify.sml:84.37 

Cela ressemble presque à un bogue dans le compilateur lui-même. Bizarre, mais possible.

Mais PolyML n'aime pas non plus (bien que son message d'erreur est moins étrange):

> fun applyToZero (f: 'a -> 'a) = f 0; 
poly: : error: Type error in function application. 
    Function: f : 'a -> 'a 
    Argument: 0 : int 
    Reason: Can't unify int to 'a (Cannot unify with explicit type variable) 
Found near f 0 

Ce qui suit fonctionne le:

fun ignoreF (f: 'a -> 'a) = 1 

avec le type inféré ('a -> 'a) -> int. Cela montre qu'il n'est pas impossible de créer une fonction d'ordre supérieur de ce type.

Pourquoi SML n'accepte-t-il pas ma définition de applyToZero? Y at-il une solution de contournement qui me permettra de le définir de sorte que son type est ('a -> 'a) -> int?

Motivation: dans ma tentative de résoudre le puzzle this question, j'ai pu définir une fonction tofun de type int -> 'a -> 'a et une autre fonction fromfun avec la propriété désirée qui fromfun (tofun n) = n pour tous les entiers n. Cependant, le type déduit de mon travail fromfun est ('int -> 'int) -> 'int). Toutes mes tentatives d'ajouter des annotations de type pour que SML l'accepte comme ('a -> 'a) -> int ont échoué. Je ne veux pas montrer ma définition de fromfun puisque la personne qui a posé cette question pourrait encore travailler sur ce puzzle, mais la définition de applyToZero déclenche exactement les mêmes messages d'erreur.

Answer 1

Il ne peut se faire dans la plaine Hindley-Milner, comme utilisé par SML, car il ne prend pas en charge soi-disant plus classé ou un polymorphisme de première classe. L'annotation de type 'a -> 'a et le type ('a -> 'a) -> int ne signifient pas ce que vous pensez qu'ils font.

Cela devient plus clair si nous rendons le classeur pour la variable de type explicite.

fun ignoreF (f: 'a -> 'a) = 1 

signifie en fait

fun 'a ignoreF (f: 'a -> 'a) = 1 

qui est, 'a est un paramètre à l'ensemble de la fonction ignoreF, pas son argument f. Par conséquent, le type de la fonction est

ignoreF : ∀ 'a. (('a -> 'a) -> int) 

Ici, je fais le liant pour 'a explicite dans le type comme un quantificateur universel. C'est ainsi que vous écrivez de tels types dans la théorie des types, alors que SML maintient tous les quantificateurs implicites dans sa syntaxe. Maintenant, le type que vous pensiez que cela avait serait écrit

ignoreF : (∀ 'a. ('a -> 'a)) -> int 

Notez la différence: dans la première version, l'appelant de ignoreF obtient de choisir comment 'a est instancié, par conséquent, il pourrait être quelque chose, et la fonction ne peut pas assumer son int (ce qui explique pourquoi applyToZero ne vérifie pas le type). Dans le second type, l'appelant de l'argument peut choisir, c'est-à-dire, ignoreF.

Mais un tel type n'est pas supporté par Hindley-Milner. Il supporte seulement ce qu'on appelle le polymorphisme prenable (ou polymorphisme de rang 0) où tous les ∀ sont au niveau le plus externe - c'est pourquoi il peut les garder implicites, puisqu'il n'y a pas d'ambiguïté sous cette restriction. Le problème avec le polymorphisme de rang supérieur est que l'inférence de type est indécidable.

Donc, votre applyToZero ne peut pas avoir le type que vous voulez en SML. La seule façon d'obtenir quelque chose comme il est à l'aide du système de module et ses foncteurs:

functor ApplyToZero (val f : 'a -> 'a) = struct val it = f 0 end 

BTW, le message d'erreur que vous citez SML/NJ peut être ne peut pas causée par le code que vous montriez. Vous devez avoir fait autre chose.

Answer 2

Si nous utilisons l'algorithme d'inférence de type Hindley-Milner sur fun applyToZero f = f 0, nous obtiendrons f : int -> 'a en raison du terme f 0. Il est évident que f est une fonction f : 'b -> 'a. Nous appliquons cette fonction à 0, ainsi 'b = int. Par conséquent, l'annotation de type explicite f : 'a -> 'a génère l'erreur que vous observez. En passant, SML/NJ v110.80 fonctionne très bien sur ma machine et imprime le message d'erreur suivant:

stdIn:2.39-2.42 Error: operator and operand don't agree [overload - user bound tyvar] 
    operator domain: 'a 
    operand:   [int ty] 
    in expression: 
    f 0