Exemplos de inferência de tipos

Exemplo 1

Qual o tipo da seguinte função?
  1. A função tem um argumento. Portanto, o seu tipo terá uma seta no nível exterior. A forma do tipo será:

  2. Olhando para o corpo da função, percebe-se logo que "x" tem de ter tipo inteiro por causa do operador "+". Temos então:

  3. O resultado da função é um par ordenado, como se vê. Então:

  4. As duas componentes do resultado têm de ser inteiras por causa do uso de "x", que é inteiro. Então:

Exemplo 2

Qual o tipo da seguinte função?
  1. A função tem três argumentos. Portanto, o seu tipo terá três setas no nível exterior. A forma do tipo será:

  2. Olhando para o corpo da função, dá jeito começar a tratar o "z" (o terceiro argumento) por estar a ser usado de forma livre e poder ter um tipo qualquer α. Temos então:

  3. No corpo da função, "y" está a ser usado como função. Vemos ainda que "y" é aplicado a um argumento de tipo α. Além disso o resultado de y está a ser usado de forma livre, pelo que terá tipo β. Então:

  4. No corpo da função, "x" está a ser usado como função com dois argumentos. Vemos que o primeiro argumento tem tipo α e o segundo tipo β. Então:

  5. Qual o tipo do resultado da função "x"? Esse tipo é livre, pois não está sujeito a qualquer restrição causada por uma operação. Será então γ.

  6. Como os resultados de "f" e "x" têm o mesmo tipo, finalmente:

Exemplo 3

Agora um exercício ao contrário. Invente uma função que tenha o seguinte tipo:
  1. Vemos que a função tem um argumento:

  2. O resultado precisa de ser uma função com dois argumentos:

  3. Queremos obrigar x a ser inteiro e y e z a serem strings. Pode ser assim:

  4. Esta é praticamente a função pretendida, exceto que o resultado é booleano e não float. Resolve-se facilmente adicionando um if:

Outra maneira: Numa aula teórica futura vamos estudar regras de equivalência entre funções e regras de equivalência entre tipos de funções. Uma coisa que vamos aprender é que o operador de tipos -> é associativo à direita. Portanto o tipo deste problema é equivalente a este: Vamos repetir a resolução do problema, agora para este tipo.
  1. Vemos que a função tem três argumentos:

  2. Queremos obrigar x a ser inteiro e y e z a serem strings. Pode ser assim:

  3. Esta é praticamente a função pretendida. Mas o resultado está a ser booleano e não float. Resolve-se facilmente adicionando um if: