DataKinds + KindSignatures question
Hello, The following code:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-}
import Data.ByteString
data CmdKind = GET | SET
class Serialize (cmd :: CmdKind) where serialize :: cmd -> ByteString
Results in the following error:
wojtek@wojtek-desktop:~/src/he/snip$ ghc dk.hs [1 of 1] Compiling Main ( dk.hs, dk.o )
dk.hs:9:17: Expected a type, but ‘cmd’ has kind ‘CmdKind’ In the type ‘cmd -> ByteString’ In the class declaration for ‘Serialize’
Is this so by design, or should I write it in a different way, or is it just not implemented? -- Kind regards, Wojtek N.
On Wed, Nov 26, 2014, at 01:17 PM, Wojtek Narczyński wrote:
dk.hs:9:17: Expected a type, but ‘cmd’ has kind ‘CmdKind’ In the type ‘cmd -> ByteString’ In the class declaration for ‘Serialize’
The error message says that it expected a type. That might be a bit confusing. What it means by "type" is "a thing with kind *". That is the kind of types, and those types are the only things which have values. The argument to a function must be a value, so the argument to the "->" operator must be a type. Another example to consider which might make this more clear: Prelude> let { f :: Maybe -> a; f x = undefined } <interactive>:2:12: Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘* -> *’ In the type signature for ‘f’: f :: Maybe -> a Notice that in the type signature for f, I forgot to apply Maybe to an argument. On its own, Maybe has kind * -> *, which means that Maybe is not a type. After all, there is no such thing as a "value of type Maybe".
Is this so by design, or should I write it in a different way, or is it just not implemented?
I don't think it's clear what you are trying to do, so it is hard to say what you should write. -Karl
On 27.11.2014 05:08, Karl Voelker wrote:
The error message says that it expected a type. That might be a bit confusing. What it means by "type" is "a thing with kind *". That is the kind of types, and those types are the only things which have values. The argument to a function must be a value, so the argument to the "->" operator must be a type. But why is it expecting type of kind '*' and rejecting type of kind 'CmdKind'? Functions are limited to work on types of kind '*'?
I don't think it's clear what you are trying to do, so it is hard to say what you should write. I wanted to declare a class for that can only be instantiated for types of certain kind, and then create instances for all that types in a single statement. Basically, I was just trying to understand how kinds and type classes are related. Also, trying to save some typing.
-- Thank you, Wojtek Narczynski
Wojtek Narczyński
Hello,
The following code:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-}
import Data.ByteString
data CmdKind = GET | SET
class Serialize (cmd :: CmdKind) where serialize :: cmd -> ByteString
Results in the following error:
wojtek@wojtek-desktop:~/src/he/snip$ ghc dk.hs [1 of 1] Compiling Main ( dk.hs, dk.o )
dk.hs:9:17: Expected a type, but ‘cmd’ has kind ‘CmdKind’ In the type ‘cmd -> ByteString’ In the class declaration for ‘Serialize’
Is this so by design, or should I write it in a different way, or is it just not implemented?
As Karl explained, type parameters of (->) need to have kind *, whereas your argument cmd has kind CmdKind. A ``workaround'' to this is using Proxy (or any other type that has something of kind CmdKind as (phantom) type). You can then define something like: import Data.Proxy class Serialize (cmd :: CmdKind) where serialize :: Proxy cmd -> ByteString myByteString = serialize (Proxy :: Proxy GET) Depending on what you are trying to do that may be applicable. Regards, -- - Frank
On 27.11.2014 10:06, Frank Staals wrote:
As Karl explained, type parameters of (->) need to have kind *, whereas your argument cmd has kind CmdKind.
Okay, I get it now. I can't have regular functions on types of kind other than '*'. I must stop thinking of '*' as some of wildcard.
A ``workaround'' to this is using Proxy (or any other type that has something of kind CmdKind as (phantom) type). You can then define something like:
import Data.Proxy
class Serialize (cmd :: CmdKind) where serialize :: Proxy cmd -> ByteString
myByteString = serialize (Proxy :: Proxy GET)
Depending on what you are trying to do that may be applicable.
Oh, so Proxy can be understood as a type level function from 'CmdKind' to '*'? -- Kind regards, Wojtek Narczynski
On 27 November 2014 at 21:04, Wojtek Narczyński
On 27.11.2014 10:06, Frank Staals wrote:
As Karl explained, type parameters of (->) need to have kind *, whereas your argument cmd has kind CmdKind.
Okay, I get it now. I can't have regular functions on types of kind other than '*'. I must stop thinking of '*' as some of wildcard.
A ``workaround'' to this is using Proxy (or any other type that has something of kind CmdKind as (phantom) type). You can then define something like:
import Data.Proxy
class Serialize (cmd :: CmdKind) where serialize :: Proxy cmd -> ByteString
myByteString = serialize (Proxy :: Proxy GET)
Depending on what you are trying to do that may be applicable.
Oh, so Proxy can be understood as a type level function from 'CmdKind' to '*'?
Not really: "Proxy CmdKind" is the safer/saner equivalent of doing "(undefined :: CmdKind)" to be able to specify a type. e.g.: show . (`asProxyTypeOf` (Proxy :: Proxy Int)) . read It just brings the type into scope, not any actual values.
-- Kind regards, Wojtek Narczynski
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com
On 27/11/14 12:04, Wojtek Narczyński wrote:
I must stop thinking of '*' as some of wildcard.
Totally.
Oh, so Proxy can be understood as a type level function from 'CmdKind' to '*'?
Sure. In fact, any type constructor can be seen as a (possibly nullary) type function: Prelude> :k Maybe Maybe :: * -> * Maybe is a type function from types (*) to types (*). Prelude Control.Monad.State> :k StateT StateT :: * -> (* -> *) -> * -> * StateT (not to be confused with StateT on the value level that has type (s -> m (a, s)) -> StateT s m a) is a type function of three arguments, two of them of kind * and one of kind (* -> *). Now let's look at Proxy: Prelude Data.Proxy> :k Proxy Proxy :: k -> * Proxy is declared as a kind-polymorphic type (see PolyKinds). Here k is actually a "wildcard" (a kind variable that can be instantiated with any kind). Thus, you can specialize Proxy to be of kind * -> *, or (* -> *) -> *, or MyKind -> *. However, since the type Proxy k has a value (also called Proxy), the return kind of the Proxy type function is necessarily *. You can't build a type function returning a non-* kind using a data or newtype declaration. You can do it, however, using type families. Roman Roman
participants (5)
-
Frank Staals -
Ivan Lazar Miljenovic -
Karl Voelker -
Roman Cheplyaka -
Wojtek Narczyński