Re: Kindness of strangers (or strangeness of Kinds)

2012-06-12 Thread AntC 
Edward Kmett ekmett at gmail.com writes:

 On Mon, Jun 11, 2012 at 9:58 PM, AntC anthony_clayden at clear.net.nz 
wrote:

 [snip ...]

 Could we have :k (-) :: OpenKind - * - *  -- why not?
 
 I don't quite understand why you would want arbitrary kinded arguments, but 
only in negative position. 


Thanks Edward, oops I've used the wrong terminology, sorry for the confusion. 
I didn't mean OpenKind but AnyKind. I put that only in a negative position 
more to sharpen the question, but also because I assumed the result from (-) 
would have to be grounded in Kind *; and then at least one of its arguments 
would also have to be grounded in Kind *.


I think perhaps(?) more PolyKindness is on the horizon: 
http://hackage.haskell.org/trac/ghc/wiki/GhcKinds  (section on GADKs, and sub-
pages on KindPolymorphism and ExplicitTypeApplication). I guess GHC is getting 
there by small steps, and doesn't yet have powerful enough Kind refinement nor 
Kind equality constraints, nor interleaving of Type and Kind inference.



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-11 Thread AntC 
Simon Peyton-Jones simonpj at microsoft.com writes:

 
 There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying 
hard to get rid of it as much as
 possible, and it is much less important than it used to be. It's always been 
there, and is nothing to do with polykinds.
 
 I've extended the commentary a bit: see Types and Kinds here
 http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
 
 The ArgKind thing has gone away following Max's recent unboxed-tuples patch, 
so we now only have OpenKind
 (described on the above pages).
 

Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)

It's not that I have a specific problem (requirement) I'm trying to solve. 
It's more that I'm trying to understand how this ladder of 
Sorts/Kinds/Types/values hangs together.

With Phantom types, we've been familiar for many years with uninhabited types, 
so why are user-defined (promoted) Kinds/Types different?

The Singletons stuff shows there are use cases for mapping from uninhabited 
types to values -- but it seems to need a lot of machinery (all those shadow 
types and values). And indeed TypeRep maps from not-necessarily-inhabited 
types to values.

Is it that we really need to implement type application in the surface 
language to get it all to come together? Then we won't need functions applying 
to dummy arguments whose only purpose is to carry a Type::Kind.

To give a tight example:

data MyNat = Z | S MyNat-- to be promoted

data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat - *

proxyNat :: n - ProxyNat n -- rejected: Kind mis-match
proxyNat _ = ProxyNat

The parallel of that with phantom types (and a class constraint for MyNat) 
seems unproblematic -- albeit with Kind *.

Could we have :k (-) :: OpenKind - * - *  -- why not?


AntC


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-11 Thread Edward Kmett 
On Mon, Jun 11, 2012 at 9:58 PM, AntC anthony_clay...@clear.net.nz wrote:

 Simon Peyton-Jones simonpj at microsoft.com writes:

 
  There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying
 hard to get rid of it as much as
  possible, and it is much less important than it used to be. It's always
 been
 there, and is nothing to do with polykinds.
 
  I've extended the commentary a bit: see Types and Kinds here
  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
 
  The ArgKind thing has gone away following Max's recent unboxed-tuples
 patch,
 so we now only have OpenKind
  (described on the above pages).

 Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)

 It's not that I have a specific problem (requirement) I'm trying to solve.
 It's more that I'm trying to understand how this ladder of
 Sorts/Kinds/Types/values hangs together.

 With Phantom types, we've been familiar for many years with uninhabited
 types,
 so why are user-defined (promoted) Kinds/Types different?

 The Singletons stuff shows there are use cases for mapping from uninhabited
 types to values -- but it seems to need a lot of machinery (all those
 shadow
 types and values). And indeed TypeRep maps from not-necessarily-inhabited
 types to values.

 Is it that we really need to implement type application in the surface
 language to get it all to come together? Then we won't need functions
 applying
 to dummy arguments whose only purpose is to carry a Type::Kind.

 To give a tight example:

data MyNat = Z | S MyNat-- to be promoted

data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat - *

proxyNat :: n - ProxyNat n -- rejected: Kind mis-match
proxyNat _ = ProxyNat

 The parallel of that with phantom types (and a class constraint for MyNat)
 seems unproblematic -- albeit with Kind *.

 Could we have :k (-) :: OpenKind - * - *  -- why not?


I don't quite understand why you would want arbitrary kinded arguments, but
only in negative position.

Internally its already more like (-) :: OpenKind - OpenKind - * at the
moment. The changes simply permitted unboxed tuples in argument position,
relaxing a previous restriction. OpenKind is just a superkind of * and #,
not every kind. Kinds other than * and # just don't have a term level
representation. (Well kind Constraint is inhabited by dictionaries for
instances after a fashion, but you don't get to manipulate them directly.)

I'm a lot happier with the new plumbing than I was with the crap I've been
able to write by hand over the years for natural number types/singletons,
and I'm actually pretty happy with the fact that it makes it clearer that
there is a distinction between the type level and the term level, and I
can't say that I buy the idea of just throwing things open like that.

In particular, the OpenKind for all kinds that you seem to be proposing
sounds more like letting (-) :: forall (a :: BOX?) (b :: BOX?). a - b -
* (or (-) :: forall (a :: BOX?). a - * - *) than OpenKind, which exists
to track where unboxed types can lurk until polymorphism forces it to *.

With the 'more open' OpenKind you propose, it no longer collapses to * when
used in a polymorphic fashion, but merely dumbs down to forall (a :: BOX).
a, which strikes me as a particularly awkward transition. At the least,
you'd need to actually break the 'BOX is the only superkind' rule to
provide the quantification that can span over unboxed types and any boxed
type, (scribbled as BOX? above).

That seems to be a pretty big mess for something that can be solved readily
with simpler tools.

Mind you there is another case for breaking the BOX is the only superkind
rule (that is the horrible syntax hack that requires monomorphization of
the kinds of the results of type/data families can be cleaned up), but once
you have more than one superkind, you start complicating type equality,
needing other coercions, so it really shouldn't be done lightly.

-Edward
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-09 Thread Edward Kmett 
ghci :k Maybe
Maybe :: * - *

On Sat, Jun 9, 2012 at 1:34 AM, Rustom Mody rustompm...@gmail.com wrote:

 On Thu, Jun 7, 2012 at 7:16 AM, AntC anthony_clay...@clear.net.nz wrote:

 I'm confused about something with promoted Kinds (using an example with
 Kind-
 promoted Nats).

 This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already
 explained somewhere


 Is there a way of seeing kinds in ghci?
 [In gofer I could do :s +k -- yeah this was 20 years ago :-) ]


 ___
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Simon Peyton-Jones 
There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying hard 
to get rid of it as much as possible, and it is much less important than it 
used to be. It's always been there, and is nothing to do with polykinds.

I've extended the commentary a bit: see Types and Kinds here
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler

The ArgKind thing has gone away following Max's recent unboxed-tuples patch, so 
we now only have OpenKind (described on the above pages).

Simon

| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of AntC
| Sent: 08 June 2012 00:37
| To: glasgow-haskell-users@haskell.org
| Subject: Re: Kindness of strangers (or strangeness of Kinds)
| 
| José Pedro Magalhães jpm at cs.uu.nl writes:
| 
|  On Thu, Jun 7, 2012 at 2:46 AM, AntC anthony_clayden at
|  clear.net.nz
| wrote:
| 
|  What does the `ArgKind' message mean?
| 
|  `ArgKind` and `OpenKind` is what previously was called `?` and `??`
|  (or the
| otherway around; I can't remember).
| http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Ki
| ndsubty
| ping
| 
| Thanks Pedro, I'm trying to understand what's changing and why. (And I'd
| better repeat that I'm looking at 7.4.1, not HEAD; and SPJ's being
| perfectly clear that the promoted Kind stuff is not yet officially
| approved for prime
| time):
| 
| GHC 7.2.1 :k (-) :: ?? - ? - *
| 
| GHC 7.4.1 :k (-) :: * - * - *
| 
| At first sight (-) is becoming less polyKinded. Is the eventual aim to
| be:
| 
| GHC 7.6+ :k (-) :: AnyKind1 - AnyKind2 - *
| 
| 
| 
| You might also want to have a look at Richard and Stephanie's latest
| paper
| draft, about singletons, which is related to what you are trying in your
| example:http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
| 
| 
| That's what I'm doing, and trying to understand the machinery behind it.
| The
| naieve approach I started with was how to get one-way from type to its
| single
| value -- I wasn't aiming for the whole singleton gig.
| 
| AntC
| 
| 
| 
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Richard Eisenberg 
Yes, I think using a singleton will solve your problem. It essentially 
acts like Proxy but keeps the parallelism between types and terms.


Here would be the definitions:

data Nat = Z | S Nat

-- This is the singleton type
data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: forall (n :: Nat). SNat n - SNat (S n)

class NatToIntN (n :: Nat) where
  natToIntN :: SNat n - Int
instance NatToIntN Z where
  natToIntN _ = 0
instance (NatToIntN n) = NatToIntN (S n) where
  natToIntN (SS n) = 1 + natToIntN n

-
It might be worth noting that there is no need for a class to define 
natToIntN. The following would also work:


natToIntN :: SNat n - Int
natToIntN SZ = 0
natToIntN (SS n) = 1 + natToIntN n


Please do check out our paper for more info at the link Pedro sent out.

Richard

On 6/7/12 8:28 AM, José Pedro Magalhães wrote:

Hi,

On Thu, Jun 7, 2012 at 2:46 AM, AntC anthony_clay...@clear.net.nz 
mailto:anthony_clay...@clear.net.nz wrote:



What does the `ArgKind' message mean?


`ArgKind` and `OpenKind` is what previously was called `?` and `??` 
(or the other

way around; I can't remember).
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubtyping

You might also want to have a look at Richard and Stephanie's latest 
paper draft, about

singletons, which is related to what you are trying in your example:
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf 
http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper.pdf



Cheers,
Pedro



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-08 Thread Rustom Mody 
On Thu, Jun 7, 2012 at 7:16 AM, AntC anthony_clay...@clear.net.nz wrote:

 I'm confused about something with promoted Kinds (using an example with
 Kind-
 promoted Nats).

 This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already
 explained somewhere


Is there a way of seeing kinds in ghci?
[In gofer I could do :s +k -- yeah this was 20 years ago :-) ]
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread José Pedro Magalhães 
Hi,

On Thu, Jun 7, 2012 at 2:46 AM, AntC anthony_clay...@clear.net.nz wrote:


 What does the `ArgKind' message mean?


`ArgKind` and `OpenKind` is what previously was called `?` and `??` (or the
other
way around; I can't remember).
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubtyping

You might also want to have a look at Richard and Stephanie's latest paper
draft, about
singletons, which is related to what you are trying in your example:
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf


Cheers,
Pedro
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread AntC 
José Pedro Magalhães jpm at cs.uu.nl writes:

 On Thu, Jun 7, 2012 at 2:46 AM, AntC anthony_clayden at clear.net.nz 
wrote:
 
 What does the `ArgKind' message mean?
 
 `ArgKind` and `OpenKind` is what previously was called `?` and `??` (or the 
otherway around; I can't remember). 
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubty
ping

Thanks Pedro, I'm trying to understand what's changing and why. (And I'd 
better repeat that I'm looking at 7.4.1, not HEAD; and SPJ's being perfectly 
clear that the promoted Kind stuff is not yet officially approved for prime 
time):

GHC 7.2.1 :k (-) :: ?? - ? - *

GHC 7.4.1 :k (-) :: * - * - *

At first sight (-) is becoming less polyKinded. Is the eventual aim to be:

GHC 7.6+ :k (-) :: AnyKind1 - AnyKind2 - *



You might also want to have a look at Richard and Stephanie's latest paper 
draft, about singletons, which is related to what you are trying in your 
example:http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
 

That's what I'm doing, and trying to understand the machinery behind it. The 
naieve approach I started with was how to get one-way from type to its single 
value -- I wasn't aiming for the whole singleton gig.

AntC



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-07 Thread wagnerdm 

Quoting AntC anthony_clay...@clear.net.nz:


GHC 7.2.1 :k (-) :: ?? - ? - *

GHC 7.4.1 :k (-) :: * - * - *

At first sight (-) is becoming less polyKinded. Is the eventual aim to be:

GHC 7.6+ :k (-) :: AnyKind1 - AnyKind2 - *


I sort of doubt it. After all, the prototypical thing to do with a  
function is to apply it to something, and Haskell expressions are  
categorized by types of OpenKind -- the new kinds you create with the  
new extension don't classify inhabited types.


It looks to me like a - b and (-) a b are just different  
syntactic classes now, not interconvertible with each other:


Prelude GHC.Exts :set -XMagicHash
Prelude GHC.Exts :k Int# - Int#
Int# - Int# :: *
Prelude GHC.Exts :k (-) Int# Int#

interactive:1:6:
Expecting a lifted type, but `Int#' is unlifted
In a type in a GHCi command: (-) Int# Int#

Perhaps this is a side-effect of the introduction of PolyKinds; from  
the release notes:


There is a new feature kind polymorphism (-XPolyKinds): Section  
7.8.1, ?Kind polymorphism?. A side-effect of this is that, when the  
extension is not enabled, in certain circumstances kinds are now  
defaulted to * rather than being inferred.


Though I must say it's not 100% clear to me exactly what's changed, or  
whether it was intentional.

~d

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-06 Thread wagnerdm 

Quoting AntC anthony_clay...@clear.net.nz:


{-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures#-}

data MyNat = Z | S Nat

class NatToIntN (n :: MyNat)
where natToIntN :: (n :: MyNat) - Int
instance NatToIntN Z
where natToIntN _ = 0
instance (NatToIntN n) = NatToIntN (S n)
where natToIntN _ = 1 + natToInt (undefined :: n)

But GHC rejects the class declaration (method's type):
Kind mis-match
 Expected kind `ArgKind', but `n' has kind `MyNat'
(Taking the Kind signature out of the method's type gives same message.)


At a guess, (-) :: * - * - *, but n :: MyNat, not n :: *, so (-) n  
is badly kinded. In comparison:



data Proxy a = Proxy

class NatToInt (n :: MyNat)
where natToInt :: Proxy (n :: MyNat) - Int
instance NatToInt Z
where natToInt _ = 0
instance (NatToInt n) = NatToInt (S n)
where natToInt _ = 1 + natToInt (Proxy :: Proxy n)


Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument  
to hand to (-).


~d

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Kindness of strangers (or strangeness of Kinds)

2012-06-06 Thread AntC 
 wagnerdm at seas.upenn.edu writes:

 
 Quoting AntC anthony_clayden at clear.net.nz:
 
  {-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures#-}
 
  data MyNat = Z | S MyNat
 
  class NatToIntN (n :: MyNat)
  where natToIntN :: (n :: MyNat) - Int
  instance NatToIntN Z
  where natToIntN _ = 0
  instance (NatToIntN n) = NatToIntN (S n)
  where natToIntN _ = 1 + natToInt (undefined :: n)
 
  But GHC rejects the class declaration (method's type):
  Kind mis-match
   Expected kind `ArgKind', but `n' has kind `MyNat'
  (Taking the Kind signature out of the method's type gives same message.)
 
 At a guess, (-) :: * - * - *, but n :: MyNat, not n :: *, so (-) n  
 is badly kinded. In comparison:
 
  data Proxy a = Proxy
 
  class NatToInt (n :: MyNat)
  where natToInt :: Proxy (n :: MyNat) - Int
  instance NatToInt Z
  where natToInt _ = 0
  instance (NatToInt n) = NatToInt (S n)
  where natToInt _ = 1 + natToInt (Proxy :: Proxy n)
 
 Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument  
 to hand to (-).
 
 ~d
 

Thanks for the prompt response, and yes, you're right, so says GHCi:

:k (-) :: * - * - *  -- so `ArgKind` in the message means `*'

:k Proxy :: AnyK - *   -- which answers what is `AnyKind'

So Proxy is a kind-level wormhole: forall k. k - *
Singleton types are a wormhole from types to values.

For the natToInt method, it's a shame having to insert Proxy's everywhere -- 
it takes away from the parallel to value-level equations.

Perhaps I need promoted GADT's?

Or perhaps PolyKinded (-) :: k1 - k2 - k3?

AntC


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users