Just a single datapoint: this explanation started to lose me at “and a -> String. (In that last one, the type function is the arrow; Haskell would allow you to write it (->) a String. Also, (->)is the only type that HM specifically requires to exist.)” I don’t understand what the arrow _is_, nor why HM requires it to exist. Googling didn’t actually seem to help much, but that’s likely because “it” has a name that I don’t know.
You further lost me when you went on to write “sticking one or more “∀”s in front of a monotype”. I don’t know what an upside-down A is—I think I’ve read about these in various mathematical contexts, but I’m not sure if what I remember from those is the same as the meaning here, and the following paragraphs unfortunately didn’t elucidate.
I really appreciate the effort you put into this. Hopefully someday I’ll come back and be able to take those steps that I don’t yet know enough to take now.
To answer your questions, a -> b denotes functions from type a to type b; so the function “round”, taking a float and returning an int, has type Float -> Int. It’s required to exist just because the rules of type inference specifically refer to it. You could implement HM without a List type or an Int type, it might be silly, but it would be meaningful. But if you tried to implement it without ->, it’s not clear to me what you’d actually be implementing.
And ∀ is read “for all”—it’s pretty standard in math, but if you don’t know it or how standard it is, yeah, it would be opaque. Someone commented when I first wrote this that I ought to make a note of that, and I agreed it was a good idea and forgot to do it. I’ll try again to remember to update it in the near future, along with a note about the arrow.
Just a single datapoint: this explanation started to lose me at “and
a -> String. (In that last one, the type function is the arrow; Haskell would allow you to write it(->) a String. Also,(->)is the only type that HM specifically requires to exist.)” I don’t understand what the arrow _is_, nor why HM requires it to exist. Googling didn’t actually seem to help much, but that’s likely because “it” has a name that I don’t know.You further lost me when you went on to write “sticking one or more “∀”s in front of a monotype”. I don’t know what an upside-down A is—I think I’ve read about these in various mathematical contexts, but I’m not sure if what I remember from those is the same as the meaning here, and the following paragraphs unfortunately didn’t elucidate.
I really appreciate the effort you put into this. Hopefully someday I’ll come back and be able to take those steps that I don’t yet know enough to take now.
Thanks for the datapoint!
To answer your questions,
a -> bdenotes functions from type a to type b; so the function “round”, taking a float and returning an int, has typeFloat -> Int. It’s required to exist just because the rules of type inference specifically refer to it. You could implement HM without aListtype or anInttype, it might be silly, but it would be meaningful. But if you tried to implement it without->, it’s not clear to me what you’d actually be implementing.And
∀is read “for all”—it’s pretty standard in math, but if you don’t know it or how standard it is, yeah, it would be opaque. Someone commented when I first wrote this that I ought to make a note of that, and I agreed it was a good idea and forgot to do it. I’ll try again to remember to update it in the near future, along with a note about the arrow.Thanks again!