Voir par exemple Data.Maybe.Base dans le fichier stdlib - tous Maybe, Any et All ont un constructeur just.Comment désambiguïser les noms de constructeur en conflit
Agda permet ces définitions. Comment peut-on spécifier lequel utiliser?
Chaque type de données est livré avec son propre module. Donc Maybe, All et Any sont tous les constructeurs de type et les modules simultanément. Ainsi, vous pouvez écrire Maybe.just, All.just ou Any.just pour désambiguïser le constructeur. Ou il peut être désambiguïsé par l'inférence de type (l'unification est un terme plus approprié) ou une signature de type explicite comme Thilo dit dans leur commentaire. (Ce n'est pas vrai cependant que vous obtiendrez une erreur s'il y a une ambiguïté - vous obtiendrez une méta non résolue).
Si vous voulez être technique, le meilleur terme est probablement quelque chose comme "Désambiguïsation orientée type" qui est possible lorsque vous êtes en mode * vérification * car vous avez déjà un type et, étant donné que vous voulez que l'expression ait ce type, il est assez clair quel type de données le constructeur correspond. – gallais
@gallais, vous pouvez obtenir ce type par unification. C'est à dire. si vous avez quelque chose comme 'let f = just dans f (fromMaybe 0 (f 0))', alors les deux 'f' seront désambiguïsés même si nous pouvons être en mode d'inférence. Mais oui, le terme correct pour ce genre de chose est la résolution de nom orientée type. – user3237465
Vous avez en effet raison. – gallais
Inférence de type. Lorsque vous appelez l'une des fonctions 'just', elle essaie de voir de quel type de résultat vous avez besoin (en fonction de l'endroit où vous utilisez ce résultat). Si cela reste ambigu, vous obtiendrez une erreur et devrez ajouter une déclaration de type explicite quelque part. Espérons qu'il n'y en ait qu'un dans un endroit stratégique qui rende tout le reste clair (mais les déclarations de type explicites sont toujours de bon style, ne serait-ce que pour la documentation). – Thilo