[Haskell-beginners] Type signatures returned with :t
Erik Dominikus
erik.dominikus71 at gmail.com
Sun Sep 19 04:09:37 UTC 2021
> What deeper lore am I not seeing here?
The "deeper lore" you are looking for is:
- Type variables that look unbound are actually implicitly bound with a
universal quantifier:
- "Maybe a" is actually "forall a. Maybe a";
- "Either a b" is actually "forall a. forall b. Either a b", that is,
"forall a. (forall b. Either a b)";
- "Either a (Either b c)" is actually "forall a. forall b. forall c.
Either a (Either b c)";
- "a" is actually "forall a. a";
- "f a" is actually "forall f. forall a. f a".
- alpha-equivalence: You can rename the bound variables of an expression
without changing its meaning, as long as you don't change the bindings.
- Example of changing the bindings: "forall x. forall y. x" (x is
bound by the first/outer quantifier) is not alpha-equivalent to
"forall y.
forall x. x" (x is bound by the second/inner quantifier).
Examples of alpha-equivalence (here "≡" reads "is alpha-equivalent to"):
forall a. forall b. Either a b
≡ forall x. forall y. Either x y
≡ forall b. forall a. Either b a
forall a. Either Bool a
≡ forall b. Either Bool b
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20210919/446aac35/attachment.html>
More information about the Beginners
mailing list