Comment puis-je connaître le type d'une fonction Haskell?

Question

Actuellement je me prépare pour mes examens et c'est quelque chose à propos de Haskell que je n'ai jamais vraiment compris.

La règle de type est le suivant

"et" moyens "et" en allemand.

Ainsi, les fonctions données sont

f :: ([a] -> b) -> a -> [b] 
g :: c -> Int -> c 

Et maintenant, je dois déterminer le type (f g) en utilisant la règle de type ci-dessus. Quelqu'un peut-il m'expliquer comment procéder à ce stade?

Answer 1

Juste pour rapidement en revue, nous savons que ces faits:

1. Si s :: sigma -> tau
   et t :: rho
   et gamma(sigma) = gamma(rho)
   puis s t :: gamma(tau).
2. f :: ([a] -> b) -> a -> [b]
3. g :: c -> Int -> c

Nous aimerions connaître le type de f g. Il semble que la règle (1) pourrait nous dire que si nous avons choisi s, t, sigma, tau, rho, et gamma de manière appropriée. Prenons quelques conjectures sur la façon dont nous pourrions les définir de manière appropriée et voir où cela nous mène.

• Depuis la conclusion (1) dit s t :: ... et nous voulons savoir f g :: ..., nous devrions probablement choisir s = f et t = g.
• Depuis la prémisse de (1) dit s :: sigma -> tau et nous avons choisi s = f et savons f :: ([a] -> b) -> a -> [b] de (2), nous devrions probablement choisir sigma = [a] -> b et tau = a -> [b].
• Depuis la prémisse de (1) dit t :: rho et nous avons choisi t = g et savons g :: c -> Int -> c de (3), nous devrions probablement choisir rho = c -> Int -> c.

Résumant nos choix, nous avons maintenant transformé (1) à cette forme:

Si f :: ([a] -> b) -> a -> [b]
et g :: c -> Int -> c
et gamma([a] -> b) = gamma(c -> Int -> c)
puis f g :: gamma(a -> [b]).

Il n'y a qu'une seule variable de (1) pour laquelle nous n'avons pas encore choisi de valeur, à savoir gamma.La troisième prémisse limite gamma un peu, à savoir, il doit satisfaire:

gamma([a] -> b) = gamma(c -> Int -> c) 

On peut supposer qu'il ya une hypothèse implicite selon laquelle il se comporte comme une substitution, qui est, récursion sur des structures de type et le remplacement des variables de type, de sorte que l'égalité précédente hypothèse est équivalente à celle-ci:

[gamma(a)] -> gamma(b) = gamma(c) -> Int -> gamma(c) 

pour cette équation est vrai, nous devons avoir toutes ces choses:

gamma(c) = [gamma(a)] 
gamma(b) = Int -> gamma(c) = Int -> [gamma(a)] 

Si nous faisons un choix arbitraire pour gamma(a), ces équations nous disent les résultats de gamma(b) et gamma(c); Choisissons gamma(a) = a. Puis:

gamma(a) = a 
gamma(b) = Int -> [a] 
gamma(c) = [a] 

Maintenant, nous avons rempli les locaux de (1), et nous apprenons sa conclusion:

f g :: gamma(a -> [b]) 
f g :: gamma(a) -> [gamma(b)] 
f g :: a -> [Int -> [a]]