A question on datakinds syntax

Hi, I am reading the document of spock-0.11, and found two strange definitions in the Web.Spock. ```` type Var a = Path ((:) * a ([] *)) Open var :: (Typeable * a, PathPiece a) => Path ((:) * a ([] *)) Open ```` What's the meaning of the star between Typeable and a ? The kind of Typeable is * -> *. I cannot understand why the Typeable in the var prototype takes two kinds. In the Web.Routing.Combinators of reroute-0.4, those are defined as following: ```` type Var a = Path (a ': '[]) Open var :: (Typeable a, PathPiece a) => Path (a ': '[]) Open ```` Why there are two difference definition about the same thing? Thanks, Haiwei

Haddock displays kind annotations oddly. At a guess (which could well be
off base; I'm still rather weak on this stuff), Spock has PolyKinds
enabled, so an explicit (x :: *) kind annotation must be preserved as an
override to the default of allowing any kind; if PolyKinds is not enabled,
then * is the default kind and wouldn't be annotated. (Reader beware: * is
not a wildcard/"match any", it is specifically the kind of inhabited boxed
types!)
On Fri, Jan 13, 2017 at 3:31 AM, Haiwei Zhou
Hi,
I am reading the document of spock-0.11, and found two strange definitions in the Web.Spock.
```` type Var a = Path ((:) * a ([] *)) Open
var :: (Typeable * a, PathPiece a) => Path ((:) * a ([] *)) Open
````
What's the meaning of the star between Typeable and a ?
The kind of Typeable is * -> *. I cannot understand why the Typeable in the var prototype takes two kinds.
In the Web.Routing.Combinators of reroute-0.4, those are defined as following:
```` type Var a = Path (a ': '[]) Open
var :: (Typeable a, PathPiece a) => Path (a ': '[]) Open
````
Why there are two difference definition about the same thing?
Thanks, Haiwei
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Haddock struggles sometimes to render types with -XPolyKinds enabled. The problem is that GHC generally does not require kind arguments to be written and it does not print them out (unless you say -fprint-explicit-kinds). But Haddock, I believe, prints out kinds whenever -XPolyKinds is on. So the two different definitions are really the same: it's just that one module has -XPolyKinds and the other doesn't. The * is the kind of ordinary types. So Int has kind * (we write Int :: *) while Maybe has kind * -> *. Typeable actually has kind `forall k. k -> Constraint`, meaning that it's polykinded. In the first snippet below, the * argument to Typeable instantiates k with *, because type variable a has kind *. This all tends to be quite confusing, and I wish I could point you to a tutorial or some such on it all... but I don't know if one exists! I hope this is helpful, Richard
On Jan 13, 2017, at 1:31 AM, Haiwei Zhou
wrote: Hi,
I am reading the document of spock-0.11, and found two strange definitions in the Web.Spock.
```` type Var a = Path ((:) * a ([] *)) Open
var :: (Typeable * a, PathPiece a) => Path ((:) * a ([] *)) Open
````
What's the meaning of the star between Typeable and a ?
The kind of Typeable is * -> *. I cannot understand why the Typeable in the var prototype takes two kinds.
In the Web.Routing.Combinators of reroute-0.4, those are defined as following:
```` type Var a = Path (a ': '[]) Open
var :: (Typeable a, PathPiece a) => Path (a ': '[]) Open
````
Why there are two difference definition about the same thing?
Thanks, Haiwei _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
Brandon Allbery
-
Haiwei Zhou
-
Richard Eisenberg