This question is not subjective. A very specific verb is used in the referenced book, and I'd like to understand what the implication of that phrasing is, because I'm afraid I'm misunderstanding something.
From Learn You a Haskell, the following paragraph is the third and last one containing "we assume *
".
data Barry t k p = Barry { yabba :: p, dabba :: t k }
And now we want to make it an instance of
Functor
.Functor
wants types of kind* -> *
butBarry
doesn't look like it has that kind. What is the kind ofBarry
? Well, we see it takes three type parameters, so it's going to besomething -> something -> something -> *
. It's safe to say thatp
is a concrete type and thus has a kind of*
. Fork
, we assume*
and so by extension,t
has a kind of* -> *
. Now let's just replace those kinds with thesomething
s that we used as placeholders and we see it has a kind of(* -> *) -> * -> * -> *
.
Why are we assuming anything at all? Upon reading "we assume X (i.e. we assume that X is true)" it is natural for me to think that we should also consider the case that X is false. In the specific case of the example, couldn't t
be of kind (* -> *) -> *
and k
of kind (* -> *)
? If this was the case, whatever t
and k
actually were, t k
would still be a concrete type, no?
I see that the whole line of reasoning is then checked against the compiler, but I don't think the compiler assumes. If it does, I'd like to know what, if it doesn't then again I'm afraid I'm missing the meaning of the paragraph.
k :: L
for any kindL
, as long ast :: L -> *
. A compiler here must however choose some specificL
, or resort to a polykind. A polykind would be the most general option, but here GHC choosesL = *
(basic Haskell does not have polykinds, they have to be turned on as an extension). Since it chooses something which is rather arbitrary, LYAH uses the word "assume" (AFAICT). – chi Dec 7 '19 at 21:31