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.
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
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
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
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
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
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
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).
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).
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
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 -- I know 7.4.1 is relatively experimental. I have
searched the bug tracs and discussions I could find.)
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
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
13 matches
Mail list logo
