Fwd: Re: Multiple letters between -> ->

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Fwd: Re: Multiple letters between -> ->

Marcus Manning




-------- Forwarded Message --------
Subject: Re: [Haskell-beginners] Multiple letters between -> ->
Date: Sat, 25 Nov 2017 13:05:25 +0100
From: Marcus Manning [hidden email]
To: Francesco Ariis [hidden email]


Sorry, for the long break.

Thanks for replying.

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
<interactive>:13:3: error:
    • Data constructor not in scope: Maybe :: h a
    • Perhaps you meant variable ‘maybe’ (imported from Prelude)

So what instead does h a mean in a function declaration?

Cheers,

Marcus.

On 11/23/2017 06:27 PM, Francesco Ariis wrote:
> On Thu, Nov 23, 2017 at 06:19:51PM +0100, Marcus Manning wrote:
>> 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`,
> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Francesco Ariis
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Marcus Manning
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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Francesco Ariis
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Marcus Manning
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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Jeffrey Brown
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



--
Jeff Brown | Jeffrey Benjamin Brown
Website   |   Facebook   |   LinkedIn(spammy, so I often miss messages here)   |   Github   

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Marcus Manning
In reply to this post by Francesco Ariis
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Francesco Ariis
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 (,)
    (,) :: * -> * -> *

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Fwd: Re: Multiple letters between -> ->

Francesco Ariis
On Thu, Nov 30, 2017 at 12:55:07PM +0100, Marcus Manning wrote:
> But Either is not (*->*)->*, instead it is *->(*->*). Is (*->*)->*
> expressable in Haskell functions?

Yes, with an appropriate data declaration:

    λ> data FooType a = FooCons (a Int)
    λ> :k FooType
    FooType :: (* -> *) -> *

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners