To pytanie nie jest subiektywne. Bardzo konkretny czasownik jest używany w książce, do której się odwołuje, i chciałbym zrozumieć, jakie są implikacje tego sformułowania, ponieważ obawiam się, że coś źle zrozumiałem.
W Learn You a Haskell poniższy akapit jest trzecim i ostatnim, który zawiera „zakładamy *”.
data Barry t k p = Barry { yabba :: p, dabba :: t k }A teraz chcemy zrobić z tego przykład
Functor.Functorchce rodzajów,* -> *aleBarrynie wygląda na to, że ma tego rodzaju. Jakiego rodzajuBarry? Widzimy, że wymaga trzech parametrów typu, więc tak będziesomething -> something -> something -> *. Można śmiało powiedzieć, żepjest to konkretny typ, a zatem ma swego rodzaju*. Dlakzakładamy,*a więc co za tym idzie,tma niby* -> *. Teraz po prostu zamieńmy te rodzaje na tesomething, których używaliśmy jako symbole zastępcze i widzimy, że ma coś w rodzaju(* -> *) -> * -> * -> *.
Dlaczego w ogóle coś zakładamy? Po przeczytaniu „zakładamy, że X (tzn. Zakładamy, że X jest prawdą)” jest dla mnie naturalne, że powinniśmy również rozważyć przypadek, w którym X jest fałszywy. Czy w konkretnym przypadku tego przykładu nie może tbyć miły (* -> *) -> *i kmiły (* -> *)? Jeśli tak było, cokolwiek ti kfaktycznie tak było,t k nadal będzie to rodzaj betonu, nie?
Widzę, że cała linia rozumowania jest następnie porównywana z kompilatorem, ale nie sądzę, że kompilator zakłada . Jeśli tak, chciałbym wiedzieć, a jeśli nie, to obawiam się, że nie rozumiem znaczenia akapitu.
k :: Lna każdy rodzajL, o ilet :: L -> *. Kompilator tutaj musi jednak wybrać jakiś konkretnyLlub uciekać się do polikinda. Polykind byłby najbardziej ogólną opcją, ale tutaj GHC wybieraL = *(podstawowy Haskell nie ma polikindów, należy je włączyć jako rozszerzenie). Ponieważ wybiera coś, co jest raczej arbitralne, LYAH używa słowa „zakładać” (AFAICT).