-------- Forwarded Message --------
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 |
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 |
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 |
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 |
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 |
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 |
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: _______________________________________________ Beginners mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners |
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 aBecause (->) 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 |
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 |
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 |
Free forum by Nabble | Edit this page |