Fwd: Re: Multiple letters between -> ->

-------- Forwarded Message --------
Subject: Re: [Haskell-beginners] Multiple letters between -> ->
Date: Sat, 25 Nov 2017 13:05:25 +0100
From: Marcus Manning
Hi,
Original I thought a Signature like:
f :: h a -> h a
means that h is a higher kinded type just like in Type Classes ( for instance f in Functor f).
But I heard such a meaning is not allowed in normal Haskell functions. What instead is the meaning of h a? Hello Marcus, you can write that but, since we know nothing about `h` and `a`,
On Thu, Nov 23, 2017 at 06:19:51PM +0100, Marcus Manning wrote: the only possible (non-undefined) function to implement that signature is:
f :: h a -> h a f = id
Any other implementation would require us to know something about h, hence a typeclass-constraint (e.g. Functor h =>) on h. _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

On Sat, Nov 25, 2017 at 01:06:03PM +0100, Marcus Manning wrote:
I do not believe that h is a higher kinded type. What I want to express is that a function f could take a type constructor as argument and simply returns it, but
f Maybe
throws an Error
Hello Marcus, you cannot pass type constructors (Maybe) to functions! Only *data* constructors (Just, Nothing). Hence the reason why the compiler complains, there is no *data* constructor named `Maybe`. Even in ghci, to inspect type constructors, we use a different command λ> :type Maybe <interactive>:1:1: error: • Data constructor not in scope: Maybe • Perhaps you meant variable ‘maybe’ (imported from Prelude) λ> :kind Maybe Maybe :: * -> *

Ok, but what is h in: f :: h a -> ... is "h" a data constructor or a type constructor or a normal function? What is j in f:: j k l -> ... and hwat is the difference between j and h? On 11/25/2017 01:48 PM, Francesco Ariis wrote:
On Sat, Nov 25, 2017 at 01:06:03PM +0100, Marcus Manning wrote:
I do not believe that h is a higher kinded type. What I want to express is that a function f could take a type constructor as argument and simply returns it, but
f Maybe
throws an Error Hello Marcus, you cannot pass type constructors (Maybe) to functions! Only *data* constructors (Just, Nothing). Hence the reason why the compiler complains, there is no *data* constructor named `Maybe`. Even in ghci, to inspect type constructors, we use a different command
λ> :type Maybe
<interactive>:1:1: error: • Data constructor not in scope: Maybe • Perhaps you meant variable ‘maybe’ (imported from Prelude) λ> :kind Maybe Maybe :: * -> *
_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

On Sat, Nov 25, 2017 at 03:03:26PM +0100, Marcus Manning wrote:
Ok,
but what is h in:
f :: h a -> ...
is "h" a data constructor or a type constructor or a normal function? What is j in
f:: j k l -> ...
and hwat is the difference between j and h?
`h` is a type constructor and `h a` denotes a kind of `* -> *`, hence λ> :t f f :: h s -> h s λ> :t f (Just 8) f (Just 8) :: Num s => Maybe s -- because Maybe :: * -> * λ> :t f Bool <interactive>:1:3: error: Data constructor not in scope: Bool :: h s Similarly, `f :: j k l -> j k l` would only work on kinds `* -> * -> *` (tuples, etc.) and not on Maybes (* -> *).

Ah thanks, I get confused with instance and declaration level. But why I can call g with Just: let g :: h a b -> h a b; g a = a g Just but Just is a->Maybe a On 11/25/2017 03:34 PM, Francesco Ariis wrote:
On Sat, Nov 25, 2017 at 03:03:26PM +0100, Marcus Manning wrote:
Ok,
but what is h in:
f :: h a -> ...
is "h" a data constructor or a type constructor or a normal function? What is j in
f:: j k l -> ...
and hwat is the difference between j and h? `h` is a type constructor and `h a` denotes a kind of `* -> *`, hence
λ> :t f f :: h s -> h s λ> :t f (Just 8) f (Just 8) :: Num s => Maybe s -- because Maybe :: * -> * λ> :t f Bool <interactive>:1:3: error: Data constructor not in scope: Bool :: h s
Similarly, `f :: j k l -> j k l` would only work on kinds `* -> * -> *` (tuples, etc.) and not on Maybes (* -> *).
_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

On Sat, Nov 25, 2017 at 04:19:04PM +0100, Marcus Manning wrote:
But why I can call g with Just:
let g :: h a b -> h a b; g a = a
g Just
but Just is a->Maybe a
Because (->) is a type constructor itself, just with convenient infix syntax: λ> :k (->) (->) :: TYPE q -> TYPE r -> *

I don't know if this is helpful, but I've abbreviated and elaborated on what Francesco said.
Original I thought a Signature like:
f :: h a -> h a
means that h is a higher kinded type just like in Type Classes ( for instance f in Functor f).
But I heard such a meaning is not allowed in normal Haskell functions. What instead is the meaning of h a?
Let's take a concrete example: Prelude> let f = fmap id Prelude> :t f f :: Functor f => f b -> f b Prelude> The (->) symbol goes between types (it takes one type to another), so f b must be a type, and therefore f is a type constructor.
f Maybe
throws an Error
Maybe is a type constructor, not a value constructor. Functions in Haskell can only take types. Value constructors are types; type constructors are not.
but what is h in:
f :: h a -> ...
is "h" a data constructor or a type constructor or a normal function? What is j in
f:: j k l -> ...
and hwat is the difference between j and h?
h and j in those examples are both type constructors. One of them takes two arguments, the other only takes one.
But why I can call g with Just:
let g :: h a b -> h a b; g a = a
g Just
but Just is a->Maybe a
Just has type "(->) a (Maybe a)", a.k.a. type "a -> Maybe a". (->) is a
two-argument type constructor.
On Sat, Nov 25, 2017 at 8:39 AM, Francesco Ariis
On Sat, Nov 25, 2017 at 04:19:04PM +0100, Marcus Manning wrote:
But why I can call g with Just:
let g :: h a b -> h a b; g a = a
g Just
but Just is a->Maybe a
Because (->) is a type constructor itself, just with convenient infix syntax:
λ> :k (->) (->) :: TYPE q -> TYPE r -> *
_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Jeff Brown | Jeffrey Benjamin Brown Website https://msu.edu/~brown202/ | Facebook https://www.facebook.com/mejeff.younotjeff | LinkedIn https://www.linkedin.com/in/jeffreybenjaminbrown(spammy, so I often miss messages here) | Github https://github.com/jeffreybenjaminbrown

Sorry again fo the long break, and thanks for explanation. Three Questions: 1.) Because (->) is defined with itself, it is also a Meta Type Constructor (TYPE == variable Rank Type == a Meta Type ?) 2.) How do I define a function which takes a 3-Kinded Type: let f:: h (g a); f a = a where g * -> * and h (*->*)->*, but it did not work as: h is deduced to be h * -> *. Prelude> let f:: h (g a); f a = a <interactive>:42:18: error: • Couldn't match type ‘h’ with ‘(->) (g a)’ ‘h’ is a rigid type variable bound by the type signature for: f :: forall (h :: * -> *) (g :: * -> *) a. h (g a) at <interactive>:42:5-15 Expected type: h (g a) Actual type: g a -> g a • The equation(s) for ‘f’ have one argument, but its type ‘h (g a)’ has none • Relevant bindings include f :: h (g a) (bound at <interactive>:42:18) What can I do? 3.) Is there any tool in Haskel where I can see which function parameter is bound to the given input, for instance something like a function showBinds: showBinds const (\c -> "s") (\(b,c) -> "c") Prelude> Param a gets (\c -> "s") b gets (\(b,c) -> "c") This is a simple example, but it gets more complicated with massive use of autocurrying. On 11/25/2017 05:39 PM, Francesco Ariis wrote:
On Sat, Nov 25, 2017 at 04:19:04PM +0100, Marcus Manning wrote:
But why I can call g with Just:
let g :: h a b -> h a b; g a = a
g Just
but Just is a->Maybe a Because (->) is a type constructor itself, just with convenient infix syntax:
λ> :k (->) (->) :: TYPE q -> TYPE r -> *
_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Hello Marcus, On Thu, Nov 30, 2017 at 12:37:12PM +0100, Marcus Manning wrote:
2.) How do I define a function which takes a 3-Kinded Type:
let f:: h (g a); f a = a
where g * -> * and h (*->*)->*, but it did not work as:
h is deduced to be h * -> *.
h hasn't got kind * -> * -> *, as Maybe hasn't got kind * -> * -> * but * -> *. A simple type constructor like the one you are searching for is Either λ> :k Either Either :: * -> * -> * or a tuple λ> :k (,) (,) :: * -> * -> *
participants (3)
-
Francesco Ariis
-
Jeffrey Brown
-
Marcus Manning