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

6 May 2015

      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"  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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

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

Ben