Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Hello, I have updated `GHC.TypeLits` to avoid the use of `Any` and also to use type families instead of functional dependencies. The new version should be in `base` on the `master` branch. I described the basic idea of what I did on this wiki page: http://hackage.haskell.org/trac/ghc/wiki/TypeNats/SingletonsAndKinds As usual, feedback is most welcome. -Iavor On Mon, Oct 15, 2012 at 6:13 PM, Richard Eisenberg wrote: > I think there's a decent record of this conversation at > http://hackage.haskell.org/trac/ghc/ticket/7259 > > The comments there skip over some of the discussion in this thread, but I > think the key ideas are all there. > > Here is how I see things: > - Yes, I believe Any can be turned back into a type family, and Iavor and > I will refactor around this change. As for my singletons paper, this > changes the encoding slightly, but nothing major. I think it's a change for > the better in the long run. > - I raised a concern about type inference in the presence of eta-expansion > in an earlier post to this thread and on the Trac page. Before really > moving forward here, I think it would good for others to think about these > issues. Instead of rehashing the idea again, please do visit the Trac page > and comment there. > - At one point, this thread included a discussion of injective type > families. While these would be a nice thing to have, they seem orthogonal > at this point and are probably best dropped from this discussion (which > seems to have happened naturally, at any rate). > > Richard > > On Oct 15, 2012, at 8:10 PM, Simon Peyton-Jones > wrote: > > I’m afraid I’ve rather lost track of this thread. Would someone care to > summarise, on a wiki page perhaps? > > I think the story is: > > ·Inspired by Nick’s idea, Iavor and Pedro have converged on a > single, type-family-based style for defining singletons. > ·This style no longer requires Any to be a data type, so I can > turn it back into a type family, which is a Good Thing because it paves the > way for an eta rule. RSVP and I’ll do that. > ·Iavor mutters about sketchiness, but I’m not sure what that > means specifically. > ·I’m not sure how, it at all, it affects Richard’s singletons > paper > > Simon > > > *From:* Iavor Diatchki [mailto:diatc...@galois.com] > *Sent:* 12 October 2012 21:11 > *To:* Richard Eisenberg > *Cc:* Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor > McBride; glasgow-haskell-users@haskell.org > *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a > functional dependency? > ** ** > Hello, > > (summary: I think Nick's idea works for what's in GHC.TypeLits, and it > would allow us to switch from `Any` as a constructor to `Any` as a > function.) > > On 10/11/2012 08:47 PM, Richard Eisenberg wrote: > > Iavor and I collaborated on the design of the building blocks of singleton > types, as we wanted our work to be interoperable. A recent scan through > TypeLits tells me, though, that somewhere along the way, our designs > diverged a bit. Somewhere on the to-do list is to re-unify the interfaces, > and actually just to import TypeLits into Data.Singletons so the > definitions are one and the same. Iavor, I'm happy to talk about the > details if you are. > > > The module GHC.TypeLits hasn't really changed much since last we talked > (the Nat1 type is new, but that's only for working with type-level naturals > and unrelated to this discussion). I added the SingE class so that my work > is compatible with Richard's (a simple newtype suffices if we are only > interested in working with singletons for type-level literals). So we > should certainly make the two compatible again, let me know what needs to > change. > > I was just playing around with Nick's idea and here is my version of the > code, which loads fine (but as I discuss in point 2 bellow I think it is a > bit sketchy...) > > import GHC.TypeLits hiding (SingE(..), Kind) > import qualified GHC.TypeLits as Old > > data Kind (k :: *) -- discuessed in point 2 bellow > > class SingE (any :: Kind k) rep | any -> rep where > fromSing :: Sing (a :: k) -> rep > > instance SingE (any :: Kind Nat) Integer where > fromSing = Old.fromSing > > instance SingE (any :: Kind Symbol) String where > fromSing = Old.fromSing > > I think that there are two interesting points about this code: > > 1. It is important that the instances are polymorphic because this tells > GHC that it is allowed to use the instance in any context as long as the > kinds match, regardless of the actual type. Note that this is not > the
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I think there's a decent record of this conversation at
http://hackage.haskell.org/trac/ghc/ticket/7259
The comments there skip over some of the discussion in this thread, but I think
the key ideas are all there.
Here is how I see things:
- Yes, I believe Any can be turned back into a type family, and Iavor and I
will refactor around this change. As for my singletons paper, this changes the
encoding slightly, but nothing major. I think it's a change for the better in
the long run.
- I raised a concern about type inference in the presence of eta-expansion in
an earlier post to this thread and on the Trac page. Before really moving
forward here, I think it would good for others to think about these issues.
Instead of rehashing the idea again, please do visit the Trac page and comment
there.
- At one point, this thread included a discussion of injective type families.
While these would be a nice thing to have, they seem orthogonal at this point
and are probably best dropped from this discussion (which seems to have
happened naturally, at any rate).
Richard
On Oct 15, 2012, at 8:10 PM, Simon Peyton-Jones wrote:
> I’m afraid I’ve rather lost track of this thread. Would someone care to
> summarise, on a wiki page perhaps?
>
> I think the story is:
>
> ·Inspired by Nick’s idea, Iavor and Pedro have converged on a single,
> type-family-based style for defining singletons.
> ·This style no longer requires Any to be a data type, so I can turn
> it back into a type family, which is a Good Thing because it paves the way
> for an eta rule. RSVP and I’ll do that.
> ·Iavor mutters about sketchiness, but I’m not sure what that means
> specifically.
> ·I’m not sure how, it at all, it affects Richard’s singletons paper
>
> Simon
>
>
> From: Iavor Diatchki [mailto:diatc...@galois.com]
> Sent: 12 October 2012 21:11
> To: Richard Eisenberg
> Cc: Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor McBride;
> glasgow-haskell-users@haskell.org
> Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
> dependency?
>
> Hello,
>
> (summary: I think Nick's idea works for what's in GHC.TypeLits, and it would
> allow us to switch from `Any` as a constructor to `Any` as a function.)
>
> On 10/11/2012 08:47 PM, Richard Eisenberg wrote:
> Iavor and I collaborated on the design of the building blocks of singleton
> types, as we wanted our work to be interoperable. A recent scan through
> TypeLits tells me, though, that somewhere along the way, our designs diverged
> a bit. Somewhere on the to-do list is to re-unify the interfaces, and
> actually just to import TypeLits into Data.Singletons so the definitions are
> one and the same. Iavor, I'm happy to talk about the details if you are.
>
> The module GHC.TypeLits hasn't really changed much since last we talked (the
> Nat1 type is new, but that's only for working with type-level naturals and
> unrelated to this discussion). I added the SingE class so that my work is
> compatible with Richard's (a simple newtype suffices if we are only
> interested in working with singletons for type-level literals). So we should
> certainly make the two compatible again, let me know what needs to change.
>
> I was just playing around with Nick's idea and here is my version of the
> code, which loads fine (but as I discuss in point 2 bellow I think it is a
> bit sketchy...)
>
> import GHC.TypeLits hiding (SingE(..), Kind)
> import qualified GHC.TypeLits as Old
>
> data Kind (k :: *) -- discuessed in point 2 bellow
>
> class SingE (any :: Kind k) rep | any -> rep where
> fromSing :: Sing (a :: k) -> rep
>
> instance SingE (any :: Kind Nat) Integer where
> fromSing = Old.fromSing
>
> instance SingE (any :: Kind Symbol) String where
> fromSing = Old.fromSing
>
> I think that there are two interesting points about this code:
>
> 1. It is important that the instances are polymorphic because this tells GHC
> that it is allowed to use the instance in any context as long as the kinds
> match, regardless of the actual type. Note that this is not
> the case if we write the instance using the singleton member of the proxy
> kind:
>
> data KindProxy (k :: *) = KindProxy
>
> instance SingE ('KindProxy :: KindProxy Nat) Integer where
> fromSing (SNat n) = n
> Such instances would only work if GHC could see that the type is 'KindProxy
> so if we have a type variable of the correct kind, the instance would not
> reduce. This is related to the eta-expansion issue---if we eliminated
> `Any`, then GHC could perform a kind-based improvement to deduce that the
> type variabl
RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I'm afraid I've rather lost track of this thread. Would someone care to
summarise, on a wiki page perhaps?
I think the story is:
*Inspired by Nick's idea, Iavor and Pedro have converged on a single,
type-family-based style for defining singletons.
*This style no longer requires Any to be a data type, so I can turn it
back into a type family, which is a Good Thing because it paves the way for an
eta rule. RSVP and I'll do that.
*Iavor mutters about sketchiness, but I'm not sure what that means
specifically.
*I'm not sure how, it at all, it affects Richard's singletons paper
Simon
From: Iavor Diatchki [mailto:diatc...@galois.com]
Sent: 12 October 2012 21:11
To: Richard Eisenberg
Cc: Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor McBride;
glasgow-haskell-users@haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
dependency?
Hello,
(summary: I think Nick's idea works for what's in GHC.TypeLits, and it would
allow us to switch from `Any` as a constructor to `Any` as a function.)
On 10/11/2012 08:47 PM, Richard Eisenberg wrote:
Iavor and I collaborated on the design of the building blocks of singleton
types, as we wanted our work to be interoperable. A recent scan through
TypeLits tells me, though, that somewhere along the way, our designs diverged a
bit. Somewhere on the to-do list is to re-unify the interfaces, and actually
just to import TypeLits into Data.Singletons so the definitions are one and the
same. Iavor, I'm happy to talk about the details if you are.
The module GHC.TypeLits hasn't really changed much since last we talked (the
Nat1 type is new, but that's only for working with type-level naturals and
unrelated to this discussion). I added the SingE class so that my work is
compatible with Richard's (a simple newtype suffices if we are only interested
in working with singletons for type-level literals). So we should certainly
make the two compatible again, let me know what needs to change.
I was just playing around with Nick's idea and here is my version of the code,
which loads fine (but as I discuss in point 2 bellow I think it is a bit
sketchy...)
import GHC.TypeLits hiding (SingE(..), Kind)
import qualified GHC.TypeLits as Old
data Kind (k :: *) -- discuessed in point 2 bellow
class SingE (any :: Kind k) rep | any -> rep where
fromSing :: Sing (a :: k) -> rep
instance SingE (any :: Kind Nat) Integer where
fromSing = Old.fromSing
instance SingE (any :: Kind Symbol) String where
fromSing = Old.fromSing
I think that there are two interesting points about this code:
1. It is important that the instances are polymorphic because this tells GHC
that it is allowed to use the instance in any context as long as the kinds
match, regardless of the actual type. Note that this is not
the case if we write the instance using the singleton member of the proxy kind:
data KindProxy (k :: *) = KindProxy
instance SingE ('KindProxy :: KindProxy Nat) Integer where
fromSing (SNat n) = n
Such instances would only work if GHC could see that the type is 'KindProxy so
if we have a type variable of the correct kind, the instance would not reduce.
This is related to the eta-expansion issue---if we eliminated `Any`, then GHC
could perform a kind-based improvement to deduce that the type variable must be
equal to `KindProxy`, because this is the only type with the correct kind.
2. As Nick noticed, we are not doing any fancy type computing in the class, so
we don't actually need any KindProxy elements---we are just doing overloading
based on a kind rather than a type. To emphasize this I made Kind an empty
type/kind and GHC is still happy: instances are resolved as intended. But...
`Kind` has no elements so what are the instances applied to? The only reason
this works is that GHC has defaulted the instances to use `Any`. To me this
seems a bit sketchy.
So what to do? Changing the code in this style (using the normal non-empty
proxy) makes sense because I think that it would allow us to change `Any` into
a type function rather than a type constructor, like Simon did and un-did
recently. The reason I think this will work is because now there will be no
uses of `Any` in the definitions of the instances, it will only appear in the
uses of the instances.
Furthermore, I think it makes sense for GHC to check that for each use of the
type function `Any`, the kind where it is used is non-empty. I'm not sure how
easy it would be to implement that, so maybe we can deal with it later.
-Iavor
___
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 - what's the general status on this initiative? Has much | > happened in about a month?) | | From my end, nothing. I'm trying to wrap up some other work I'm doing | on GHC (ordered overlapping type family instances), and it looks like | some of the questions I raised in my last email in this thread are | still open. I think "this initiative" refers to the question of eta expansion in FC. We are stalled on this, partly for lack of bandwidth and partly because there are more urgent things to do. But I did capture the issue in this ticket http://hackage.haskell.org/trac/ghc/ticket/7259 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?
| Iavor and I collaborated on the design of the building blocks of | singleton types, as we wanted our work to be interoperable. A recent | scan through TypeLits tells me, though, that somewhere along the way, | our designs diverged a bit. Somewhere on the to-do list is to re-unify | the interfaces, and actually just to import TypeLits into | Data.Singletons so the definitions are one and the same. Iavor, I'm | happy to talk about the details if you are. That would be good! 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?
On Oct 11, 2012, at 11:20 PM, Nicolas Frisby wrote: > > (Also — what's the general status on this initiative? Has much > happened in about a month?) >From my end, nothing. I'm trying to wrap up some other work I'm doing on GHC >(ordered overlapping type family instances), and it looks like some of the >questions I raised in my last email in this thread are still open. > > The to my trick key is to use the promotion of this data type. > >> data KindProxy (k :: *) = KindProxy Yes, I used this in an earlier version of singletons. Then, Simon told me about Any, and that cleaned up the code considerably. I don't think, though, there was anything fundamentally wrong (other than aesthetics) with KindProxy. Thanks for bringing this up, as I had forgotten about this approach in the intervening months. > > I'm less familiar with the usage in GHC.TypeLits. Iavor and I collaborated on the design of the building blocks of singleton types, as we wanted our work to be interoperable. A recent scan through TypeLits tells me, though, that somewhere along the way, our designs diverged a bit. Somewhere on the to-do list is to re-unify the interfaces, and actually just to import TypeLits into Data.Singletons so the definitions are one and the same. Iavor, I'm happy to talk about the details if you are. Nick, thanks for pushing on this thread! Richard ___ 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 Thu, Oct 11, 2012 at 10:20 PM, Nicolas Frisby wrote: > The to my trick key is to use the promotion of this data type. "The key to my trick is to use the promotion of this data type." Wow — I have no idea what happened there. ___ 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 Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg wrote:
> As for recovering "kind classes" and such once Any is made into a type
> family: I'm in favor of finding some way to do explicit kind instantiation,
> making the Any trick obsolete. I'm happy to leave it to others to decide the
> best concrete syntax.
I'll admit I haven't parsed this entire email thread, but I read
enough of it early on that I wanted to avoid Any recently. Returning
to find this quote from Richard, perhaps the trick I came up is the
one you're after.
(Also — what's the general status on this initiative? Has much
happened in about a month?)
The to my trick key is to use the promotion of this data type.
> data KindProxy (k :: *) = KindProxy
I needed it in order to define this family, which counts the number of
arguments a kind has.
> type family CountArgs (kp :: KindProxy k) :: Nat
> type instance CountArgs (kp :: *) = Z
> type instance CountArgs (kp :: kD -> kR) = S (CountArgs ('KindProxy ::
> KindProxy kR))
The proxy is necessary on the RHS of the second instance, in which I
need a type of kind kR, but I wouldn't have any means to build one
(without Any) were CountArgs simply of kind (k -> Nat).
This usage is comparable to Richard's usage in the singletons library,
insomuch as I understand from the Haskell 2012 paper.
I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I
believe I'd change SingE like so
> class SingE (kparam :: KindProxy k) rep | kparam -> rep where
> fromSing :: Sing (a :: k) -> rep
> instance SingE (kparam :: KindProxy Nat) Integer where
> fromSing (SNat n) = n
> instance SingE (kparam :: KindProxy Symbol) String where
> fromSing (SSym s) = s
However, looking through the rest of that module, I see no point where
a proxy is actually required (as it is required in the second case of
CountArgs). Maybe I'm just missing it, or maybe Iavor is just
interested in *enforcing* the fact that the type is not of
consequence?
Along those same lines… Iavor had SingE instances declared for (Any ::
KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he
didn't leave the type polymorphic, as I have. Perhaps it matters for
various uses of SingE? I haven't tried using my code with examples, so
maybe that's where issues would show up. If it were necessary, the
instances could instead be as follows.
> instance SingE ('KindProxy :: KindProxy Nat) Integer where
> fromSing (SNat n) = n
> instance SingE ('KindProxy :: KindProxy Symbol) String where
> fromSing (SSym s) = s
Is this the kind of trick you were after, Richard? It might pollute
the code base and interface a bit with KindProxy wrappers, but I've
not found that insurmountable. Hopefully that isn't a show stopper for
you.
HTH
___
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 Sun, Sep 16, 2012 at 11:49 AM, Simon Peyton-Jones wrote: > I don't really want to eagerly eta-expand every type variable, because (a) > we'll bloat the constraints and (b) we might get silly error messages. For > (b) consider the insoluble constraint > [W] a~b > where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll > get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we > DEFINITELY don't want to report that as a type error! I almost forgot to mention this, but... You should perhaps talk to the agda implementors. They've done a lot of work to avoid eta expanding as much as possible, because it was killing performance (but it does also make for some nicer display). So they probably know some tricks. -- 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?
Please see my responses inline. On Sep 16, 2012, at 11:49 AM, Simon Peyton-Jones wrote: > Eta rules > ~~ > * We want to add eta-rules to FC. Sticking to pairs for now, that would > amount to > adding two new type functions (Fst, Snd), and three new, built-in axioms > axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a) > axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a > axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a > Generalising to arbitrary products looks feasible. The last two axioms are the straightforward compilations of the type families Fst and Snd -- nothing new is needed to create these. The first is the challenge and will require some type inference magic. > > * Adding these axioms would make FC inconsistent, because > axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..) > and that has two different type constructors on each side. > However, I think is readily solved: see below under "Fixing Any" > > * Even in the absence of Any, it's not 100% obvious that adding the above > eta axioms retains consistency of FC. I believe that Richard is > volunteering > to check this out. Right, Richard? I'll be going through the consistency proof shortly for some other work I'm doing, so I'll throw this into the mix while it's all paged in. This might be tricky, though. > > Type inference > ~ > I'm a little unclear about the implications for inference. One route > might be this. Suppose we are trying to solve a constraint > [W] (a:'(k1,ks)) ~ '( t1, t2 ) > where a is an untouchable type variable. (if it was touchable we'd > simply unify it.) Then we can replace it with a constraint >[W] '(Fst a, Snd a) ~ '( t1, t2) I don't think that's the right replacement. The next natural step would be decomposition, leading to (Fst a ~ t1) and (Snd a ~ t2), which would then get stuck, because Fst and Snd aren't injective. So, I would say we need a1, a2 fresh [G] a ~ '(a1, a2) [W] '(a1, a2) ~ '(t1, t2) which would then decompose correctly. As I write this, I'm worried about that freshness condition… what if 'a' appears multiple times in the type? We would either need to guarantee that a1 and a2 are the same each time, or create new [W] constraints that a1 ~ a1', etc. But, maybe this is easier in practice than it seems. Type inference experts? > > Is that it? Or do we need more? I'm a bit concerned about constraints like >F a ~ e > where a:'(k1,k2), and we have a type instance like F '(a,b) = … Here, the proper eta-expansion (a ~ '(Fst a, Snd a)) works great, no? > > Anything else? > > I don't really want to eagerly eta-expand every type variable, because (a) > we'll bloat the constraints and (b) we might get silly error messages. For > (b) consider the insoluble constraint >[W] a~b > where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll > get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we > DEFINITELY don't want to report that as a type error! Could this be handled using mechanisms already in place to report errors about unexpanded type synonyms? If so, we could eagerly expand, and I think that would ease the implementation. However, I defer to those more expert than I in such issues. > > Fixing Any > ~~~ > * I think we can fix the Any problem readily by making Any into a type > family, > that has no instances. We certainly allow equalities with a type > *family* application on the left and a type constructor on the right. > I have implemented this change already... it seems like a good plan. > > * Several people have asked why we need Any at all. Consider this source > program > reverse [] > At what type should we instantiate 'reverse' and the empty list []? Any > type > will do, but we must choose one; FC doesn't have unbound type variables. > So I instantiate it at (Any *): > reverse (Any *) ([] (Any *)) > > Why is Any poly-kinded? Because the above ambiguity situation sometimes > arises at other kinds. > > * I'm betting that making Any into a family will mess up Richard's > (entirely separate) > use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ > Any k2) > does not entail (k1~k2). We need Any to be an *injective* type family. > We want > injective type families anyway, so I guess I should add the internal > machinery > (which is easy). I don't think injectivity is the key here. As I understand it, any equality t1 ~ t2 entails k1 ~ k2, where t1:k1 and t2:k2. When trying to unify Any k1 ~ Any k2, GHC will already (I think) unify k1 and k2, just based on the kinds, not on injectivity. Is there something here I'm missing? > > I believe that injective type families are fully decomposable, just like > data type families, > correct? No, I don't think so. Data families are generative, which is a stronger condition than inje
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones wrote: > [...] > Type inference > ~ > I'm a little unclear about the implications for inference. One route > might be this. Suppose we are trying to solve a constraint > [W] (a:'(k1,ks)) ~ '( t1, t2 ) > where a is an untouchable type variable. (if it was touchable we'd > simply unify it.) Then we can replace it with a constraint > [W] '(Fst a, Snd a) ~ '( t1, t2) > > Is that it? Or do we need more? I'm a bit concerned about constraints like > F a ~ e > where a:'(k1,k2), and we have a type instance like F '(a,b) = ... > F a ~ F '(Fst a, Snd a) has to hold, so one does need to expand a for constraints like F a ~ e in this case. One way to think of it is that patterns like '(a,b) are the same as value-level ~(a,b) ones. -- Andrea ___ 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?
Hello, On Tue, Sep 18, 2012 at 12:10 AM, Simon Peyton-Jones wrote: > > The technically-straightforward thing to do is to add kind application, > but that's a bit complicated notationally. > http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication Does > anyone have any other ideas? > > I think that the right way to proceed would be to add explicit syntax for kind abstraction and application (which, I imagine, we already have internally in GHC). As for the concrete syntax, I prefer the explicitly annotated form, even if the ":: Kind" part is treated completely syntactically for the moment, because the notation seems compatible with future generalizations that we might want to do (e.g., the work that Stephanie, Richard, Connor, and Adam are doing). So the source Haskell might look something like this: type family SingRep (a :: Kind) type instance SingRep (Nat :: Kind) = Integer class SingE (a :: Kind) where ... -Iavor PS: I just modified the ExplicitTypeApplication wiki page to reflect more accurately the singletons example. For those who've seen the old page: I changed the 'Sing' data family example, because that family needs an actual type parameter---it is not enough to just have a kind parameter (the reason being that we want to write things like "Sing 5", where "5" is a type). ___ 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 think I was a little hasty below, and need a little help.
Making 'Any' an type family, even an injective one, does not work for the use
that Richard and Iavor make of it, eg in TypeLits. Here's an example from
TypeLits:
instance SingE (Any :: Nat) Integer where
where SingE :: forall k. k -> * -> Constraint
Here Iavor is using Any as a proxy kind argument. He really wants
SingE :: forall k. * -> Constraint
with kind-indexed instances. But (much as with the Typeable class at the value
level) he is giving it a type argument so that he can later say things like
SingE (Any :: *->*) v
Without this trick we'd need kind application, something like
SingE {*->*} v
None of this works if Any is a type family, because the type patterns in an
instance decl aren't allowed to involve type families (and rightly so; value
declarations don't have functions in patterns).
Nor can we fix this by introducing some *other* constant, Proxy :: forall k. k,
because that suffers from the inconsistency problem that we started with.
Another way to say this is as follows. In the value world we have often written
typeOf (undefined :: a)
using bottom as a proxy type argument. That works in Haskell, but not in a
strict, or strongly-normalising language. And at the type level we are
(mostly) strongly normalising.
The technically-straightforward thing to do is to add kind application, but
that's a bit complicated notationally.
http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication Does anyone
have any other ideas?
Simon
| -Original Message-
| From: Simon Peyton-Jones
| Sent: 16 September 2012 16:49
| To: Richard Eisenberg; Andrea Vezzosi
| Cc: Adam Gundry; Conor McBride; Stephanie Weirich; glasgow-haskell-
| us...@haskell.org; Simon Peyton-Jones
| Subject: RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
| functional dependency?
|
| Friends
|
| Thanks for this useful conversation, by email and at ICFP. Here's my
| summary. Please tell me if I'm on the right track. It would be great
| if someone wanted to create a page on the GHC wiki to capture the issues
| and outcomes.
|
| Simon
|
| Eta rules
| ~~
| * We want to add eta-rules to FC. Sticking to pairs for now, that
| would amount to
| adding two new type functions (Fst, Snd), and three new, built-in
| axioms
| axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
| axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
| axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
| Generalising to arbitrary products looks feasible.
|
| * Adding these axioms would make FC inconsistent, because
| axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
| and that has two different type constructors on each side.
| However, I think is readily solved: see below under "Fixing Any"
|
| * Even in the absence of Any, it's not 100% obvious that adding the
| above
|eta axioms retains consistency of FC. I believe that Richard is
| volunteering
|to check this out. Right, Richard?
|
| Type inference
| ~
| I'm a little unclear about the implications for inference. One route
| might be this. Suppose we are trying to solve a constraint
| [W] (a:'(k1,ks)) ~ '( t1, t2 )
| where a is an untouchable type variable. (if it was touchable we'd
| simply unify it.) Then we can replace it with a constraint
| [W] '(Fst a, Snd a) ~ '( t1, t2)
|
| Is that it? Or do we need more? I'm a bit concerned about constraints
| like
| F a ~ e
| where a:'(k1,k2), and we have a type instance like F '(a,b) = ...
|
| Anything else?
|
| I don't really want to eagerly eta-expand every type variable, because
| (a) we'll bloat the constraints and (b) we might get silly error
| messages. For (b) consider the insoluble constraint
| [W] a~b
| where a and b are both skolems of kind '(k1,k2). If we eta-expand both
| we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b),
| and we DEFINITELY don't want to report that as a type error!
|
| Fixing Any
| ~~~
| * I think we can fix the Any problem readily by making Any into a type
| family,
| that has no instances. We certainly allow equalities with a type
| *family* application on the left and a type constructor on the
| right.
| I have implemented this change already... it seems like a good
| plan.
|
| * Several people have asked why we need Any at all. Consider this
| source program
| reverse []
| At what type should we instantiate 'reverse' and the empty list []?
| Any type
| will do, but we must choose one; FC doesn't have unbound type
| variables.
| So I instantiate it at (Any *):
| reverse (Any *) ([] (Any *))
|
| Why is Any poly-kinded? Because the
RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
| Will unsafeCoercing to and from Any still work with this plan? (If not | then I can just use data Anything = forall a. Anything a, so it's not a | big deal.) Yes I think it'll be fine, but thanks for highlighting this other use of Any. 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?
On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones wrote: > > Fixing Any > ~~~ > * I think we can fix the Any problem readily by making Any into a type family, > that has no instances. We certainly allow equalities with a type > *family* application on the left and a type constructor on the right. > I have implemented this change already... it seems like a good plan. > Will unsafeCoercing to and from Any still work with this plan? (If not then I can just use data Anything = forall a. Anything a, so it's not a big deal.) -- Your ship was destroyed in a monadic eruption. ___ 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?
Friends Thanks for this useful conversation, by email and at ICFP. Here's my summary. Please tell me if I'm on the right track. It would be great if someone wanted to create a page on the GHC wiki to capture the issues and outcomes. Simon Eta rules ~~ * We want to add eta-rules to FC. Sticking to pairs for now, that would amount to adding two new type functions (Fst, Snd), and three new, built-in axioms axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a) axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a Generalising to arbitrary products looks feasible. * Adding these axioms would make FC inconsistent, because axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..) and that has two different type constructors on each side. However, I think is readily solved: see below under "Fixing Any" * Even in the absence of Any, it's not 100% obvious that adding the above eta axioms retains consistency of FC. I believe that Richard is volunteering to check this out. Right, Richard? Type inference ~ I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint [W] (a:'(k1,ks)) ~ '( t1, t2 ) where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint [W] '(Fst a, Snd a) ~ '( t1, t2) Is that it? Or do we need more? I'm a bit concerned about constraints like F a ~ e where a:'(k1,k2), and we have a type instance like F '(a,b) = ... Anything else? I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint [W] a~b where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error! Fixing Any ~~~ * I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type *family* application on the left and a type constructor on the right. I have implemented this change already... it seems like a good plan. * Several people have asked why we need Any at all. Consider this source program reverse [] At what type should we instantiate 'reverse' and the empty list []? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at (Any *): reverse (Any *) ([] (Any *)) Why is Any poly-kinded? Because the above ambiguity situation sometimes arises at other kinds. * I'm betting that making Any into a family will mess up Richard's (entirely separate) use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any k2) does not entail (k1~k2). We need Any to be an *injective* type family. We want injective type families anyway, so I guess I should add the internal machinery (which is easy). I believe that injective type families are fully decomposable, just like data type families, correct? To make them available at the source level, we'd just need to a) add the syntax injective type family F a :: * b) check for injectivity when the user adds type instances Richard, would you like to do that 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 Sep 5, 2012, at 2:21 PM, Edward Kmett wrote: > > I noticed that the polykindedness of Any is abused in the GHC.TypeLits to > make fundeps determining a kind, but where else is it exploited? I similarly abused Any to write the singletons library, but it's really a hack to work with kind classes and functions from kinds to types. If these features were directly accessible, the Any hack would no longer be needed. Has anyone out there used Any for another purpose? Richard___ 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've come to think the culprit here is the fallacy that Any should inhabit
every kind.
I realize this is useful from an implementation perspective, but it has a
number of far reaching consequences:
This means that a product kind isn't truly a product of two kinds. x * y,
it winds up as a *distinguishable* x * y + 1, as Andrea has shown us
happens because you can write a type family or MPTC with fundep that can
match on Any.
A coproduct of two kinds x + y, isn't x + y, its x + y + 1.
Kind level naturals aren't kind nats, they are nats + 1, and not even the
one point compactification we get with lazy nats where you have an
indistinguishable infinity added to the domain, but rather there is a
distinguished atom to each kind under consideration.
I noticed that the polykindedness of Any is abused in the GHC.TypeLits to
make fundeps determining a kind, but where else is it exploited?
-Edward
On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg wrote:
> I retract my statement.
>
> My mistake was that I looked at the definition for consistency in FC --
> which correctly is agnostic to non-base-kind coercions -- and applied it
> only to the set of coercion assumptions, not to any coercion derivable from
> the assumptions. As Andrea's example shows, by assuming an eta coercion, it
> is possible to derive an inconsistent coercion.
>
> Examining the definition for FC consistency more closely, an eta coercion
> does not match to the form allowed for coercion assumptions used to prove
> consistency. The proof, in [1], requires all assumptions to have a type
> family application on the left-hand side. An eta coercion does not have a
> type family application on either side, and so the consistency proof in [1]
> does not apply.
>
> In light of this, it would seem that allowing eta coercions while
> retaining consistency would require some more work.
>
> Thanks for pointing out my mistake.
> Richard
>
> [1] S. Weirich et al. "Generative Type Abstraction and Type-level
> Computation."
> (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)
>
> On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:
>
> > On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg
> wrote:
> >> [...]
> >> So, it seems possible to introduce eta coercions into FC for all kinds
> containing only one type constructor without sacrificing soundness. How the
> type inference engine/source Haskell triggers the use of these coercions is
> another matter, but there doesn't seem to be anything fundamentally wrong
> with the idea.
> >>
> >
> > A recent snapshot of ghc HEAD doesn't seem to agree:
> >
> > {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> > TypeFamilies, ScopedTypeVariables, TypeOperators #-}
> >
> > import GHC.Exts
> > import Unsafe.Coerce
> >
> > data (:=:) :: k -> k -> * where
> > Refl :: a :=: a
> >
> > trans :: a :=: b -> b :=: c -> a :=: c
> > trans Refl Refl = Refl
> >
> > type family Fst (x :: (a,b)) :: a
> > type family Snd (x :: (a,b)) :: b
> >
> > type instance Fst '(a,b) = a
> > type instance Snd '(a,b) = b
> >
> > eta :: x :=: '(Fst x, Snd x)
> > eta = unsafeCoerce Refl
> > -- ^^^ this is an acceptable way to simulate new coercions, i hope
> >
> > type family Bad s t (x :: (a,b)) :: *
> > type instance Bad s t '(a,b) = s
> > type instance Bad s t Any = t
> >
> > refl_Any :: Any :=: Any
> > refl_Any = Refl
> >
> > cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> > cong_Bad Refl = Refl
> >
> > s_eq_t :: forall (s :: *) (t :: *). s :=: t
> > s_eq_t = cong_Bad (trans refl_Any eta)
> >
> > subst :: x :=: y -> x -> y
> > subst Refl x = x
> >
> > coerce :: s -> t
> > coerce = subst s_eq_t
> >
> > {-
> > GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help
> > *Main> coerce (4.0 :: Double) :: (Int,Int)
> > (Segmentation fault
> > -}
> >
> > -- Andrea Vezzosi
> >
>
>
> ___
> 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: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I retract my statement.
My mistake was that I looked at the definition for consistency in FC -- which
correctly is agnostic to non-base-kind coercions -- and applied it only to the
set of coercion assumptions, not to any coercion derivable from the
assumptions. As Andrea's example shows, by assuming an eta coercion, it is
possible to derive an inconsistent coercion.
Examining the definition for FC consistency more closely, an eta coercion does
not match to the form allowed for coercion assumptions used to prove
consistency. The proof, in [1], requires all assumptions to have a type family
application on the left-hand side. An eta coercion does not have a type family
application on either side, and so the consistency proof in [1] does not apply.
In light of this, it would seem that allowing eta coercions while retaining
consistency would require some more work.
Thanks for pointing out my mistake.
Richard
[1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation."
(http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)
On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:
> On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg wrote:
>> [...]
>> So, it seems possible to introduce eta coercions into FC for all kinds
>> containing only one type constructor without sacrificing soundness. How the
>> type inference engine/source Haskell triggers the use of these coercions is
>> another matter, but there doesn't seem to be anything fundamentally wrong
>> with the idea.
>>
>
> A recent snapshot of ghc HEAD doesn't seem to agree:
>
> {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> TypeFamilies, ScopedTypeVariables, TypeOperators #-}
>
> import GHC.Exts
> import Unsafe.Coerce
>
> data (:=:) :: k -> k -> * where
> Refl :: a :=: a
>
> trans :: a :=: b -> b :=: c -> a :=: c
> trans Refl Refl = Refl
>
> type family Fst (x :: (a,b)) :: a
> type family Snd (x :: (a,b)) :: b
>
> type instance Fst '(a,b) = a
> type instance Snd '(a,b) = b
>
> eta :: x :=: '(Fst x, Snd x)
> eta = unsafeCoerce Refl
> -- ^^^ this is an acceptable way to simulate new coercions, i hope
>
> type family Bad s t (x :: (a,b)) :: *
> type instance Bad s t '(a,b) = s
> type instance Bad s t Any = t
>
> refl_Any :: Any :=: Any
> refl_Any = Refl
>
> cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> cong_Bad Refl = Refl
>
> s_eq_t :: forall (s :: *) (t :: *). s :=: t
> s_eq_t = cong_Bad (trans refl_Any eta)
>
> subst :: x :=: y -> x -> y
> subst Refl x = x
>
> coerce :: s -> t
> coerce = subst s_eq_t
>
> {-
> GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help
> *Main> coerce (4.0 :: Double) :: (Int,Int)
> (Segmentation fault
> -}
>
> -- Andrea Vezzosi
>
___
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 Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg wrote:
> [...]
> So, it seems possible to introduce eta coercions into FC for all kinds
> containing only one type constructor without sacrificing soundness. How the
> type inference engine/source Haskell triggers the use of these coercions is
> another matter, but there doesn't seem to be anything fundamentally wrong
> with the idea.
>
A recent snapshot of ghc HEAD doesn't seem to agree:
{-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
TypeFamilies, ScopedTypeVariables, TypeOperators #-}
import GHC.Exts
import Unsafe.Coerce
data (:=:) :: k -> k -> * where
Refl :: a :=: a
trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl
type family Fst (x :: (a,b)) :: a
type family Snd (x :: (a,b)) :: b
type instance Fst '(a,b) = a
type instance Snd '(a,b) = b
eta :: x :=: '(Fst x, Snd x)
eta = unsafeCoerce Refl
-- ^^^ this is an acceptable way to simulate new coercions, i hope
type family Bad s t (x :: (a,b)) :: *
type instance Bad s t '(a,b) = s
type instance Bad s t Any = t
refl_Any :: Any :=: Any
refl_Any = Refl
cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
cong_Bad Refl = Refl
s_eq_t :: forall (s :: *) (t :: *). s :=: t
s_eq_t = cong_Bad (trans refl_Any eta)
subst :: x :=: y -> x -> y
subst Refl x = x
coerce :: s -> t
coerce = subst s_eq_t
{-
GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help
*Main> coerce (4.0 :: Double) :: (Int,Int)
(Segmentation fault
-}
-- Andrea Vezzosi
___
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?
Forgot to include the reference: [1] B. A. Yorgey et al. "Giving Haskell a Promotion" (http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf) On Sep 3, 2012, at 3:26 PM, Richard Eisenberg wrote: > On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote: > >> As Edward and others have recognised, the problem here is that FC >> coercions are not expressive enough to prove eta rules, that is >> >> forall x : (a, b) . x ~ (Fst x, Snd x) >> >> or more generally, that every element of a single-constructor (record) >> type is equal to the constructor applied to the projections. >> >> It seems like it should be perfectly fine to assert such a thing as an >> axiom, though, ... unless >> you have Any (as Richard observed), in which case all bets are off. Why >> did you want Any again? > > > I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, > Any has been helpful in other type hackery exploits of mine...) So, any way > of introducing eta-coercions will have to respect Any. > > Intriguingly, the most recent published formulation of FC [1] leaves room for > adding eta rules. The issue is one of consistency: if we have a coercion g : > forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and the existence > of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for > consistency (from which progress & preservation are proved) apply only to > coercions at a base kind, either * or Constraint. So, our eta coercion g is > exempt from the consistency check -- it cannot make a system inconsistent. > Thus, with or without Any, the coercion g cannot lead to a program that > crashes due to a type error. > > So, it seems possible to introduce eta coercions into FC for all kinds > containing only one type constructor without sacrificing soundness. How the > type inference engine/source Haskell triggers the use of these coercions is > another matter, but there doesn't seem to be anything fundamentally wrong > with the idea. > > Richard ___ 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 Sep 1, 2012, at 4:25 AM, Adam Gundry wrote: > As Edward and others have recognised, the problem here is that FC > coercions are not expressive enough to prove eta rules, that is > > forall x : (a, b) . x ~ (Fst x, Snd x) > > or more generally, that every element of a single-constructor (record) > type is equal to the constructor applied to the projections. > > It seems like it should be perfectly fine to assert such a thing as an > axiom, though, ... unless > you have Any (as Richard observed), in which case all bets are off. Why > did you want Any again? I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, Any has been helpful in other type hackery exploits of mine...) So, any way of introducing eta-coercions will have to respect Any. Intriguingly, the most recent published formulation of FC [1] leaves room for adding eta rules. The issue is one of consistency: if we have a coercion g : forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and the existence of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for consistency (from which progress & preservation are proved) apply only to coercions at a base kind, either * or Constraint. So, our eta coercion g is exempt from the consistency check -- it cannot make a system inconsistent. Thus, with or without Any, the coercion g cannot lead to a program that crashes due to a type error. So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea. Richard ___ 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 not Conor, but I'll have a go...
On 31/08/12 20:14, Simon Peyton-Jones wrote:
> 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.
As Edward and others have recognised, the problem here is that FC
coercions are not expressive enough to prove eta rules, that is
forall x : (a, b) . x ~ (Fst x, Snd x)
or more generally, that every element of a single-constructor (record)
type is equal to the constructor applied to the projections.
It seems like it should be perfectly fine to assert such a thing as an
axiom, though: FC doesn't care what your equality proof is, provided
it's consistent. Consistency of eta-laws follows from the fact that any
inhabitant of the kind must be built with the sole constructor, unless
you have Any (as Richard observed), in which case all bets are off. Why
did you want Any again?
> 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 (:*)?
Here's my solution:
irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).
(:*) i i i a (ax |> g1) (Nil i a) |> g2
where
g1 : a x ~ a '(Fst x, Snd x)
g1 = < a > (eta x)
g2 : Thrist i a '(Fst x, Snd x) ~ Thrist i a x
g2 = < Thrist i a > (sym (eta x))
are coercions derived from the eta axiom above.
Hope this helps, now I should really go on holiday,
Adam
> *From:*Edward Kmett [mailto:ekm...@gmail.com]
> *Sent:* 31 August 2012 18:27
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users@haskell.org
> <mailto: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
wrote:
> 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.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?
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.org<mailto: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?
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 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 > 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?
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
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?
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?
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?
On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg wrote: > 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?
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 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 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
> 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 '(
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 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?
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 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 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
>>>
>>> ** **
>>>
>>> ** **
>>>
>>> *F
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
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 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 > 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, 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
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
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, 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)
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 wrote:
> 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: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
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 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
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
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
