[Haskell-cafe] minor confusion over kinds....

[Ben]

It sounds a bit like you're under the impression that * is some sort of wildcard for kinds, when you talk about "named kinds vs unnamed kinds". That's not correct; * IS a "named kind", and its name is *. Nat is distinct from * in exactly the same way that Bool is distinct from ().

Kind variables are exactly what you want, if you need to be able to handle both * -> * and Nat -> *.

The reasons for not always using (k -> *) -> Constraint rather than (* -> *) -> Constraint are the same as the reason for not making everything polymorphic at the type level; sometimes you need the assumption that your k really is *, and sometimes you just don't need the polymorphism and prefer to keep it simple (especially as kind variables require extensions).

On 6 May 2015 11:06:24 pm AEST, "Nicholls, Mark" <nicholls.mark at vimn.com> wrote:
>lets try it the other way around
>
>> instance Foo' SNat1 where
>>   type Bar' SNat1 = Z1
>>   bar' = SZ1
>
>that works!
>
>(my language will be wrong here...but the jist is)
>
>So in some something of kind
>"*->*" is substitutable for a parameter of kind "k -> *"
>"Nat->*" is substitutable for a parameter of kind "k -> *"
>"*->*" is substitutable for a parameter of kind "* -> *"
>"Nat->*" is NOT substitutable for a parameter of kind "* -> *"
>
>Hmmmm
>
>So why would I ever want to define a type class of kind
>(* -> *) -> Constraint
>Instead of
>(k -> *) -> Constraint
>
>?
>
>I think I don't completely understand what's going on.
>
>From: Nicholls, Mark
>Sent: 06 May 2015 1:02 PM
>To: haskell-cafe at haskell.org
>Subject: minor confusion over kinds....
>
>And what "*" means as opposed to other things e.g. an explicit name
>"Nat" or a kind variable "k"
>
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE ExplicitForAll #-}
>> {-# LANGUAGE FlexibleContexts #-}
>> {-# LANGUAGE FlexibleInstances #-}
>> {-# LANGUAGE GADTs #-}
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE PolyKinds #-}
>> {-# LANGUAGE StandaloneDeriving #-}
>> {-# LANGUAGE TypeFamilies #-}
>> {-# LANGUAGE TypeOperators #-}
>> {-# LANGUAGE UndecidableInstances #-}
>
>what I want is a typeclass with instances of type level Naturals
>
>here's the class, the parameter is of kind (* -> *) i.e. a is some sort
>of wrapper that maps from types to values
>
>> class Foo (a :: * -> *) where
>>   type Bar a
>>   bar :: a (Bar a)
>
>
>lets ignore DataKinds define Zero and Succ as distinct types
>
>uninhabited...but of kind "*" and "k -> *"
>
>> data Z1
>> data S1 nat
>
>SNat1 :: * -> *
>
>> data SNat1 a where
>>   SZ1 :: SNat1 Z1
>>   SS1 :: SNat1 a -> SNat1 (S1 a)
>
>off we go...
>
>> instance Foo SNat1 where
>>   type Bar SNat1 = Z1
>>   bar = SZ1
>
>
>now lets do it the datakind route
>
>> data Nat where
>>   Z :: Nat
>>   S :: Nat -> Nat
>
>ahhh...SNat is of kind "Nat -> *"
>
>> data SNat a where
>>   SZ :: SNat 'Z
>>   SS :: SNat a -> SNat ('S a)
>
>so I cant make it an instance of the same type class
>
>"The first argument of 'Foo' should have kind '* -> *',
>      but 'SNat' has kind 'Nat -> *'
>    In the instance declaration for 'Foo SNat'"
>
>
>> --instance Foo SNat where
>> --  type Bar SNat = 'Z
>> --  bar = SZ
>
>unless I redefine my class (which seems a bit silly)
>
>> class Foo' (a :: k -> *) where
>>   type Bar' a :: k
>>   bar' :: a (Bar' a)
>
>now it works.
>
>> instance Foo' SNat where
>>   type Bar' SNat = 'Z
>>   bar' = SZ
>
>clearly named kinds (?) are somehow distinct from unnames ones?
>CONFIDENTIALITY NOTICE
>
>This e-mail (and any attached files) is confidential and protected by
>copyright (and other intellectual property rights). If you are not the
>intended recipient please e-mail the sender and then delete the email
>and any attached files immediately. Any further use or dissemination is
>prohibited.
>
>While MTV Networks Europe has taken steps to ensure that this email and
>any attachments are virus free, it is your responsibility to ensure
>that this message and any attachments are virus free and do not affect
>your systems / data.
>
>Communicating by email is not 100% secure and carries risks such as
>delay, data corruption, non-delivery, wrongful interception and
>unauthorised amendment. If you communicate with us by e-mail, you
>acknowledge and assume these risks, and you agree to take appropriate
>measures to minimise these risks when e-mailing us.
>
>MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
>Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
>International, Be Viacom, Viacom International Media Networks and VIMN
>and Comedy Central are all trading names of MTV Networks Europe.  MTV
>Networks Europe is a partnership between MTV Networks Europe Inc. and
>Viacom Networks Europe Inc.  Address for service in Great Britain is
>17-29 Hawley Crescent, London, NW1 8TT.
>
>
>------------------------------------------------------------------------
>
>_______________________________________________
>Haskell-Cafe mailing list
>Haskell-Cafe at haskell.org
>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150507/a692e20f/attachment-0001.html>