- Haskell-Cafe - Haskell.org

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

can this be done with stack?
by Dennis Raddle 02 Jun '17

02 Jun '17

Using stack, but I have a need to build lots of executables. **lots** and new ones all the time .. my application is music playback. I used to have a single executable for playing music, and used it for all compositions. I later found that I needed to do a lot of configuration specific to each composition, and that the most natural language for specifying all the data and functions specific to a composition was Haskell. That means I have a source file for every composition, in the same directory where I store that composition (as a Sibelius file). But a couple things. (1) they aren't in the stack tree, (2) I don't want to add every one of these to a cabal file. What is the best way to approach this goal? D

2 5

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

02 Jun '17

> On Fri Jun 2 10:26:16 UTC 2017, J. Garrett Morris wrote: > This conversation has become deeply mysterious to me. Hi Garrett, thank you for the opportunity to debate the ideas in Instance Chains, and correct any misunderstandings I might have gained. The interaction of Overlapping Instances with other Haskell features has been vexing for a long time. There have been many approaches. I find this continuing situation particularly frustrating, because it seems to me there was an answer in 2002 [1], whose effectiveness was confirmed by the HList work 2004 [2]. I've been banging this drum for a long time [4]. > I understand that you're revisiting arguments on the structuring of conditionals ... No. Until your comment yesterday re Dijkstra (thank you for the tip), I was continuing ideas in the Sulzmann and Stuckey Constraint Handling Rules approach [1]. Although your papers/Dissertation cite some of S&S's work, you seem unaware of type disequality guards. I think that's a significant oversight. > ... that were tried and discarded in the 70s; I can see why Dijkstra's ideas might be discarded for term-level calculation: * the impossibility of determining whether guards are mutually exclusive (that's a specie of the halting problem) * the deliberate non-determinacy But that first objection is not applicable for instances/guards, because they have a very simple semantic structure: pattern-match on the instance head, then type (dis-)unifiability test. The second is a definite plus-feature for instance selection. (Reflecting how GHC works today.) So I'm fully up with the programme of the great programmer. > what I don't understand is why you need > to repeatedly mischaracterize my work to do so. If I'm mischaracterising, I apologise. I note, though, you haven't demurred at my observation that instance chains need backtracking. I find backtracking far more unacceptable than indeterminacy. > For one example, I have no idea why you make the following claim: >> Nevertheless, I can only write one Instance Chain >> per class. So I can't (say in another module) >> introduce a new datatype with instances. > The instance chains paper is quite explicit in ruling out this > interpretation; when introducing the notion of chains, we wrote: > In ilab, a class can be populated by multiple, non-overlapping > instance chains, where each chain may contain multiple clauses > (separated by the keyword else). Then I apologise. The two chief examples in that paper (gcd and the Swierstra encoding) both show a final `else ... fails` branch with a catch-all instance head. Section 3.2 comments "..., closing the Gcd class." For the Swierstra encoding in particular, the algorithm requires the class to be total (it must be closed), so that the recursive descent test/validation for go-left/go-right can be determinate. > For another, you give a fanciful description of the problems that > might arise in implementing instance chains, including: I reject "fanciful". So I'm going to give citations. >> 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." > 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. > Luckily, both instance chains and closed type families have > formalizations that can be checked to evaluate these claims. Yes, Overlapping Instances has suffered for too long from under-/non-formalised semantics. What I'll be doing for Instance Guards is giving a translation into Haskell2010 + MPTCs __without__ overlaps. (I will need to assume, though, a type-level type equality test/total function. You've already commented that's easliy produced.) A serious weakness of Instance Chains, it seems to me, is it can't be translated to existing Haskell. > In neither case do we find either equality limited to ground types > or anything that should be construed as 'look ahead'. 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. "Look ahead" is exactly what Richard is describing in the bulk of that blog post. That is, looking down the sequence of instance equations, to see if any would match and be confluent. This significantly helps progress in inference. If Instance Chains aren't going to be doing that, that's another weakness. > Perhaps you're trying to refer to the use of > infinitary unification in checking apartness (but not in > checking equality) for closed type families? No, infinitary unification is a whole 'nother bag of spanners. I am still goggling at your joint paper with Richard. > Here again, not only is there no use of or need > for infinitary unification with instance chains, ... Good! > but I discussed this difference and its consequences > in my 2015 paper. OK. I've not yet got through that paper. What I do see in the 2010 paper (perhaps this has changed subsequently) is using typeclass membership to determine whether a type is a member of the __same__ class. This seems to be essential to the Swierstra encoding such as: > else f :<: (g :+: h) if f :<: g > else f :<: (g :+: h) if f :<: h Gloss: "f is related to (g :+: h), if f is related to g". And likewise for f related to h. So: * this needs look inside the ( :+: ) to see if f is related to g or to h, or to both (fail) or to neither (fail). And now you tell me there might be other instance chains for `:<:`, so the compiler has to work through them. * it breaks down the 'phase distinctions' in instance selection. I feel very queazy about a recursion like that at the class level. We can express Russell's paradox: > else f :<: g fails if f :<: g Haskell very strictly doesn't support instance contexts driving selection of instances. That is confusing for newbies, but it's for very good decidability reasons. > Finally, you make various claims about what is and is not a solution > to the expression problem which have no apparent relationship to any of > the existing work on the expression problem or its encodings. > ... Again, this is all laid out, with examples, in my 2015 paper. I was being brief. (And this post has gone on plenty long enough, too.) I'll come back and debate that point when I've worked through your 2015 paper. What's strongly motivating me with Haskell is getting the type system to cater for extensible/anonymous records. (I'm a Relational Theorist by trade.) Closed instances (be they Chains or Type Families, or the proposed Closed Classes) are just not going to hack it. Adam G for the Overloaded Records Fields work has eschewed Type Families in favour of FunDeps. That's because it needs to create instances 'on the fly'. Now he hasn't needed overlaps yet (ORF is at an early stage), but anonymous/extensible records will. Just like HList. AntC [1] Sulzmann & Stuckey 2002 "A Theory of Overloading", esp section 8.2 "Overlapping Definitions" [2] Kiselyov et al 2004 "Strongly Typed Heterogeneous Collections" [3] https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-f… [4] https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage

3 2