OCaml에서 유추 추론 도움말

Question

이 두 함수의 형식이 잘 지정되었는지 어떻게 증명할 수 있습니까? 나는이 질문으로 조금 잃었다. 문제는 할당과 같은 이후

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) 

Answer 1

나는 완전히 본격적인 솔루션을 제공하지 않습니다.

유형 추론을 직접 수행하려면 원본을보고 공제해야합니다. 그런 다음 공제에서 모든 유형을 알 때까지 또는 불일치를 찾을 때까지 점점 더 많은 유형을 추론하십시오.

는 시작하려면 :

• reduce에서, 당신이있어 패턴 매칭 형 'a list의 패턴에 대해 lst합니다. 따라서 lst은 'a list으로 입력해야합니다.
• 각 패턴 뒤의 값은 동일한 유형이어야하므로 u의 유형은 f h (reduce f t u)입니다.

잇 cætera는 등 cætera는 ...