Type signatures returned with :t

:t Just True Just True :: Maybe Bool :t Left True Left True :: Either Bool b :t Right False Right False :: Either a Bool
What am I being told here? It seems data Maybe a = Just a | Nothing data Either a b = Left a | Right b are both straightforward parameterized types, but Maybe doesn't give me a type parameter back, while Either does, and in different order, different names (a becomes b; b becomes a) depending on which variable I invoke. What deeper lore am I not seeing here? -- ⨽ Lawrence Bottorff Grand Marais, MN, USA borgauf@gmail.com

Il 18 settembre 2021 alle 17:30 Galaxy Being ha scritto:
:t Just True Just True :: Maybe Bool :t Left True Left True :: Either Bool b :t Right False Right False :: Either a Bool
What am I being told here? It seems are both straightforward parameterized types, but Maybe doesn't give me a type parameter back, while Either does, and in different order, different names (a becomes b; b becomes a) depending on which variable I invoke. What deeper lore am I not seeing here?
When you ask the type of λ> :t Just True the interpreter *knows* that that `Maybe` is not just a `Maybe a` (so type constructor and its type parameter) but the /concrete/ type `Maybe Bool`. This would not be the case if we did λ> :t Nothing Nothing :: Maybe a Same story with `Either`. Each of the two data constructors (`Left` and `Right`) let the interpreter infer just *one* of the type parameters (the `a` and `b` in `Either a b`). Does this answer your question?

Either returns with its parameters, reversed, but Maybe did not. That's my
main question.
On Sat, Sep 18, 2021 at 5:43 PM Francesco Ariis
Il 18 settembre 2021 alle 17:30 Galaxy Being ha scritto:
:t Just True Just True :: Maybe Bool :t Left True Left True :: Either Bool b :t Right False Right False :: Either a Bool
What am I being told here? It seems are both straightforward parameterized types, but Maybe doesn't give me a type parameter back, while Either does, and in different order, different names (a becomes b; b becomes a) depending on which variable I invoke. What deeper lore am I not seeing here?
When you ask the type of
λ> :t Just True
the interpreter *knows* that that `Maybe` is not just a `Maybe a` (so type constructor and its type parameter) but the /concrete/ type `Maybe Bool`. This would not be the case if we did
λ> :t Nothing Nothing :: Maybe a
Same story with `Either`. Each of the two data constructors (`Left` and `Right`) let the interpreter infer just *one* of the type parameters (the `a` and `b` in `Either a b`). Does this answer your question? _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- ⨽ Lawrence Bottorff Grand Marais, MN, USA borgauf@gmail.com

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

I hope the wizards will forgive a down-to-earth analogy.
Either a b is a knapsack with two pockets, the one on the Left (which must
hold an "a") and the one on the Right (which must hold a "b"). But you can
only use one pocket at a time.
So when there's a specific case of Either a b such as Left True, all that
can be concluded is that this is a case of an Either whose left pocket must
be able to handle a Bool; there's not enough information to know what could
have been put in the Right pocket. So only the left-pocket type ("a") can
be replaced with something specific.
Similarly, for a specific case of Right False, it's clear that the right
pocket holds a value of type Bool (replacing the general "b"), but there's
no information to identify what type might be in the left pocket. So it
remains unspecified.
I hope that helps.
-jn-
On Sat, Sep 18, 2021 at 9:21 PM Galaxy Being
Either returns with its parameters, reversed, but Maybe did not. That's my main question.
On Sat, Sep 18, 2021 at 5:43 PM Francesco Ariis
wrote: Il 18 settembre 2021 alle 17:30 Galaxy Being ha scritto:
:t Just True Just True :: Maybe Bool :t Left True Left True :: Either Bool b :t Right False Right False :: Either a Bool
What am I being told here? It seems are both straightforward parameterized types, but Maybe doesn't give me a type parameter back, while Either does, and in different order, different names (a becomes b; b becomes a) depending on which variable I invoke. What deeper lore am I not seeing here?
When you ask the type of
λ> :t Just True
the interpreter *knows* that that `Maybe` is not just a `Maybe a` (so type constructor and its type parameter) but the /concrete/ type `Maybe Bool`. This would not be the case if we did
λ> :t Nothing Nothing :: Maybe a
Same story with `Either`. Each of the two data constructors (`Left` and `Right`) let the interpreter infer just *one* of the type parameters (the `a` and `b` in `Either a b`). Does this answer your question? _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- ⨽ Lawrence Bottorff Grand Marais, MN, USA borgauf@gmail.com _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

On 19.09.21 00:30, Galaxy Being wrote:
:t Just True Just True :: Maybe Bool
What's the type of `Just`?
:t Just Just :: a -> Maybe a
So `Just` is a constructor function that takes a value of type `a` and gives you back a value of type `Maybe a`. In your example you provide a concrete type for `a` (`True :: Bool`) so the type of the result is `Maybe Bool`.
:t Left True Left True :: Either Bool b
As above what's the type of `Left`?
:t Left Left :: a -> Either a b
Again, `Left` is a constructor function that takes a single value of type `a` but now returns a value of type `Either a b`, i.e. it has two type variables. If you specify the type of `a` (again `Bool` in your example), `b` is still unspecified/polymorphic and that's why the resulting type is `Either Bool b`. Bye, Andreas

are both straightforward parameterized types, but Maybe doesn't give me a type parameter back, while Either does, and in different order, different names (a becomes b; b becomes a) depending on which variable I invoke.
Try these diagnostics:
--- Diagnostic 1
Given that the type of "const" is "a -> b -> a" and the type of "True" is
"Bool":
:t const
const :: a -> b -> a
:t True
True :: Bool
What do you expect the type of "const True" to be?
:t const True
const True ::
participants (5)
-
Andreas Perstinger
-
Erik Dominikus
-
Francesco Ariis
-
Galaxy Being
-
Joel Neely