RE: ANNOUNCE: GHC 7.6.1 Release Candidate 1
Sorry I am a bit late to this: it appears to work fine on all my platforms: el5, el6, fc16, fc17 (justhub.org/catalogue). I haven't tested it thoroughly yet. Chris ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 7.6.1 Release Candidate 1
hscolour also fails to build out of the box.This is the Prelude.catch issue.Regards, Malcolm ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 7.6.1 Release Candidate 1
Ian Lynagh wrote: We are pleased to announce the first release candidate for GHC 7.6.1: http://www.haskell.org/ghc/dist/7.6.1-rc1/ This includes the source tarball, installers for 32bit and 64bit Windows, and bindists for amd64/Linux, i386/Linux, amd64/OSX and i386/OSX. Please test as much as possible; bugs are much cheaper if we find them before the release! On PowerPc I get this: compiler/nativeGen/X86/Regs.hs:61:1: Warning: The import of `CmmCallConv' is redundant except perhaps to import instances from `CmmCallConv' To import instances alone, use: import CmmCallConv() which in HEAD was fixed by the application of this patch: commit 2f7c578574a9d5e9b4d95847abc3d1cb1b35336d Author: Erik de Castro Lopo er...@mega-nerd.com Date: Wed Aug 8 06:44:00 2012 +1000 Cheers, Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I tried this with the release candidate. I can go pull a more recent
version and try again.
On Thu, Aug 30, 2012 at 11:04 PM, Richard Eisenberg e...@cis.upenn.eduwrote:
This looks related to bug #7128. In the response to that (fixed, closed)
bug report, Simon PJ said that functional dependencies involving kinds are
supported. Are you compiling with a version of 7.6 updated since that bug
fix?
Richard
On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:
If I define the following
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where
class IMonad (m :: (k - *) - k - *) where
ireturn :: a x - m a x
infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
instance IMonad Thrist where
ireturn a = a :- Nil
Then 'ireturn' complains (correctly) that it can't match the k with the
kind (i,i). The reason it can't is because when you look at the resulting
signature for the MPTC it generates it looks like
class IMonad k m where
ireturn :: a x - m a x
However, there doesn't appear to be a way to say that the kind k should be
determined by m.
I tried doing:
class IMonad (m :: (k - *) - k - *) | m - k where
ireturn :: a x - m a x
Surprisingly (to me) this compiles and generates the correct constraints
for IMonad:
ghci :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
-XDataKinds -XGADTs
ghci class IMonad (m :: (k - *) - k - *) | m - k where ireturn :: a x
- m a x
ghci :info IMonad
class IMonad k m | m - k where
ireturn :: a x - m a x
But when I add
ghci :{
Prelude| data Thrist :: ((i,i) - *) - (i,i) - * where
Prelude| Nil :: Thrist a '(i,i)
Prelude| (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
Prelude| :}
and attempt to introduce the instance, I crash:
ghci instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
(GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Moreover, attempting to compile them in separate modules leads to a
different issue.
Within the module, IMonad has a type that includes the kind k and the
constraint on it from m. But from the other module, :info shows no such
constraint, and the above code again fails to typecheck, but upon trying to
recompile, when GHC goes to load the IMonad instance from the core file, it
panicks again differently about references to a variable not present in the
core.
Is there any way to make such a constraint that determines a kind from a
type parameter in GHC 7.6 at this time?
I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
applicable to this situation.
-Edward
___
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: Small Int and Char closures in GHCi
On 30/08/2012 12:29, Joachim Breitner wrote: Hi, I am preparing a talk about the details of how data and programs look in memory in Haskell (well, GHC). When explaining the memory consumption of a large String, I wanted to show the effect of short-int-replacement that happens in http://hackage.haskell.org/trac/ghc/browser/rts/sm/Evac.c#L550 I use my ghc-heap-view-package to observe the heap. This programs shows the effect: import GHC.HeapView import System.Mem main = do let hallo = hallo mapM_ (\x - putStrLn $ show x ++ : ++ show (asBox x)) hallo performGC mapM_ (\x - putStrLn $ show x ++ : ++ show (asBox x)) hallo gives, as expected: $ ./SmallChar 'h': 0x7f2811e042a8/1 'a': 0x7f2811e08128/1 'l': 0x7f2811e09ef0/1 'l': 0x7f2811e0bcd8/1 'o': 0x7f2811e0db10/1 'h': 0x006d9bd0/1 'a': 0x006d9b60/1 'l': 0x006d9c10/1 'l': 0x006d9c10/1 'o': 0x006d9c40/1 but in GHCi, it does not work: $ runhaskell SmallChar.hs 'h': 0x7f5334623d58/1 'a': 0x7f5334626208/1 'l': 0x7f5334627fc0/1 'l': 0x7f5334629dc0/1 'o': 0x7f533462bba8/1 'h': 0x7f533381a1c8/1 'a': 0x7f5333672e30/1 'l': 0x7f533381a408/1 'l': 0x7f533381a6b8/1 'o': 0x7f533389c5d0/1 Note that the GC does evacuate the closures, as the pointers change. Why are these not replaced by the static ones here? Probably because GHCi has a dynamically loaded copy of the base package, so the pointer comparisons that the GC is doing do not match the dynamically-loaded I# and C# constructors. Cheers, Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Hrmm. This seems to render product kinds rather useless, as there is no way
to refine the code to reflect the knowledge that they are inhabited by a
single constructor. =(
For instance, there doesn't even seem to be a way to make the following
code compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist example)
so I'm wondering where the impedence mismatch comes in and how to gain
knowledge of this injectivity to make it work.
Also, does it ever make sense for the kind of a kind variable mentioned in
a type not to get a functional dependency on the type?
e.g. should
class Foo (m :: k - *)
always be
class Foo (m :: k - *) | m - k
?
Honest question. I can't come up with a scenario, but you might have one I
don't know.
-Edward
On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones
simo...@microsoft.comwrote:
With the code below, I get this error message with HEAD. And that looks
right to me, no?
The current 7.6 branch gives the same message printed less prettily.
** **
If I replace the defn of irt with
irt :: a '(i,j) - Thrist a '(i,j)
irt ax = ax :- Nil
** **
then it typechecks.
** **
Simon
** **
** **
Knett.hs:20:10:
Couldn't match type `x' with '(i0, k0)
`x' is a rigid type variable bound by
the type signature for irt :: a x - Thrist k a x at
Knett.hs:19:8
Expected type: Thrist k a x
Actual type: Thrist k a '(i0, k0)
In the expression: ax :- Nil
In an equation for `irt': irt ax = ax :- Nil
simonpj@cam-05-unx:~/tmp$
** **
** **
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
** **
module Knett where
** **
class IMonad (m :: (k - *) - k - *) | m - k where
ireturn :: a x - m a x
** **
infixr 5 :-
** **
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
** **
-- instance IMonad Thrist where
-- ireturn a = a :- Nil
** **
irt :: a x - Thrist a x
irt ax = ax :- Nil
** **
** **
*From:* glasgow-haskell-users-boun...@haskell.org [mailto:
glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
*Sent:* 31 August 2012 03:38
*To:* glasgow-haskell-users@haskell.org
*Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
functional dependency?
** **
If I define the following
** **
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}*
***
module Indexed.Test where
** **
class IMonad (m :: (k - *) - k - *) where
ireturn :: a x - m a x
** **
infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
** **
instance IMonad Thrist where
ireturn a = a :- Nil
** **
Then 'ireturn' complains (correctly) that it can't match the k with the
kind (i,i). The reason it can't is because when you look at the resulting
signature for the MPTC it generates it looks like
** **
class IMonad k m where
ireturn :: a x - m a x
** **
However, there doesn't appear to be a way to say that the kind k should be
determined by m.
** **
I tried doing:
** **
class IMonad (m :: (k - *) - k - *) | m - k where
ireturn :: a x - m a x
** **
Surprisingly (to me) this compiles and generates the correct constraints
for IMonad:
** **
ghci :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
-XDataKinds -XGADTs
ghci class IMonad (m :: (k - *) - k - *) | m - k where ireturn :: a x
- m a x
ghci :info IMonad
class IMonad k m | m - k where
ireturn :: a x - m a x
** **
But when I add
** **
ghci :{
Prelude| data Thrist :: ((i,i) - *) - (i,i) - * where
Prelude| Nil :: Thrist a '(i,i)
Prelude| (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
Prelude| :}
** **
and attempt to introduce the instance, I crash:
** **
ghci instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
(GHC
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
This works, though it'll be all sorts of fun to try to scale up.
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
TypeFamilies #-}
module Indexed.Test where
class IMonad (m :: (k - *) - k - *) | m - k
where ireturn :: a x - m a x
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) = a ij -
Thrist a jk - Thrist a ik
instance IMonad Thrist where
ireturn a = a :- Nil
I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less
painful.
On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett ekm...@gmail.com wrote:
Hrmm. This seems to work manually for getting product categories to work.
Perhaps I can do the same thing for thrists.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x (Fst a) (Fst b) - y (Snd a) (Snd b) - (x * y) a b
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett ekm...@gmail.com wrote:
Hrmm. This seems to render product kinds rather useless, as there is no
way to refine the code to reflect the knowledge that they are inhabited by
a single constructor. =(
For instance, there doesn't even seem to be a way to make the following
code compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist
example) so I'm wondering where the impedence mismatch comes in and how to
gain knowledge of this injectivity to make it work.
Also, does it ever make sense for the kind of a kind variable mentioned
in a type not to get a functional dependency on the type?
e.g. should
class Foo (m :: k - *)
always be
class Foo (m :: k - *) | m - k
?
Honest question. I can't come up with a scenario, but you might have one
I don't know.
-Edward
On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
With the code below, I get this error message with HEAD. And that
looks right to me, no?
The current 7.6 branch gives the same message printed less prettily.
** **
If I replace the defn of irt with
irt :: a '(i,j) - Thrist a '(i,j)
irt ax = ax :- Nil
** **
then it typechecks.
** **
Simon
** **
** **
Knett.hs:20:10:
Couldn't match type `x' with '(i0, k0)
`x' is a rigid type variable bound by
the type signature for irt :: a x - Thrist k a x at
Knett.hs:19:8
Expected type: Thrist k a x
Actual type: Thrist k a '(i0, k0)
In the expression: ax :- Nil
In an equation for `irt': irt ax = ax :- Nil
simonpj@cam-05-unx:~/tmp$
** **
** **
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds, **
**
FlexibleInstances, UndecidableInstances #-}
** **
module Knett where
** **
class IMonad (m :: (k - *) - k - *) | m - k where
ireturn :: a x - m a x
** **
infixr 5 :-
** **
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
** **
-- instance IMonad Thrist where
-- ireturn a = a :- Nil
** **
irt :: a x - Thrist a x
irt ax = ax :- Nil
** **
** **
*From:* glasgow-haskell-users-boun...@haskell.org [mailto:
glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
*Sent:* 31 August 2012 03:38
*To:* glasgow-haskell-users@haskell.org
*Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
functional dependency?
** **
If I define the following
** **
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses,
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Fri, Aug 31, 2012 at 9:06 AM, Edward Kmett ekm...@gmail.com wrote:
I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less
painful.
To flesh this out slightly, there are two options for defining pairs in Agda:
data Pair1 (A B : Set) : Set where
_,_ : A - B - Pair1 A B
record Pair2 (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
Now, if we have something similar to Thrist indexed by Pair2, we have
no problems, because:
A p - M A p
is equal to:
A (fst p , snd p) - M A (fst p , snd p)
Which is what we need for the irt definition to make sense. If we
index by Pair1, this won't happen automatically, but we have an
alternate definition of irt:
irt : {I J : Set} {A : Pair1 I J - Set} {p : Pair1 I J} - A p -
Thrist A p
irt {I} {J} {A} {i , j} ap = ap :- Nil
The pattern match {i , j} there refines p to be (i , j) everywhere, so
the definition is justified.
Without one of these two options, these definitions seem like they're
going to be cumbersome. Ed seems to have found a way to do it, by what
looks kind of like hand implementing the record version, but it looks
unpleasant.
On another note, it confuses me that m - k would be necessary at all
in the IMonad definition. k is automatically determined by being part
of the kind of m, and filling in anything else for k would be a type
error, no? It is the same kind of reasoning that goes on in
determining what 'a' is for 'id :: forall a. a - a' based on the type
of the first argument.
-- Dan
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I ran into this same issue in my own experimentation: if a type variable x has
a kind with only one constructor K, GHC does not supply the equality x ~ K y
for some fresh type variable y. Perhaps it should. I too had to use similar
workarounds to what you have come up with.
One potential problem is the existence of the Any type, which inhabits every
kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an
inconsistent coercion (equating two types with distinct ground head types).
However, because the RHS is a promoted datatype, we know that this coercion can
never be applied to a term. Because equality is homogeneous (i.e. ~ can relate
only two types of the same kind), I'm not convinced the existence of Any ~ K y
is so bad. (Even with heterogeneous equality, it might work out, given that
there is more than one type constructor that results in *...)
Regarding the m - k fundep: my experiments suggest that this dependency is
implied when you have (m :: k), but I guess not when you have k appear in the
kind of m in a more complicated way. Currently, there are no kind-level
functions, so it appears that m - k could be implied whenever k appears
anywhere in the kind of m. If (when!) there are kind-level functions, we'll
have to be more careful.
Richard
On Aug 31, 2012, at 9:06 AM, Edward Kmett wrote:
This works, though it'll be all sorts of fun to try to scale up.
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
TypeFamilies #-}
module Indexed.Test where
class IMonad (m :: (k - *) - k - *) | m - k
where ireturn :: a x - m a x
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) = a ij -
Thrist a jk - Thrist a ik
instance IMonad Thrist where
ireturn a = a :- Nil
I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less painful.
On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett ekm...@gmail.com wrote:
Hrmm. This seems to work manually for getting product categories to work.
Perhaps I can do the same thing for thrists.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x (Fst a) (Fst b) - y (Snd a) (Snd b) - (x * y) a b
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett ekm...@gmail.com wrote:
Hrmm. This seems to render product kinds rather useless, as there is no way
to refine the code to reflect the knowledge that they are inhabited by a
single constructor. =(
For instance, there doesn't even seem to be a way to make the following code
compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist example) so
I'm wondering where the impedence mismatch comes in and how to gain knowledge
of this injectivity to make it work.
Also, does it ever make sense for the kind of a kind variable mentioned in a
type not to get a functional dependency on the type?
e.g. should
class Foo (m :: k - *)
always be
class Foo (m :: k - *) | m - k
?
Honest question. I can't come up with a scenario, but you might have one I
don't know.
-Edward
On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones simo...@microsoft.com
wrote:
With the code below, I get this error message with HEAD. And that looks right
to me, no?
The current 7.6 branch gives the same message printed less prettily.
If I replace the defn of irt with
irt :: a '(i,j) - Thrist a '(i,j)
irt ax = ax :- Nil
then it typechecks.
Simon
Knett.hs:20:10:
Couldn't match type `x' with '(i0, k0)
`x' is a rigid type variable bound by
the type signature for irt :: a x - Thrist k a x at
Re: Small Int and Char closures in GHCi
Hi,
Am Freitag, den 31.08.2012, 13:14 +0100 schrieb Simon Marlow:
Note that the GC does evacuate the closures, as the pointers change. Why
are these not replaced by the static ones here?
Probably because GHCi has a dynamically loaded copy of the base package,
so the pointer comparisons that the GC is doing do not match the
dynamically-loaded I# and C# constructors.
could be; I could not find a way to verify it. I tried comparing the
info pointers of a 1::Int that I generated in ghci and one that comes
from a statically compiled module loaded into ghci, but that is probably
also linked against GHHi’s dynamically loaded base.
But if it is really the case that the RTS has different copies of base,
wouldn’t code like this then break?
if (i == stg_TSO_info
|| i == stg_WHITEHOLE_info
|| i == stg_BLOCKING_QUEUE_CLEAN_info
|| i == stg_BLOCKING_QUEUE_DIRTY_info) {
copy(p,info,q,sizeofW(StgInd),gen_no);
return;
}
(http://hackage.haskell.org/trac/ghc/browser/rts/sm/Evac.c#L635)
Or is it, by accident or careful design, the case that all the instances
where the RTS compares info pointers with well known pointers are not
relevant when running in GHCi?
Thanks,
Joachim
--
Joachim nomeata Breitner
m...@joachim-breitner.de | nome...@debian.org | GPG: 0x4743206C
xmpp: nome...@joachim-breitner.de | http://www.joachim-breitner.de/
signature.asc
Description: This is a digitally signed message part
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg e...@cis.upenn.eduwrote: I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with. One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...) I think it may have to. Working the example further runs into a similar problem. When you go to implement indexed bind, there isn't a way to convince GHC that (Snd ij ~ i, Fst ij ~ j) entails (ij ~ '(i,j)) I'm working around it (for now) with unsafeCoerce. :-( But it with an explicitly introduced equality this code would just work, like it does in other platforms. https://github.com/ekmett/indexed/blob/master/src/Indexed/Thrist.hs#L21 Regarding the m - k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m - k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Hrmm. This seems to render product kinds rather useless, as there is no way to
refine the code to reflect the knowledge that they are inhabited by a single
constructor. =(
Wait. When you say “This seems to render produce kinds useless”, are you saying
that in the code I wrote, you think irt should compile?? I reproduce it below
for completeness.
Simon
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Knett where
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
irt :: a x - Thrist a x
irt ax = ax :- Nil
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Same question. Do you expect the code below to type-check? I have stripped it
down to essentials. Currently it’s rejected with
Couldn't match type `a' with '(,) k k1 b0 d0
And that seems reasonable, doesn’t it? After all, in the defn of bidStar, (:*)
returns a value of type
Star x y ‘(a,c) ‘(b,d)
which is manifestly incompatible with the claimed, more polymorphic type. And
this is precisely the same error as comes from your class/instance example
below, and for precisely the same reason.
I must be confused.
Simon
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
data Star :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x a b - y c d - Star x y '(a,c) '(b,d)
bidStar :: Star T T a a
bidStar = bidT :* bidT
data T a b = MkT
bidT :: T a a
bidT = MkT
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
dependency?
Hrmm. This seems to render product kinds rather useless, as there is no way to
refine the code to reflect the knowledge that they are inhabited by a single
constructor. =(
For instance, there doesn't even seem to be a way to make the following code
compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist example) so
I'm wondering where the impedence mismatch comes in and how to gain knowledge
of this injectivity to make it work.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
It is both perfectly reasonable and unfortunately useless. :(
The problem is that the more polymorphic type isn't any more polymorphic,
since (ideally) the product kind (a,b) is only inhabited by things of the
form '(x,y).
The product kind has a single constructor. But there is no way to express
this at present that is safe.
As it stands, I can fake this to an extent in one direction, by writing
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Kmett where
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
a ij - Thrist a '(j,k) - Thrist a ik
irt :: a x - Thrist a x
irt ax = ax :- Nil
and this compiles, but it just pushes the problem down the road, because
with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
ij, Snd ij) :: (x,y)
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
when you go to define an indexed bind, and type families are insufficient
to the task. Right now to get this property I'm forced to fake it with
unsafeCoerce.
-Edward
On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:
Same question. Do you expect the code below to type-check? I have
stripped it down to essentials. Currently it’s rejected with
** **
Couldn't match type `a' with '(,) k k1 b0 d0
** **
And that seems reasonable, doesn’t it? After all, in the defn of bidStar,
(:*) returns a value of type
Star x y ‘(a,c) ‘(b,d)
which is manifestly incompatible with the claimed, more polymorphic type.
And this is precisely the same error as comes from your class/instance
example below, and for precisely the same reason.
** **
I must be confused.
** **
Simon
** **
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
** **
data Star :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where**
**
(:*) :: x a b - y c d - Star x y '(a,c) '(b,d)
** **
bidStar :: Star T T a a
bidStar = bidT :* bidT
** **
data T a b = MkT
** **
bidT :: T a a
bidT = MkT
** **
** **
** **
*From:* Edward Kmett [mailto:ekm...@gmail.com]
*Sent:* 31 August 2012 13:45
*To:* Simon Peyton-Jones
*Cc:* glasgow-haskell-users@haskell.org
*Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
functional dependency?
** **
Hrmm. This seems to render product kinds rather useless, as there is no
way to refine the code to reflect the knowledge that they are inhabited by
a single constructor. =(
** **
For instance, there doesn't even seem to be a way to make the following
code compile, either.
** **
** **
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
** **
import Prelude hiding (id,(.))
** **
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
** **
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where***
*
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
** **
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
** **
This all works perfectly fine in Conor's SHE, (as does the thrist example)
so I'm wondering where the impedence mismatch comes in and how to gain
knowledge of this injectivity to make it work.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Also, even after upgrading to HEAD, I'm getting a number of errors like:
[2 of 8] Compiling Indexed.Functor ( src/Indexed/Functor.hs,
dist/build/Indexed/Functor.o )
ghc: panic! (the 'impossible' happened)
(GHC version 7.7.20120830 for x86_64-apple-darwin):
tc_fd_tyvar
k{tv aZ8}
k{tv l} [sig]
ghc-prim:GHC.Prim.BOX{(w) tc 347}
I'll try to distill this down to a reasonable test case.
-Edward
On Fri, Aug 31, 2012 at 1:26 PM, Edward Kmett ekm...@gmail.com wrote:
It is both perfectly reasonable and unfortunately useless. :(
The problem is that the more polymorphic type isn't any more
polymorphic, since (ideally) the product kind (a,b) is only inhabited by
things of the form '(x,y).
The product kind has a single constructor. But there is no way to express
this at present that is safe.
As it stands, I can fake this to an extent in one direction, by writing
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Kmett where
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
a ij - Thrist a '(j,k) - Thrist a ik
irt :: a x - Thrist a x
irt ax = ax :- Nil
and this compiles, but it just pushes the problem down the road, because
with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
ij, Snd ij) :: (x,y)
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
when you go to define an indexed bind, and type families are insufficient
to the task. Right now to get this property I'm forced to fake it with
unsafeCoerce.
-Edward
On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones simo...@microsoft.com
wrote:
Same question. Do you expect the code below to type-check? I have
stripped it down to essentials. Currently it’s rejected with
** **
Couldn't match type `a' with '(,) k k1 b0 d0
** **
And that seems reasonable, doesn’t it? After all, in the defn of
bidStar, (:*) returns a value of type
Star x y ‘(a,c) ‘(b,d)
which is manifestly incompatible with the claimed, more polymorphic
type. And this is precisely the same error as comes from your
class/instance example below, and for precisely the same reason.
** **
I must be confused.
** **
Simon
** **
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
** **
data Star :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where*
***
(:*) :: x a b - y c d - Star x y '(a,c) '(b,d)
** **
bidStar :: Star T T a a
bidStar = bidT :* bidT
** **
data T a b = MkT
** **
bidT :: T a a
bidT = MkT
** **
** **
** **
*From:* Edward Kmett [mailto:ekm...@gmail.com]
*Sent:* 31 August 2012 13:45
*To:* Simon Peyton-Jones
*Cc:* glasgow-haskell-users@haskell.org
*Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
functional dependency?
** **
Hrmm. This seems to render product kinds rather useless, as there is no
way to refine the code to reflect the knowledge that they are inhabited by
a single constructor. =(
** **
For instance, there doesn't even seem to be a way to make the following
code compile, either.
** **
** **
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
** **
import Prelude hiding (id,(.))
** **
class Category k where
id :: k a a
(.) :: k b c - k a b - k a c
** **
data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where**
**
(:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)
** **
instance (Category x, Category y) = Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
** **
This all works perfectly fine in Conor's SHE, (as does the thrist
example) so I'm wondering where the impedence mismatch comes in and how to
gain knowledge of this injectivity to make it work.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Try translating into System FC! It’s not just a question of what the type
checker will pass; we also have to produce a well-typed FC program.
Remember that (putting in all the kind abstractions and applications:
Thrist :: forall i. ((i,i) - *) - (i,i) - *
(:*) :: forall i j k. forall (a: (i,j) - *).
a '(i,j) - Thrist (j,k) a '(j,k) - Thrist (i,k) a '(i,k)
So consider ‘irt’:
irt :: forall i. forall (a : (i,i) - *). forall (x : (i,i)).
a x - Thrist i a x
irt = /\i. /\(a : (i,i) - *). /\(x: (i,i). \(ax: a x).
(:*) ? ? ? ? ax (Nil ...)
So, what are the three kind args, and the type arg, to (:*)?
It doesn’t seem to make sense... in the body of irt, (:*) produces a result of
type
Thrist (i,k) a ‘(i,k)
but irt’s signature claims to produce a result of type
Thrist i a x
So irt’s signature is more polymorphic than its body.
If we give irt a less polymorphic type signature, all is well
irt :: forall p,q. forall (a : ((p,q),(p,q)) - *). forall (x : ((p,q),(p,q))).
a x - Thrist (p,q) a x
Maybe you can explain what you want in System FC? Type inference and the
surface language come after that. If it can’t be expressed in FC it’s out of
court. Of course we can always beef up System FC.
I’m copying Stephanie and Conor who may have light to shed.
Simon
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 31 August 2012 18:27
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
dependency?
It is both perfectly reasonable and unfortunately useless. :(
The problem is that the more polymorphic type isn't any more polymorphic,
since (ideally) the product kind (a,b) is only inhabited by things of the form
'(x,y).
The product kind has a single constructor. But there is no way to express this
at present that is safe.
As it stands, I can fake this to an extent in one direction, by writing
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Kmett where
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
a ij - Thrist a '(j,k) - Thrist a ik
irt :: a x - Thrist a x
irt ax = ax :- Nil
and this compiles, but it just pushes the problem down the road, because with
that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd
ij) :: (x,y)
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when
you go to define an indexed bind, and type families are insufficient to the
task. Right now to get this property I'm forced to fake it with unsafeCoerce.
-Edward
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I'm going to defer to Conor on this one, as it is one of the examples from
his Kleisli Arrows of Outrageous fortune that I'm translating here. ;)
-Edward
On Fri, Aug 31, 2012 at 3:14 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:
Try translating into System FC! It’s not just a question of what the
type checker will pass; we also have to produce a well-typed FC program.**
**
** **
Remember that (putting in all the kind abstractions and applications:
Thrist :: forall i. ((i,i) - *) - (i,i) - *
(:*) :: forall i j k. forall (a: (i,j) - *).
a '(i,j) - Thrist (j,k) a '(j,k) - Thrist (i,k) a '(i,k)
** **
So consider ‘irt’:
** **
irt :: forall i. forall (a : (i,i) - *). forall (x : (i,i)).
a x - Thrist i a x
irt = /\i. /\(a : (i,i) - *). /\(x: (i,i). \(ax: a x).
(:*) ? ? ? ? ax (Nil ...)
** **
So, what are the three kind args, and the type arg, to (:*)?
** **
It doesn’t seem to make sense... in the body of irt, (:*) produces a
result of type
Thrist (i,k) a ‘(i,k)
but irt’s signature claims to produce a result of type
Thrist i a x
So irt’s signature is more polymorphic than its body.
** **
If we give irt a less polymorphic type signature, all is well
** **
irt :: forall p,q. forall (a : ((p,q),(p,q)) - *). forall (x :
((p,q),(p,q))).
a x - Thrist (p,q) a x
** **
** **
Maybe you can explain what you want in System FC? Type inference and the
surface language come after that. If it can’t be expressed in FC it’s out
of court. Of course we can always beef up System FC.
** **
I’m copying Stephanie and Conor who may have light to shed.
** **
Simon
** **
*From:* Edward Kmett [mailto:ekm...@gmail.com ekm...@gmail.com]
*Sent:* 31 August 2012 18:27
*To:* Simon Peyton-Jones
*Cc:* glasgow-haskell-users@haskell.org
*Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
functional dependency?
** **
It is both perfectly reasonable and unfortunately useless. :(
** **
The problem is that the more polymorphic type isn't any more
polymorphic, since (ideally) the product kind (a,b) is only inhabited by
things of the form '(x,y).
** **
The product kind has a single constructor. But there is no way to express
this at present that is safe.
** **
As it stands, I can fake this to an extent in one direction, by writing***
*
** **
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
** **
module Kmett where
** **
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
** **
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
** **
data Thrist :: ((i,i) - *) - (i,i) - * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
a ij - Thrist a '(j,k) - Thrist a ik
** **
irt :: a x - Thrist a x
irt ax = ax :- Nil
** **
and this compiles, but it just pushes the problem down the road, because
with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
ij, Snd ij) :: (x,y)
** **
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
when you go to define an indexed bind, and type families are insufficient
to the task. Right now to get this property I'm forced to fake it with
unsafeCoerce.
** **
-Edward
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
