Hello,
Maybe this is well known already (or maybe it's a bug), but lately I've
again found that functional
dependencies are more versatile than type families. In particular, they can
be used to compute
kinds from types, whereas type families cannot. Consider the code below,
which implements
On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães j...@cs.uu.nl wrote:
The most interesting part here is the functional dependency fs - k, where k
is a kind variable!
If this is not a bug (and it does seem to work as I expect it to), then could
we have type families
return kinds too
When we discussed this last time (summarized by the link Pedro sent, I
think) it came up that it might be nice to also
have kind synonyms, which would be analogous to type synonyms, but one
level up. The natural syntax for that would be to have a type kind
declaration, but this seems a bit
On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson r...@soi.city.ac.uk wrote:
GHC implements data kinds by promoting data declarations of a certain
restricted form, but I wonder if it would be better to have a special
syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
, Jan 25, 2013 at 7:19 AM, Ross Paterson r...@soi.city.ac.ukwrote:
GHC implements data kinds by promoting data declarations of a certain
restricted form, but I wonder if it would be better to have a special
syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
This is exactly
GHC implements data kinds by promoting data declarations of a certain
restricted form, but I wonder if it would be better to have a special
syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
At the moment, things get promoted whether you need them or not, and
if you've made some
See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData
Cheers,
Pedro
On Fri, Jan 25, 2013 at 3:19 PM, Ross Paterson r...@soi.city.ac.uk wrote:
GHC implements data kinds by promoting data declarations of a certain
restricted form, but I wonder if it would be better to have
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.
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
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
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
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
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
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).
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
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
Hi Richard,
I've had a look at the updated proposal page; it looks fine to me. I don't
really have a preference between the standard and alternative
implementations right now.
You do mention parse errors with kinds and promoted constructors (which is
related to http://hackage.haskell.org/trac
at 03:09, Richard Eisenberg e...@seas.upenn.edu wrote:
Hi all,
I'm working on bringing Template Haskell up to speed with the new
extensions for polymorphic kinds and promoted data kinds. This requires a
few small, non-breaking changes to TH datatypes. I've made a (short) wiki
page at http
://hackage.haskell.org/trac/ghc/wiki/TemplateHaskellRichKinds
In my continued experiments with this, I've realized that we will need
even more constructors to make all the different kinds expressible. The
Wiki page is updated for this also, and I've listed two alternative
implementations. Comments
Hi all,
I'm working on bringing Template Haskell up to speed with the new
extensions for polymorphic kinds and promoted data kinds. This requires
a few small, non-breaking changes to TH datatypes. I've made a (short)
wiki page at
http://hackage.haskell.org/trac/ghc/wiki
On Tue, Jan 10, 2012 at 09:41:11PM +0400, Serge D. Mechveliani wrote:
People,
GHC provides some extensions for kinds.
Does this make possible different kinds, for example, for `*' ?
Terms have types, and types have kinds. (*) is a term, so it has a
type, not a kind.
Prelude.Num has
People,
GHC provides some extensions for kinds.
Does this make possible different kinds, for example, for `*' ?
Prelude.Num has * :: a - a - a.
And mathematicians also like to denote as `*'
(\cdot in TeX)
a multiplication of a vector v by a coefficient r. It is expressed by the
declaration
Hi Ian,
thanks for your feedback.
I should have taken more care.
change line 198
let (tokenLines :: [[Token]]) =
to
let tokenLines
May I ask you to (amend-)record it?
I don't mind wether darcs lists me as author of this tiny minor fix.
Or is it easier for you to apply another
Now there is
http://mawercer.de/hasktags_patch3
(fixed exhausted pattern match when processing literate haskell files)
No aborts while tagging the core libraries, some extra libraries and
HAppS libs. (45 packages tested)
___
Glasgow-haskell-users
Hi Simon,
thanks for pointing me to the ticket (therby telling me that hasktags
was not really usable before ?). The ticket can be marked as fixed now I
hope.
I've tried enhancing it but I don't know wether it still finds
everyting in all cases. So more testing is needed.
I've included a small
: [EMAIL PROTECTED]
[mailto:glasgow-haskell-users-
| [EMAIL PROTECTED] On Behalf Of Geoffrey Alan Washburn
| Sent: 06 August 2005 15:18
| To: glasgow-haskell-users@haskell.org
| Subject: Inductive kinds
|
|
| Are there any plans for inductively defined kinds in some future
| version of GHC
Simon Peyton-Jones wrote:
You mean something like 'datakind' in Tim Sheard's Omega?
Essentially.
Nothing is imminent. What I'd like to do, though, is to use data
*types* at the type level, rather than reproduce the data-type
declaration stuff at the kind level. Thus
data Nat =
Are there any plans for inductively defined kinds in some future
version of GHC?
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
February 2005 12:31
| To: glasgow-haskell-users@haskell.org
| Subject: Kinds in ghc
|
| Hi
|
| I can report success on compiling latest CVS on Mac OS X including
| stage 2 with ghci support. (greencard does not compile, but that's not
| a problem for ghc to be compiled it seems.)
|
| Now that I
Hi
I can report success on compiling latest CVS on Mac OS X including
stage 2 with ghci support. (greencard does not compile, but that's not
a problem for ghc to be compiled it seems.)
Now that I have the compiler up, I notice that types are not reported
as before. Instead of nice t,t', etc, I
| type Kind = Type
|
| What does this mean?
It means that Kinds are represented by Types.
Admittedly, Kinds only use a small fragment of what Types can represent,
namely Arrow, and type constructor applications. So * is represented by
a TyConApp with a TyCon that is called typeCon.
The really
Hello,
It means that Kinds are represented by Types.
Admittedly, Kinds only use a small fragment of what Types can represent,
namely Arrow, and type constructor applications. So * is represented by
a TyConApp with a TyCon that is called typeCon.
The really annoying thing about Kinds
Hello again,
I have browsed the GHC commentary and I could not find
a lot of information about kinds. But kinds are very
important for my implementation! The parser seems to
call liftedTypeKind from TypeRep. But in TypeRep we
have
type Kind = Type
What does this mean?
I briefly explain
On Tuesday 05 August 2003 4:00 pm, Simon Peyton-Jones wrote:
| id# :: (a :: # ) - a
| id# x = x
That should really be rejected. You couldn't call it because you'd have
to instantiate 'a' to Int# or Double#, and that would mean different
code for different calls.
GHC (after modifying the
function is
ever effectively applied to an unboxed value. Does this mean that
forcing kinds to # will not work, for example as in
id# :: (a :: # ) - a
id# x = x
? For some reason GHC does not produce any code for this
definition, although it seems to be able to inline it and simplify it
away
| All right. I do expect the compiler to yell if a polymorphic function
is
| ever effectively applied to an unboxed value. Does this mean that
| forcing kinds to # will not work, for example as in
| id# :: (a :: # ) - a
| id# x = x
That should really be rejected. You couldn't call it because
-notation, but it seems a bit ad
hoc.
Simon
| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED]
| On Behalf Of Sebastien Carlier
| Sent: 04 August 2003 16:09
| To: [EMAIL PROTECTED]
| Subject: Polymorphic kinds
|
|
| Hello,
|
| I am experimenting with GHC
illustrates the problem:
{-# OPTIONS -fglasgow-exts #-}
import GHC.Prim
x :: IO Int#
x =
return 1#
GHC (HEAD from 2003-08-01) reports:
T.lhs:5:
Kind error: Expecting a lifted type, but `Int#' is unlifted
When checking kinds in `IO Int#'
In the type: IO Int#
While checking
The ultimate goal is to write a
prototype operating system in Haskell, using the GHC RTS as a kind of
microkernel
As a useful stepping stone towards that goal, you might look at Utah's OSKit:
http://www.cs.utah.edu/flux/oskit/
It gives you a bunch of useful bits like bootloaders, device
b) = Traversable (a b) where ..
Because of the obvious kind errors. What I suppose I need is some sort of
lambda expansion over kinds, so I could say:
instance (Traversable a, Traversable b) = Traversable (\x - a b x)
or something like that.
Obviously this doesn't exist.
How can I get around
kind errors. What I suppose I need is some sort of
lambda expansion over kinds, so I could say:
instance (Traversable a, Traversable b) = Traversable (\x - a b x)
or something like that.
Obviously this doesn't exist.
How can I get around this?
- Hal
--
Hal Daume III
Computer
At 2002-01-18 13:10, Hal Daume III wrote:
Now, I want to say that if some data type 'd' is Traversable and another
data type 'e' is Traversable, then the combined data type is
Traversable. That is, for example, I want to say that a Tree of Lists is
traversable, or that a List of Trees, or a
46 matches
Mail list logo
