Início / coding / Perguntas / 77977046
Accepted
Alberto Zaccagni
Asked: 2024-02-11 22:11:01 +0800 CST

Descobrir por que esses tipos diferem ao usar um catch all na correspondência de padrões

  • 772

Gostaria de ajuda para entender como a inferência de tipo afeta o código a seguir, que vem de uma pergunta anterior (que, após algumas reflexões, simplifiquei para o seguinte):

type 'a result =
  | Succ of 'a
  | Fail

let first f = function
  | Succ c -> let res = f c in Succ res
  | fail   -> fail

let second f = function
  | Succ c -> let res = f c in Succ res
  | Fail   -> Fail

Minha pergunta é: por que fin firsthave type ('a -> 'a)mas fin secondhave type ('a -> 'b)?

Você pode vê-lo aqui .

ocaml

1 respostas

  1. Best Answer
    • As duas ocorrências de Failin são tratadas como dois valores distintos e, portanto Fail -> Fail, secondpodem ter tipos diferentes 'a resulte 'b result, mas
    • As duas ocorrências de failin são tratadas como o mesmo valor e, portanto, não podem alterar os tipos fail -> fail.first

    Ou pelo menos o sistema de inferência de tipos não permite alterar tipos. Não tenho certeza se isso é uma especificação ou uma peculiaridade desse intérprete específico.

    Como alimento para reflexão, uma terceira versão:

    let third f r = match r with
  | Succ c -> Succ (f c)
  | _ -> r

    Você e eu sabemos que se chegarmos ao _caso do pattern-match, significa que ré Faile pode ser de qualquer 'b resulttipo, mas o que o compilador vê é que é rdo tipo 'a resultjá que é a entrada, e assim por diante 'a == 'b.

    • 2

relate perguntas