Re: Type operators in GHC
Indeed -- lovely notational tricks, Iavor Edward! I think I'd be happy with one of these variations. At least worth experimenting with. -- Conal On Mon, Sep 17, 2012 at 8:05 PM, Carter Schonwald carter.schonw...@gmail.com wrote: 1) kudos to iavor and edward on the slick notation invention! 2) the key point is that ghc 7.6 does not have support for infix type variable notation, and how to encode infix arrow notations nicely subject that design choice, right? i'm likely just being a tad redundant in this conversation, but it never hurts to sanity check :) cheers -Carter On Mon, Sep 17, 2012 at 6:40 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote: Hi, Note that nobody was suggesting two pragmas with incompatible behaviors, only to have just one symbol reserved to still be able to have type operator variables. An issue with reserving a symbol for type operator variables is it doesn't help you today. 7.6.1 is already released. This means that any change in behavior would have to be in 7.6.2 at the earliest. Assuming the bikeshedding could complete and Simon et al. frantically patched the code tomorrow, rushing to release a 7.6.2 before the platform release. Failing that, you'd have a whole release cycle to wait through, probably a platform, before you could go back to your old behavior, and then your code would have some strange gap of GHC version numbers over which it didn't work. Everyone would have to pretend 7.6.1 never happened, or and break anyone's code that was already written for 7.6, so instead of one breaking change, we'd now have two. For instance, I'm already using ~ in 'github.com/ekmett/indexed.git' for natural transformations and I am loving it, and would be sad to lose it to the choice of ~ as a herald, similarly it would make the ~c~ trick more verbose, and ~ is particularly terrible for operators like ~+~. Other herald choices lead to different issues, '.' is slightly better for the other operators, but makes kind of ugly arrows, plus some day i'd _really_ like to be able to use . as a type constructor for functor composition! It is currently reserved at the type level as an almost accidental consequence of the way forall gets parsed today. I really like Iavor's entirely-in-language way of addressing the issue, due in part to it providing even better associativity than the existing approach, and honestly, even if GHC HQ was somehow convinced to set aside an ad hoc herald for type variables, I'd probably start using it in my code. (probably sandwiching between something like :- and : for old GHC compatibility). I really like that I can just call the Category c, and just get ~c~ or something similar as its arrows. This feels more notationally accurate to me. It also has two major benefits compared to any proposal for adding different heralds: 1.) It is compatible with old code, code written with 7.6.1 and I suppose future code, since (:) is such a remarkably awkward choice of herald for the reasons already documented that it seems an unlikely choice. 2.) I can program with it today. I just realized if you don't want to worry about collisions with the type naturals from GHC.TypeLits, and didn't care about pre-7.6 compatibility, you could strip the notation down all the way to cmap :: CFunctor f c d = (x -c y) - f x -d f y This is even shorter than the conventional cmap :: CFunctor f (~) (~~) = (x ~ y) - f x ~~ f y Which turns the but it is longer argument against it on its head. ;) -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 ___ 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 simo...@microsoft.com 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?
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 injective. Consider (D a ~ b c), where D is a data family (or a constructor, for
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 simo...@microsoft.com 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
