Comment procéder pour prouver que ces deux fonctions sont bien typées? Je suis un peu perdu avec cette question.Aide à l'inférence de type dans OCaml
let rec reduce f lst u =
match lst with
| [] -> u
| (h::t) -> f h (reduce f t u)
let rec forall2 p l1 l2 =
match (l1,l2) with
| ([],[]) -> true
| ([],_) -> false
| (_,[]) -> false
| ((h1::t1),(h2::t2)) ->
(p h1 h2) && (forall2 p t1 t2)
Je ne vais pas donner une solution à part entière puisque la question ressemble à une mission.
Pour faire l'inférence de type vous-même, tout ce que vous avez à faire est de regarder la source et faire des déductions. Puis, à partir de vos déductions, en déduire de plus en plus de types jusqu'à ce que tous les types sont connus, ou jusqu'à ce que vous avez trouvé une divergence.
Pour vous aider à démarrer:
reduce, vous êtes motif correspondant lst contre les modèles de type 'a list. Ainsi, lst doit être entré comme 'a list.u a le même type que f h (reduce f t u).Et cætera, et cætera ...
Que voulez-vous dire par "preuve d'une fonction à l'aide d'une inférence de type"? Avez-vous une mission pour prouver que ces fonctions sont bien tapées à la main? – camlspotter
Oui, je dois prouver qu'ils sont bien typés, mais j'ai du mal à savoir par où commencer ou un exemple à suivre. – user3460123
Commencez avec les cas de base et les types connus, puis revenez en arrière à partir de là. – glennsl