Fonction ML de type 'a ->' b

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.}

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

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.

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.