- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]
by Anthony Clayden 05 Jun '17

05 Jun '17

> On Sun Jun 4 13:11:47 UTC 2017, J. Garrett Morris wrote: >> On Sun, Jun 4, 2017 at 1:00 PM, Anthony Clayden wrote: >> ... > You have reiterated a point that is made at length ... Good, so we're agreed that the 2010 paper is inconsistent to reject `(f :+: f)` but accept `((f :+: f) :+: f)`. > I shouldn't, however, have suggested in 2015 that > the deduplicated version is necessarily preferable. I don't follow. The 2015 version is consistent. > If you omit the deduplication constraints, you simply end > up with Leijen-style scoped rows [Leijen, TFP05] ... Ouch! Its "A novel aspect of this work is that records can contain duplicate labels, " is about the most blood-chilling claim I've seen in the many papers on records systems. It is true, though, compared to what you seem to suggest "effectively introducing a form of scoping over the labels. " If `((f :+: g) :+: (h :+: f))` is to be supported, what's the basis for preferring `f` to the left or right? > ... Of course, if, as we did in 2010, you use classes instead > of branching to implement elimination on variants, you have no way to > tell the difference between the two models of variants, .. Is the only point I was wanting to make: using a single class fails to separate concerns, in this example. >> I'm working on showing how the Swierstra encoding >> could be catered for in Haskell 2010 + MPTCs+TypeEq. > You keep talking about guarding instances or equations. > Guards are equivalent to closed type families, I think not. They're somewhere between CTFs and Instance Chains. In that guarded instances are not closed. Which also appears to be your claim wrt Instance Chains. > ... so of course they're sufficient to implement > Swierstra's encoding (following any of ...), (I was specifically aiming to implement using Haskell as at 2010, but let it pass ...) Yes any of these approaches are "sufficient". That's not in debate. > and will require auxiliary definitions and indirections Yes, see code I posted subsequent to your message. > that would not be required using instance chains. Huh? Your 2015 paper uses auxiliaries class `In` Figure 3 in the Instance Chains version. True that the 2010 paper uses no auxiliaries, but it thereby ends up inconsistent. What is "wrong" with using auxiliaries? (Again, in terms of readability.) AntC

1 0

Different results when building wxHaskell on Cabal and Stack
by Yotam Ohad 04 Jun '17

04 Jun '17

Hello cafe, Lately, I wanted to try wxHaskell, so I downloaded and install wxWidgets and added the necessary paths to %PATH%. The problem was that when trying to build, cabal would have no problem at all, while stack sends me into battle with my path, complaining about missing header and executable files and so on. I don't understand why stack is having such a hard time when cabal has no trouble at all. I know that they are not the same, but I still think that it is weird that stack is acting like that. Thanks for your help, Yotam

2 1

Re: [Haskell-cafe] Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]
by Anthony Clayden 04 Jun '17

04 Jun '17

> On Sun Jun 4 12:00:21 UTC 2017, Anthony Clayden wrote: > I think this shows that using class instances > to both define methods and drive selection logic > can fail to separate concerns. Richard's been (quite correctly) prodding me to explain why I want a no-instance in places, rather than an `instance ,,, fails` or `instance (TypeError ... ) => ...` I think Figure 7 in Garrett's 2015 paper provides a case in point. I find that `type family Ifi` and its call line 5/6 above to be more like an exercise in obfuscated type-programming. `type family Into` doesn't observe kind-hygiene in the way we'd expect a term-level function to observe type-hygiene. Type families `Into` or Ifi` might properly return: * Refl | L lp | R rp -- that could be a DataKind (where `lp` or `rp` is from a recursive call to `Into`) * or `Nope` -- which is a Boolean DataKind (yeuch) Yes `Into` does need to chase down the data structure in order to return the correct L/R accessor. But it doesn't need to also encode failure in that way. The frustrating thing (for me as reader) is `type family IsIn` is looking ahead inside the data structure to find `f`. Isn't that enough lookahead and error detection? I want there to be no equation for `Into` returning `Nope`. So I want no Line 7, nor line 10, 13 in `type family Ifi`. I think I'd tackle it this way. Instead of `type family IsIn` returning a Boolean, > type family CountF f g :: Nat where > CountF f f = (S Z) > CountF f (g :+: h) = Plus (CountF f g) (CountF f h) > CountF f g = Z Then for `Into` I'd use a count-preparing helper function, (instead of `Ifi`) and avoid those `Nope` returns: > type family Into f g where > Into f f = Refl > Into f (g :+: h) = IntoLR f (g :+: h) (CountF f g) (CountF f h) > -- no fail case needed > > type family IntoLR f g (cg :: Nat) (ch :: Nat) > type instance Into' f (g :+: h) (S Z) Z = L (Into f g) > type instance Into' f (g :+: h) Z (S Z) = R (Into f h) > -- no fail case needed, no overlap, so not closed So if the counts return {Z, Z} or {S Z, S Z} or {S (S (S Z)), S (S (S (S Z)))}, etc, there's simply no instance for `IntoLR`. (If you want a helpful error message, of course easy enough to add failure instances.) For completeness, I'll give the Instance Guard version for `CountF` and `Into`: > type family {-# INSTANCEGUARD #-} CountF f g :: Nat > type instance CountF f f = (S Z) > type instance CountF f (g :+: h) | f /~ (g :+: h) > = Plus (CountF f g) (CountF f h) > type instance CountF f g | f /~ g, g /~ (_ :+: _) = Z > type family {#- INSTANCEGUARD -#} Into f g > type instance Into f f = Refl > type instance Into f (g :+: h) | f /~ (g :+: h) > = IntoLR f (g :+: h) (CountF f g) (CountF f h) Those families/instances could be Associated types, grounded in the class instances (also guarded). Now I can see my way to translating this into Haskell 2010. AntC

1 0

Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]
by Anthony Clayden 04 Jun '17

04 Jun '17

[starting a new thread for this topic] > On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote: >> On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote: >> else f :<: g fails if f :<: g >> Haskell very strictly doesn't support instance contexts >> driving selection of instances. > Haskell instance selection ... > if you apply the same restriction to instance chains ... What was confusing me is that there's a fault in the instance definitions for the Swierstra encoding as appears in the 2010 Instance Chains paper. I see in your 2015 paper that's been fixed. But before I go on to discuss, is there a typo in the 2015 paper? Figure 6 line 6 shows a type family equation > IsIn f g = Yep That's supposed to mirror the Instance Chains solution Figure 3 line 6: > else f `In` g fails So Figure 6/line 6's `Yep` should be a `Nope`?? Ok what was the fault in the 2010 paper? It correctly failed `instance f :<: (f :+: f)`, because that's ambiguous as to whether the wanted `f` should match left or right of `:+:`. But it didn't fail `instance f :<: ((f :+: f) :+: f)`, because from the failure above, the left operand of the outer `:+:`, viz `(f :+: f)`, is not an instance. So `f :<: ((fail) :+: f)` succeeds. I think this shows that using class instances to both define methods and drive selection logic can fail to separate concerns. You wrote [on the GCD thread]: >>>>> Of course, you'll have an easier time of it >>>>> if you limit yourself to only considering type-level definitions, >>>>> and not the corresponding method definitions. >>>>> But doing so rather misses the point of instance chains. It seems to me that in the 2010 paper, the fault arises from considering only the method definitions and failing to pay attention to the type-level. And yes, I want to make an easy time as possible for the programmer -- both writing and especially reading code. The second approach in the 2015 paper using a case-preparing Type Family seems to me to cleanly impose a phase distinction first type-level calculation then class instance selection/method overloading. So my end-game is to be able to remove FunDeps from the language, in favour of class and instance contexts giving Type Families with Equality constraints. (By all means, let's encourage those Type Families to be Associated within classes, per your Partiality paper with Richard.) To achieve that we need better support for overlaps. We need to do that in an understandable way for the programmer. That is, the 'umble programmer like me, not needing an advanced PhD in abstruse type theory. I think Instance Guards help readability by putting the instance selection criteria all in the one place at the instance head; not reliant on the reader scanning through a prior chain of instances/elses. > ... there is no reason to imagine that using > either instance chains or closed type families > would be any obstacle to implementing them. [viz extensible variants/co-products] No I'm not suggesting any lack of capability. If anything, Instance Chains are _too_ powerful. I'm working on showing how the Swierstra encoding could be catered for in Haskell 2010 + MPTCs+TypeEq. That is, was achievable in GHC 2004. (I could do with a few extra milli-Olegs of brain power.) It's a debate about whether/why/how we introduce syntactic sugar into current capability vs introducing a heretofore avoided feature into type inference viz: type class membership driving instance selection, as opposed to currently: types driving instance selection. AntC

2 1

Avoiding orphan instances and dependency blowups
by Clinton Mead 04 Jun '17

04 Jun '17

Hi All Consider this common situation. 1. Class C in package A. 2. A data type D in package B. 3. There is a clear instance C D but: 4. We do not want A to depend on B as most users of A do not use B. 5. We do not want B to depend on A as most users of B do not use A. Currently the proposed solutions are: 1. Create a third package, say AB, that depends on both A and B, wrap D in a newtype, and define an instance there. 2. Create a third package, say AB, that depends on both A and B as above, but instead create an orphan instance C D in this package. 3. Just give in and either make A depend on B or B depend on A. None of these solutions seem very satisfying. The first one, wrapping D in a newtype, destroys much of the interoperability that is attempting to be achieved by defining the instance in the first place. The second solution uses orphan instances and for a variety of reasons many seem to suggest these should be avoided. The third option introduces a snowball of dependencies that the vast majority of the time will be completely unused. I've heard some conversations of changes to GHC to deal with this, like "authoritative instances" but nothing seems to have come of it? I thought to myself, maybe this is a problem that could be solved by the package manager, not GHC. Here's the draft of how this could work: 1. Create a package, AB, that depends on A and B, but passes an "option" to B, in this case "A". So the dependencies of AB are A and B(A). 2. The package B defines the instance C D, but wrapped in some preprocessor #ifdef style macros. 3. The package manager passes the requested flags to B during it's compilation, and those flags trigger the sections of code required to be compiled and also additional dependencies. 4. If a new package is installed adds to the flags of B, B is recompiled. This way, packages could define instances for each other but if those dependencies are not used, they do not need to be compiled. But the user has a way to explicitly activate the instances. My questions: 1. Is this a roughly okay idea? 2. Is there already a better way of doing what I'm proposing (perhaps through backpack which I don't know much about yet)? 3. Is there a way to make this happen currently in Stack or Cabal, perhaps with custom setup scripts, or will this need some significant changes to Stack/Cabal themselves? Clinton

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 04 Jun '17

04 Jun '17

Errk, braino! This: > data HNil = HNil > data HList e l = HList e l Should be: > data HNil = HNil > data HCons e l = HCons e l AntC

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 03 Jun '17

03 Jun '17

> On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote: >> On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote: >> Although your papers/Dissertation cite some of S&S's work, >> you seem unaware of type disequality guards. > Of course we were aware of inequality guards. > They are a special case of the observation in §2.3 > of the instance chains paper about unifying > but non-overlapping instances; §7 of that paper and §7.1 of my > dissertation discuss extending the formal treatment > to accept such instances. Then I'm sorry Garrett, but if any of those refs are intended to be talking about inequality guards, it's so oblique as to have failed to communicate. In particular, you fail to mention them in your dissertation §7.1, first bullet. Example: "The first challenge is to develop a method to represent negative syntactic constraints on types. For example, in the following instance chain > instance C (Maybe t) > else C t "the second clause can only apply to types that are not of the form Maybeτ for some type τ. To pursue this approach, we would need to develop representations and proof rules for such limitations on the instantiation of type variables." I would write that non-Maybe instance as: > instance C t | t /~ (Maybe _) -- underscore = anonymous I guess instance chain: > else C t fails if t == (Maybe tau) > -- but that must not introduce typevar `tau` to the environment. The S&S CHR approach did "develop proof rules" to type inequalities (according to the 2002 paper). An explicit inequality guard makes it easy to test whether two instances are apart. > My Hackage survey ("Using Hackage > to inform language design", Haskell 2010) > discovered that 85% of overlapping instances were > contained within the same module, ... Well of course they are! Putting overlapping instances in separate modules is disastrous, everybody knows that. There's a thorough write-up from SPJ here https://mail.haskell.org/pipermail/haskell-cafe/2010-July/080043.html That does not prove people _want_ to restrict the instances to a single module. They have no choice in practice. So I'm surprised there's as much as 15% of overlapping instances in separate modules. I shudder at the incoherence. If you surveyed a joinery and found everything held together with nails, that would reflect only that there were no screwdrivers on the premisses. > motivating the formalization of that > usage pattern with instance chains. No. I would say (to both Instance Chains and Closed Type Families/Classes): motivating to support something less restrictive. Viz the ability to write stand-alone instances, that can be verified to not overlap (taking guards into account), same approach as the classes in the standard libraries. (Note how the monad transformers library was re-architected, to avoid the dangers of importing overlaps.) AntC

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 03 Jun '17

03 Jun '17

> On Fri Jun 2 13:48:43 UTC 2017, Richard Eisenberg wrote: > I'm going to respond just to the few points that concern > me directly. > Thanks Richard, blige! there's a lot to catch up with. > > On Jun 2, 2017, at 9:34 AM, Anthony Clayden wrote: > >>> There's a persistent problem for the compiler > >>> testing for type equality: > >>> the usage sites must have the types grounded. > >>> It's often more successful to prove disequality. > > > > That's straight out of the HList paper [2], > > Section 9 "By chance or by design?". > > "We should point out however groundness issues. > > If TypeEq is to return HTrue, the types must be > > ground; TypeEq can return HFalse even for unground > > types, provided they are instantiated enough to > > determine that they are not equal." > > While this may be true for HList's TypeEq, it is not true > for closed type families. If we have > > > type family Equals a b where > > Equals a a = True > > Equals a b = False > HList's TypeEq is comparable from 2004!, using typeclasses/FunDeps/Overlaps: > class TypeEq a b p | a b -> p where > instance TypeEq a a HTrue > instance (p ~ HFalse) => TypeEq a b p The False instance needs bare typevar `p` so that it overlaps; consequently needs UndecidableInstances. (I've used (~), but that was a typecast class in 2004.) > then (Equals [a] [a]) will reduce to True, even if `a` is > universally bound. Indeed, even (Equals a a) will reduce > to True. So there is no groundness issue any more. > Great stuff! And that TypeEq behaves likewise now. I was trying to cast the discussion back to ~2010, the Instance Chains work. IIRC groundedness was still a difficulty then. > > > >> and also: > > > >>> I suspect that for the compiler, > >>> Instance Chains will be as problematic > >>> for type inference as with Closed Type Families: > >>> CTFs have a lot of searching under the covers > >>> to 'look ahead' for equations that can safely match. > > > > That's from Richard, particularly this comment [3]. > > The whole blog post is relevant here, I think. > > I'm not sure where you're getting "look ahead" from. > Closed type families -- and that post, as far as I can > tell -- don't discuss looking ahead. Instead, closed type > families are all about looking *behind*, Well, I think we're saying the same thing. Your last comment on that blog post links to the NewAxioms write-up. That has this example: > type family And (a :: Bool) (b :: Bool) where > And False a = False > And True b = b > And c False = False > And d True = d > And e e = e "All of these equations are compatible, meaning that GHC does not have to do the apartness check against the target." Faced with simplifying `And c False`, does GHC get stuck at the first or second equation, because it can't resolve `c` to `False` or `True`? No, it "looks ahead" to the third equation. Because it sees that if `And c False` unifies with either of the first two, it'll yield the same result `False`. Your comment on the blog post is "coincident overlap within closed type families (the new nomenclature for branched instances) would indeed be useful." I think it would be useful, too, for Instance Chains or Closed Classes. But there's a problem: Class instances must select method implementations, as well type improvement. So we need to fix on a specific instance, even though we only have `And c False`. > > I think the situation has changed with the introduction > > of Type Families. They weren't applicable in 2010. > > So not relevant to the Instance Chains paper. > My mistake: I meant to say "... introduction of Closed Type Families". > Type families were introduced in 2005, I believe. > At least, that's when the papers were written. Hmm, careful. 2005 was Assoc types only. The usually cited paper for Type Families is Schrivers et al 2008. Garrett's papers cite that, not the 2005, and I agree that's the full write-up. But the 2008 paper was written in parallel with development. The feature appeared in GHC after the paper. And it wasn't complete: we waited a long time to get Type Families/(~) in superclass constraints. (There were a couple of release which supported the syntax superclass, but it did nothing.) > I don't know what version of GHC first included them, > but I think it was before 2010. > Vintage ~2010 there was limited support for overlap in TF instances -- the equations had to be "confluent". (This is the (||) example near the top of your blog post, where you conclude "and we can just write || using separate instances, anyway." Yes you could just write separate instances in ~2010.) I don't see that Instance Chains has a comparable notion of "confluent" or "compatible". But perhaps I missed it. > > > > "Look ahead" is exactly what Richard is describing > > in the bulk of that blog post. > > I disagree here: ... See above AntC

1 0

listing include files in a cabal file
by Patrick Pelletier 03 Jun '17

03 Jun '17

I have some C code in my Cabal package, consisting of both *.c and *.h files. Obviously, the *.c files get listed in "c-sources". But I'm trying to figure out where to list the *.h files. Right now, I'm not listing them anywhere, and my package compiles just fine. According to the Cabal users guide, there is an "includes" field and an "install-includes" field. The "includes" field seems to only be relevant when compiling via C. And even when compiling via C, wouldn't the include already be picked up when it is part of the foreign declaration, e. g.: foreign import ccall unsafe "tmr_tag_data.h TMR_bytesToHex" c_TMR_bytesToHex :: Ptr Word8 -> Word32 -> CString -> IO () As for the "install-includes" field, I don't think my header files would need to be installed, because they're internal to my package. The package's interface is entirely in Haskell. Should I just put my include files in "extra-source-files", so they get added to the package, but otherwise aren't treated specially? Or should I be using "includes" and/or "install-includes"? Thanks, --Patrick

2 2

do I need to uninstall haskell-mode before installing intero?
by Dennis Raddle 03 Jun '17

03 Jun '17

I want to try intero with emacs/stack. I have been using haskell-mode. Do I need to uninstall it first--is there any potential conflict? Thanks, D

1 1