[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