Fonction ML de type 'a ->' b

19

Notre professeur nous a demandé de penser à une fonction dans OCaml qui a le type

'a -> 'b

c'est-à-dire une fonction d'un argument qui pourrait être n'importe quoi, et qui peut retourner un autre chose.

J'ai pensé à utiliser raisedans une fonction qui ignore son argument:

let f x = raise Exit

Mais le professeur a dit qu'il y avait une solution qui ne nécessite aucune fonction dans la bibliothèque standard. Je suis confus: comment pouvez-vous en faire un 'bsi vous n'en avez pas en premier lieu?

Je demande ici plutôt que sur Stack Overflow parce que je veux comprendre ce qui se passe, je ne veux pas simplement voir un programme sans explication.

Gilles 'SO- arrête d'être méchant'
la source
2
Veuillez cibler la programmation d'apprentissage des élèves CS101 dans votre réponse, pas le théoricien de type que votre réponse pourrait l'inspirer à devenir plus tard.
Gilles 'SO- arrête d'être méchant'
Il serait utile que vous expliquiez comment vous avez compris que raisecela fonctionnerait, nous savons donc comment expliquer au mieux pourquoi la solution recherchée par votre prof (qui fonctionnera pour les mêmes raisons que celles qui raisefonctionnent) fonctionne.
sepp2k
@ sepp2k raise : exn -> 'aafin que je puisse obtenir la valeur de retour, j'ignore simplement l'argument.
Gilles 'SO- arrête d'être méchant'
1
Question de suivi: fonctions ML des listes polymorphes aux listes polymorphes
Gilles 'SO- arrête d'être méchant'
2
Voir aussi Pourquoi l'algorithme Hindley-Milner ne donnera-t-il jamais un type comme t1 -> t2? discuter d'un cadre plus théorique.
Gilles 'SO- arrête d'être méchant'

Réponses:

18

Le squelette est let f x = BODY. Dans BODY, vous devez utiliser x uniquement de manière générique (par exemple, ne l'envoyez pas à une fonction qui attend des entiers) et vous devez renvoyer une valeur de tout autre type. Mais comment cette dernière partie peut-elle être vraie? La seule façon de satisfaire la déclaration "pour tous les types 'b, la valeur renvoyée est une valeur de type 'b" est de s'assurer que la fonction ne retourne pas . Il y a exactement deux possibilités: soit BODY fautes ou il ne se termine pas. La fonction est raisedéfaillante, ce qui suit ne se termine pas:

let rec f x = f x
rgrig
la source
19

Tout d'abord, quelques remarques. En utilisant uniquement le calcul lambda typé de base, il n'est pas possible d'obtenir 'a -> 'bcar le système de typage est en correspondance (via l' isomorphisme de Curry Howard ) avec des logiques intuitionnistes, et la formule correspondante A → Bn'est pas une tautologie.

D'autres extensions telles que les tuples et les correspondances / conditions préservent toujours une certaine cohérence logique en ajoutant des types de produits *qui correspondent aux connecteurs logiques et , et des types de somme |qui correspondent aux ou . Encore une fois, ne vous attendez pas à ce qu'ils produisent ce 'a -> 'btype, car cela permettrait de prouver une formule qui n'est pas une tautologie.

Donc, vos seules chances sont d'utiliser d'autres constructions qui échappent aux logiques comme raise(mais vous n'y êtes pas autorisé dans ce cas)… ou let rec! La récursivité permet de construire des programmes qui ne se terminent jamais, et leurs résultats peuvent recevoir un type de retour arbitraire car ils ne seront jamais produits. Maintenant, si vous pensez à la fonction non terminale la plus triviale (celle qui s'appelle directement pour retourner un résultat):

let rec f x = f x

Vous remarquerez que son type est exactement 'a -> 'b: quel que soit l'argument fourni, le résultat (qui ne sera jamais calculé) peut être supposé avoir n'importe quel type.

Bien sûr, ce fn'est pas une fonction intéressante, mais c'est le point. Dans OCaml, toute fonction dont le type ne ressemble pas à une formule valide est une fonction suspecte.

Stéphane Gimenez
la source
Le demandeur n'a pas compris un mot de vos deux premiers paragraphes, mais j'aime bien votre phrase «leurs résultats peuvent recevoir un type de retour arbitraire car ils ne seront jamais produits».
Gilles 'SO- arrête d'être méchant'
1

En utilisant une primitive de compilation, vous pouvez écrire ceci:

external magic: 'a -> 'b = "%identity"

(et en effet la distribution du compilateur fournit cela, bien qu'elle ne fasse pas partie du langage). Il s'agit d'une distribution d'identité non sécurisée.

Votre professeur ne veut certainement pas cela. Cependant, c'est aussi la seule fonction utile avec le type 'a -> 'bque je connaisse, et en fait elle est utilisée dans la distribution OCaml elle-même.

Demi
la source