> 2 days ago Richard Eisenberg (and mniip) wrote:
> ... > On incremental improvements / the "half-baked" nature of > type families: I agree completely. ... ["half-baked" is Richard quoting mniip] > ... the weird place of type families in the language. > It is my hope that Dependent Haskell will obviate > a lot of these concerns, allowing us to deprecate > type families as we know them > (you would just use an ordinary function in types > instead). I don't want to sidetrack the github discussion on mniip's proposal. https://github.com/ghc-proposals/ghc-proposals/pull/52 So please explain here in what way type families are "half baked". The part of type families I find hard to use and hard to reason about is closed type families. I'd be very happy to deprecate them, if there was something that did overlaps better. From what I can make out, though, in Richard's Dissertation, they can't be promoted to "ordinary functions in types". If the closed equations were ordinary functions in types, you could go: > type family F a b > type instance F Int b = b > type instance F a Bool | a /~ Int = a > -- non-unifiability guard With no need for a closed sequence of choices. Is this the "case-like computations" others talk about on the proposal? AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
> On May 12, 2017, at 6:46 AM, Anthony Clayden <[hidden email]> wrote: > > So please explain here in what way > type families are "half baked". My interpretation of mniip’s use of this descriptor was a reference to the fact that type families aren’t just functions, don’t support `case`, can’t be partially applied, etc. Instead, we should just be able to use functions in types. :) I agree that closed type families are bizarre and perhaps a misfeature -- though I think they are a good incremental step toward something better. What would be far better is if we could just use `case`, and then the closed type family syntax would desugar into case statements, much like how normal functions work. So type family F a b where F Int b = b F a Bool = a (AntC’s example) would really mean type F a b = case a of Int -> b _ -> case b of Bool -> a _ -> F a b We understand the semantics of case expressions, so this would avoid the bizarreness of closed type families. (We would also have to eliminate non-linear patterns, replacing them with some other first-class test for equality. It’s currently unclear to me how to do this right. Section 5.13.2 of my thesis dwells on this, without much in the way of a concrete way forward.) AntC’s proposed disequality constraints then become straightforward pattern guards. Richard _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
On Fri, May 12, 2017 at 01:22:35PM -0400, Richard Eisenberg wrote:
> > > On May 12, 2017, at 6:46 AM, Anthony Clayden <[hidden email]> wrote: > > > > So please explain here in what way > > type families are "half baked". > > My interpretation of mniip’s use of this descriptor was a reference to the fact that type families aren’t just functions, don’t support `case`, can’t be partially applied, etc. Instead, we should just be able to use functions in types. :) That is very much correct, but what I was exactly referring to was not the necessary limitations of type families (such as inability of partial application) but rather their unnecessary limitations. For example only being able to pattern-match at the top-level, or, with InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type injectivity. > I agree that closed type families are bizarre and perhaps a misfeature -- though I think they are a good incremental step toward something better. Closed type families have proven very useful to me, so I don't agree with calling them a misfeature, however I can see where you're coming from : throughout the entire language we enforce the notion that we can't have a "proof of type inequality" and then closed type families give us just that. Indeed, their semantics could be made more apparent. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:
> > > On May 12, 2017, at 6:46 AM, Anthony Clayden wrote: > > So please explain here in what way > > type families are "half baked". > > My interpretation of mniip's use of this descriptor was > a reference to the fact that type families aren't just > functions, don't support `case`, ... ?? But the instance mechanism is in effect case; only considerably more powerful: > I agree that closed type families are bizarre and perhaps > a misfeature -- though I think they are a good incremental > step toward something better. What would be far better is > if we could just use `case`, and then the closed type > family syntax would desugar into case statements, much > like how normal functions work. So > > type family F a b where > F Int b = b > F a Bool = a > > (AntC's example) would really mean > > type F a b = case a of > Int -> b > _ -> case b of > Bool -> a > _ -> F a b > But this is terrible for type improvement!: It insists on working through the args left to right. And through the equations top to bottom. Contrast all the good work Richard did for closed families, to 'look ahead', detect confluence of equations, and try to make progress in solving equations. As described here https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/ and in the 2013 paper. i.e. to mimic the behaviour of stand-alone instances. > We understand the semantics of case expressions, ... At the term level yes. But that semantics is not appropriate at the type level. Type-level programming is somewhat like term level; but quite a lot different. At the term level, we never expect to 'improve' an argument from knowledge of the result. So expecting them to behave the same, or deliberately hobbling type improvement to be like term-level case expressions is just not ergonomic. What's so difficult to understand about instances? The worst mis-feature for me about closed families, is I have to put all the instances together, not alongside the corresponding class instances -- even as associated types. 'Grounding' type instances with methods, and therefore with class instances seems to be a Good Thing, according to these musings https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/ Closed families aren't extensible when I declare a new type. The part of the (class) instance mechanism that's difficult to reason about is overlaps. So the idea of the (dis)equality guards on instances -- which can apply to class or type instances -- is to remove overlaps: essentially, if the heads overlap (are unifiable), the guards must disambiguate which instance to choose. I can't introduce in a different module an instance that overlaps. AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Sat May 13 06:40:47 UTC 2017, mniip wrote3:
>> On Fri, May 12, 2017 at 01:22:35PM -0400, Richard Eisenberg wrote: >> >> My interpretation of mniips use of this descriptor was .. > That is very much correct, but what I was exactly referring to was not > the necessary limitations of type families (such as inability of partial > application) but rather their unnecessary limitations. For example only > being able to pattern-match at the top-level, or, with > InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type injectivity. Don't we get limited injectivity through type family calls appearing in Equality constraints? > class (F a b ~ c) => C a b c We might have: > type instance F Int b = b And a use site which gives (a ~ Int). Then we can improve via (b ~ c). >> I agree that closed type families are bizarre and perhaps a misfeature >> -- though I think they are a good incremental step toward something better. > Closed type families have proven very useful to me, ... Thanks mniip. Yes useful to me too. (As a major user of HList-alikes.) > so I don't agree with calling them a misfeature, ... I think there were plenty of people suggesting other ways to achieve the same end. If "something better" comes out of the experience, we've lost 7~8 years of opportunity. > however I can see where you're coming from : > throughout the entire language we enforce the notion that we > can't have a "proof of type inequality" and then > closed type families give us just that. I don't like calling it "type inequality". It's proof of non-unifiability. And the rules for that are easy to write down. (Admittedly a bit messy to apply in practice.) The key fact is that Oleg et al demonstrated how it worked way back in 2004. And it works in Hugs! I don't see what's so hard. > Indeed, their semantics could be made more apparent. Disequality guards make it blimmin obvious. As described in Sulzmann & Stuckey 2002. AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:
> > ... [in] closed type families. (We > would also have to eliminate non-linear patterns, > replacing them with some other first-class test for > equality. > AntC's proposed disequality constraints then become > straightforward pattern guards. Guards don't have to be just disequalities. If you want to eliminate non-linear patterns, use _equality_ guards. Full example: > type family F a b where > F a a = a > F Int b = b > F a Bool = a > Translates to: > type instance F a b | a ~ b = a > type instance F a b | a ~ Int, a /~ b = b > type instance F a b | b ~ Bool, a /~ Int, a /~ b = a (Each instance after the first has disequality guards to negate the earlier instances' equalities., i.e. the earlier instances 'shadow' the overlap.) > It's currently unclear to me how to do this > right. ... > Assuming we have a primitive type-level equality test (?~), returning type-level Bool; we can use helper functions. The first instance desugars to a call > ... = F_a_b_Eq (a ?~ b) a b > type instance F_a_b_Eq True a b = a (Needs UndecidableInstances.) > Section 5.13.2 of my thesis dwells on this, without > much in the way of a concrete way forward.) We use type equality testing all the time. In fact instance selection relies on it. 5.13.2 says: "they [equality testing rules] cannot handle the case where Equals a a reduces to True, where a is locally bound type variable." ?? I thought GHC's equality test requires types to be grounded, i.e. not merely type vars, in order to be judged equal. Or did that change recently? Isn't that to do with impredicativity and the dreaded monomorphism: the same typevar might get a different forall-qualified type in different use sites. Contrast types can be judged dis-equal without necessarily being grounded. [HList paper section 9 refers.] AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Lots to respond to!
I do think think there's one overarching question/theme here: Do we want functional dependencies or type-level functions? Behind AntC's arguments, I see a thrust toward functional dependencies. (Not necessarily their *syntax*, but the idea of type improvement and flexible -- that is, multidirectional -- type-level reasoning.) My dependent types work pushes me toward type-level functions. But I think we can have our cake and eat it too. See my recent draft paper (expanding on the "What are type families" blog post) here: http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf (This paper will appear in revised form at ICFP'17.) While the paper skirts around the issue somewhat, it's really proposing dropping type families in favor of functional dependencies -- but only for partial type families. The key observation is this: partiality in types is bizarre, and we don't want it. So, any time we use a partial type family, you need to have a class constraint around. The class constraint ensures that we evaluate the type family only within its defined domain. Now tied to classes, partial type families are more like convenient syntax for functional dependencies. There is also treatment of partial closed type families via a new construct, closed classes (somewhat like instance chains but weaker). I expect AntC would prefer disequality guards over closed classes. I would be interested to hear more from the community on this choice -- they're really the same as ordered equations under the hood, and it's just a choice of syntax. Maybe we can even have both. Now, on to individual points: > But this is terrible for type improvement!: I agree that desugaring to `case` expressions would harm type improvement. But it gives us a reliable semantics for type-level computation, something that is sorely lacking today. Can we reconcile these? Perhaps, but it will take some Hard Thought. In any case, any real implementation of these ideas would require the Hard Thought in order to be backward compatible. (This backward compatibility necessity is one of the reasons I love working with Haskell. When adding a feature to the language, we just can't take easy ways out!) > Closed families aren't extensible > when I declare a new type. Quite true, but it's easy enough to make an open type family that calls a closed type family. In the design of closed type families, we originally thought to have (what I called) branched instances, separating out the "closedness" with the overlapping equations. In the end, it seemed simpler to have closed families have the overlapping equations and dispense with branches instances. The big problem with branched instances is that it was awkward to describe the overlap between two branched instances. AntC might argue that, if we just had disequality guards, it would all be much simpler. He might be right. In retrospect, it would have been nice to have the proposals process active when designing closed type families; we might have come up with a better design. >> so I don't agree with calling [closed type families] a misfeature, ... > > I think there were plenty of people > suggesting other ways to achieve the same end. > If "something better" comes out of the experience, > we've lost 7~8 years of opportunity. By "misfeature", I didn't mean that I shouldn't have added closed type families. I'm more referring to some of the oddities pointed out in my draft paper linked above. My recollection at the time is that other approaches were more functional-dependency-like in character. (To wit: instance chains.) When I did the closed type family work, I was thinking that type families were better than functional dependencies; now, my view is much more nuanced (leaning strongly toward fundeps instead of partial type families). I'm not sure what you mean by "lost 7~8 years of opportunity". > I don't like calling it "type inequality". > It's proof of non-unifiability. I call it apartness! > I don't see what's so hard [about non-unifiability]. It's not nearly as hard from a fundep point of view. That's because there's a very key difference in fundep-land. Suppose we have > type family F a where > F Int = Bool and that's it. We can still use `F Char` in a type, even though it's nonsensical. Similarly, if a type family doesn't terminate, we can use the type family at a type that causes it to loop. If we translate the type families to fundeps, these problems go away (say, to `class C a b | a -> b; instance C Int Bool`), because a function with a type that mentions `C Char a` can never be called, as there is no `C Char xyz` instance. The key mistake behind the closed type families paper is, essentially, to assume that `F Char` is a type; all the apartness gobbledegook follows. In my draft paper, we reverse this assumption, cleaning up this theory quite nicely. > 5.13.2 says: "they [equality testing rules] cannot handle > the case where Equals a a reduces to True, > where a is locally bound type variable." > > ?? I thought GHC's equality test > requires types to be grounded, > i.e. not merely type vars, > in order to be judged equal. > Or did that change recently? No change here -- since the advent of closed type families, GHC has been able to reduce equality over non-ground types. That's the trouble. > Isn't that to do with impredicativity > and the dreaded monomorphism: > the same typevar might get a different > forall-qualified type in different use sites. Not sure what you're talking about here. GHC is resolutely predicative (in this manner, at least -- a logician would be highly flummoxed that we call a system with Type :: Type predicative!). I do have to say all this talk has made me think more about apartness constraints in FC, at least. They might be a touch simpler than the current story. Richard > On May 14, 2017, at 5:51 AM, Anthony Clayden <[hidden email]> wrote: > >> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote: > >> >> ... [in] closed type families. (We >> would also have to eliminate non-linear patterns, >> replacing them with some other first-class test for >> equality. > >> AntC's proposed disequality constraints then become >> straightforward pattern guards. > > Guards don't have to be just disequalities. > > If you want to eliminate non-linear patterns, > use _equality_ guards. Full example: > >> type family F a b where >> F a a = a >> F Int b = b >> F a Bool = a >> > > Translates to: > >> type instance F a b | a ~ b = a >> type instance F a b | a ~ Int, a /~ b = b >> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a > > (Each instance after the first > has disequality guards to negate the earlier instances' > equalities., i.e. the earlier instances 'shadow' the > overlap.) > >> It's currently unclear to me how to do this >> right. ... >> > > Assuming we have a primitive type-level > equality test (?~), returning type-level Bool; > we can use helper functions. > The first instance desugars to a call > >> ... = F_a_b_Eq (a ?~ b) a b > >> type instance F_a_b_Eq True a b = a > > (Needs UndecidableInstances.) > >> Section 5.13.2 of my thesis dwells on this, without >> much in the way of a concrete way forward.) > > We use type equality testing all the time. > In fact instance selection relies on it. > > 5.13.2 says: "they [equality testing rules] cannot handle > the case where Equals a a reduces to True, > where a is locally bound type variable." > > ?? I thought GHC's equality test > requires types to be grounded, > i.e. not merely type vars, > in order to be judged equal. > Or did that change recently? > > Isn't that to do with impredicativity > and the dreaded monomorphism: > the same typevar might get a different > forall-qualified type in different use sites. > > Contrast types can be judged dis-equal > without necessarily being grounded. > [HList paper section 9 refers.] > > > AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Mon May 15 16:20:09 UTC 2017, Richard Eisenberg wrote:
> Lots to respond to! > Thanks Richard, phew! yes. Let's break it down a bit. > I do think think there's one overarching question/theme > here: Do we want functional dependencies or type-level > functions? Behind AntC's arguments, I see a thrust toward > functional dependencies. (Not necessarily their *syntax*, > but the idea of type improvement and flexible -- that is, > multidirectional -- type-level reasoning.) My dependent > types work pushes me toward type-level functions. Yes there is an overarching question. I don't think it's specifically FunDeps vs Type Functions. (Although I disagree the **Functional** Dependencies are somehow not "functional". Yes Mark Jones got the idea from Relational database theory. Where did Ted Codd get the idea from? Mathematical (binary) "relations", which are a set-theoretic account of, um, functions.) "Multidirectional type-level reasoning" is what all functional languages do: from Robinson's unification to Hindley-Milner to OutsideIn(X) to System F-subscript-superscript. There's been an example in Haskell's Prelude since ~1991: the `read` method's return type is 'demand-pulled' from context, not 'supply-pushed' from its parameter. Similarly if I write: > x :: Int > x = a + (b * c) We infer a, b, c must all be Int. Perhaps in another universe, Haskell had explicit type application from day 1, and insisted on giving type signatures for all vars (like nearly all procedural/OO languages). But we aren't in that universe, and I love Haskell/FP for being both type-safe and not pernickety in that way. > ... [big snip - I'll reply separately] > > I expect AntC would prefer disequality guards > over closed classes. Oh yes! I was about to say (repeating my earlier message): if we're going to ground type family instances in classes, then we need a way to distribute type instances as associated types, unless ... you're going to suggest something daft like closed classes. And then you did. > I would be interested to hear more from the > community on this choice -- they're really the same as > ordered equations under the hood, and it's just a choice > of syntax. Maybe we can even have both. > Yes please all chip in. There were strong views expressed 5~8 years ago. My two-penn'orth: I think we can mechanically translate closed equations to guards (equality and 'apart' tests). The example in my earlier post tried to show how. For class instances (with overlaps), I think there's also a mechanical translation, but only for 'well-behaved' sets of instances. (For Incoherent sets we don't have a chance.) And of course as soon as some imported instance overlaps, we have to start again to assess well-behavedness. > Now, on to individual points: > > ...the Hard Thought in order to be > backward compatible. (This backward compatibility > necessity is one of the reasons I love working with > Haskell. When adding a feature to the language, we just > can't take easy ways out!) > The backwards-compatibility I particularly want to preserve is "distributed instances". That is, putting the instance code close to type decls and other functions that build or consume that type. I also want to put explicitly *in the instance decl* the restraints on what types that instance applies for. Not implicit from where it appears in a closed but lengthy/voluminous sequence of equations. Yes there must be global coherence for the class/type instances. That's a mechanical check which compilers are good at, but humans not so much. > ... it was awkward to describe the overlap between two > branched instances. AntC might argue that, if we just had > disequality guards, it would all be much simpler. He might > be right. I'd argue it's simpler to understand each instance on its own grounds. Although a bunch of guards can get quite complex. (There was Andy A-M's example back in 2013.) The cumulative effect of the preceeding equations in the closed family is more complex. IMO. > > In retrospect, it would have been nice to have the > proposals process active when designing closed type > families; we might have come up with a better design. > There was a huge and rather repetitive (unfortunately) discussion in several rounds 2009~2012, somewhat prompted by trying to 'fix' the Haskell 2010 standard. So that we could include MPTCs in the standard. But you can't have MPTCs without FunDeps or Type Families, or without agreeing a position on overlaps. (good luck with that!) So although MPTCs were in both GHC and Hugs before 1998, they're still not 'official' >sigh<. MPTC's omission for Haskell2010 is what I meant by: > > we've lost 7~8 years of opportunity. > > My recollection at the time [of developing closed Families] > is that other approaches were > more functional-dependency-like in character. (To wit: > instance chains.) I wish Martin Sulzmann could have been more active at the time. (He occasionally expresses the intention of getting back into Haskell.) Instance guards are really a continuation of the CHR approach. So fit nicely into whole-of-program inference with type improvement. [I dislike the non-distributivity of instance chains for the same reason I dislike closed families. Although instance chains do have some nice features. Instance guards give me that feature more directly. Whereas closed type families don't give that feature at all.] > When I did the closed type family work, > I was thinking that type families were better than > functional dependencies; now, my view is much more nuanced > (leaning strongly toward fundeps instead of partial type > families). > I'm a little unsure what you mean at the top of the post about the "idea" of FunDeps vs their specific syntax. I can simulate FunDeps with superclass constraints using Type Funs and Equality constraints. This even achieves multi-directional improvement. Is that what you want to include? It took me a long time to realise this works out better than the FunDeps arrow business, especially with overlaps. The dreaded "Instances inconsistent with FunDeps" error is a devil to fiddle with. And often ends up breaking the coverage condition. [As Iavor frequently points out.] Martin pointed out that breaking coverage (using UndecidableInstances) is not as 'safe' as SPJ had been assuming. > > > I don't see what's so hard [about non-unifiability]. > > It's not nearly as hard from a fundep point of view. ... > ... [another big snip: thanks for the pointer to the paper.] > > I do have to say all this talk has made me think more > about apartness constraints in FC, at least. They might be > a touch simpler than the current story. > I think apartness is the criterion that's always applied to resolve instance selection under overlaps. The trouble is that the semantics for overlap has never been spelled out. (Nor, I suspect the criterion for a 'well-behaved' set of instances. I can volunteer that for you.) Apartness does not intrude inside constraints in the class/instance contexts, nor inside the body of a class instance/methods. It might help with instance selection wrt the rhs of type instance equations. AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Richard Eisenberg-4
If partial type families can be a problem, then how do you verify
totality, especially considering that Any is a member of every kind, so you might have to check for F Any, F (Any Int), F (Any (Any 7) 'Just), and so on? On Mon, May 15, 2017 at 11:20 AM, Richard Eisenberg <[hidden email]> wrote: > Lots to respond to! > > I do think think there's one overarching question/theme here: Do we want functional dependencies or type-level functions? Behind AntC's arguments, I see a thrust toward functional dependencies. (Not necessarily their *syntax*, but the idea of type improvement and flexible -- that is, multidirectional -- type-level reasoning.) My dependent types work pushes me toward type-level functions. > > But I think we can have our cake and eat it too. See my recent draft paper (expanding on the "What are type families" blog post) here: http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf (This paper will appear in revised form at ICFP'17.) While the paper skirts around the issue somewhat, it's really proposing dropping type families in favor of functional dependencies -- but only for partial type families. The key observation is this: partiality in types is bizarre, and we don't want it. So, any time we use a partial type family, you need to have a class constraint around. The class constraint ensures that we evaluate the type family only within its defined domain. Now tied to classes, partial type families are more like convenient syntax for functional dependencies. There is also treatment of partial closed type families via a new construct, closed classes (somewhat like instance chains but weaker). > > I expect AntC would prefer disequality guards over closed classes. I would be interested to hear more from the community on this choice -- they're really the same as ordered equations under the hood, and it's just a choice of syntax. Maybe we can even have both. > > Now, on to individual points: > >> But this is terrible for type improvement!: > > I agree that desugaring to `case` expressions would harm type improvement. But it gives us a reliable semantics for type-level computation, something that is sorely lacking today. Can we reconcile these? Perhaps, but it will take some Hard Thought. In any case, any real implementation of these ideas would require the Hard Thought in order to be backward compatible. (This backward compatibility necessity is one of the reasons I love working with Haskell. When adding a feature to the language, we just can't take easy ways out!) > >> Closed families aren't extensible >> when I declare a new type. > > Quite true, but it's easy enough to make an open type family that calls a closed type family. In the design of closed type families, we originally thought to have (what I called) branched instances, separating out the "closedness" with the overlapping equations. In the end, it seemed simpler to have closed families have the overlapping equations and dispense with branches instances. The big problem with branched instances is that it was awkward to describe the overlap between two branched instances. AntC might argue that, if we just had disequality guards, it would all be much simpler. He might be right. > > In retrospect, it would have been nice to have the proposals process active when designing closed type families; we might have come up with a better design. > >>> so I don't agree with calling [closed type families] a misfeature, ... >> >> I think there were plenty of people >> suggesting other ways to achieve the same end. >> If "something better" comes out of the experience, >> we've lost 7~8 years of opportunity. > > By "misfeature", I didn't mean that I shouldn't have added closed type families. I'm more referring to some of the oddities pointed out in my draft paper linked above. My recollection at the time is that other approaches were more functional-dependency-like in character. (To wit: instance chains.) When I did the closed type family work, I was thinking that type families were better than functional dependencies; now, my view is much more nuanced (leaning strongly toward fundeps instead of partial type families). > > I'm not sure what you mean by "lost 7~8 years of opportunity". > >> I don't like calling it "type inequality". >> It's proof of non-unifiability. > > I call it apartness! > >> I don't see what's so hard [about non-unifiability]. > > It's not nearly as hard from a fundep point of view. That's because there's a very key difference in fundep-land. Suppose we have > >> type family F a where >> F Int = Bool > > and that's it. We can still use `F Char` in a type, even though it's nonsensical. Similarly, if a type family doesn't terminate, we can use the type family at a type that causes it to loop. If we translate the type families to fundeps, these problems go away (say, to `class C a b | a -> b; instance C Int Bool`), because a function with a type that mentions `C Char a` can never be called, as there is no `C Char xyz` instance. The key mistake behind the closed type families paper is, essentially, to assume that `F Char` is a type; all the apartness gobbledegook follows. In my draft paper, we reverse this assumption, cleaning up this theory quite nicely. > >> 5.13.2 says: "they [equality testing rules] cannot handle >> the case where Equals a a reduces to True, >> where a is locally bound type variable." >> >> ?? I thought GHC's equality test >> requires types to be grounded, >> i.e. not merely type vars, >> in order to be judged equal. >> Or did that change recently? > > > No change here -- since the advent of closed type families, GHC has been able to reduce equality over non-ground types. That's the trouble. > >> Isn't that to do with impredicativity >> and the dreaded monomorphism: >> the same typevar might get a different >> forall-qualified type in different use sites. > > Not sure what you're talking about here. GHC is resolutely predicative (in this manner, at least -- a logician would be highly flummoxed that we call a system with Type :: Type predicative!). > > > I do have to say all this talk has made me think more about apartness constraints in FC, at least. They might be a touch simpler than the current story. > > Richard > > >> On May 14, 2017, at 5:51 AM, Anthony Clayden <[hidden email]> wrote: >> >>> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote: >> >>> >>> ... [in] closed type families. (We >>> would also have to eliminate non-linear patterns, >>> replacing them with some other first-class test for >>> equality. >> >>> AntC's proposed disequality constraints then become >>> straightforward pattern guards. >> >> Guards don't have to be just disequalities. >> >> If you want to eliminate non-linear patterns, >> use _equality_ guards. Full example: >> >>> type family F a b where >>> F a a = a >>> F Int b = b >>> F a Bool = a >>> >> >> Translates to: >> >>> type instance F a b | a ~ b = a >>> type instance F a b | a ~ Int, a /~ b = b >>> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a >> >> (Each instance after the first >> has disequality guards to negate the earlier instances' >> equalities., i.e. the earlier instances 'shadow' the >> overlap.) >> >>> It's currently unclear to me how to do this >>> right. ... >>> >> >> Assuming we have a primitive type-level >> equality test (?~), returning type-level Bool; >> we can use helper functions. >> The first instance desugars to a call >> >>> ... = F_a_b_Eq (a ?~ b) a b >> >>> type instance F_a_b_Eq True a b = a >> >> (Needs UndecidableInstances.) >> >>> Section 5.13.2 of my thesis dwells on this, without >>> much in the way of a concrete way forward.) >> >> We use type equality testing all the time. >> In fact instance selection relies on it. >> >> 5.13.2 says: "they [equality testing rules] cannot handle >> the case where Equals a a reduces to True, >> where a is locally bound type variable." >> >> ?? I thought GHC's equality test >> requires types to be grounded, >> i.e. not merely type vars, >> in order to be judged equal. >> Or did that change recently? >> >> Isn't that to do with impredicativity >> and the dreaded monomorphism: >> the same typevar might get a different >> forall-qualified type in different use sites. >> >> Contrast types can be judged dis-equal >> without necessarily being grounded. >> [HList paper section 9 refers.] >> >> >> AntC > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Although I am waiting for enough time to adequately respond to AntC's latest volley, I can nab this one:
> On May 18, 2017, at 4:59 PM, Zemyla <[hidden email]> wrote: > > If partial type families can be a problem, then how do you verify > totality, especially considering that Any is a member of every kind, > so you might have to check for F Any, F (Any Int), F (Any (Any 7) > 'Just), and so on? Totality is a combination of coverage and termination. It seems you are worried about coverage here -- are all possible patterns considered? However, Any doesn't pose a problem here. Because Any is an empty closed type family, it cannot appear on the left-hand side of a type family instance. (This is a change from how it was, once upon a time. But it's been this way for several releases, I think.) Termination, on the other hand, is a hard nut to crack. I offer no new nutcrackers, I'm afraid. Richard > > On Mon, May 15, 2017 at 11:20 AM, Richard Eisenberg <[hidden email]> wrote: >> Lots to respond to! >> >> I do think think there's one overarching question/theme here: Do we want functional dependencies or type-level functions? Behind AntC's arguments, I see a thrust toward functional dependencies. (Not necessarily their *syntax*, but the idea of type improvement and flexible -- that is, multidirectional -- type-level reasoning.) My dependent types work pushes me toward type-level functions. >> >> But I think we can have our cake and eat it too. See my recent draft paper (expanding on the "What are type families" blog post) here: http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf (This paper will appear in revised form at ICFP'17.) While the paper skirts around the issue somewhat, it's really proposing dropping type families in favor of functional dependencies -- but only for partial type families. The key observation is this: partiality in types is bizarre, and we don't want it. So, any time we use a partial type family, you need to have a class constraint around. The class constraint ensures that we evaluate the type family only within its defined domain. Now tied to classes, partial type families are more like convenient syntax for functional dependencies. There is also treatment of partial closed type families via a new construct, closed classes (somewhat like instance chains but weaker). >> >> I expect AntC would prefer disequality guards over closed classes. I would be interested to hear more from the community on this choice -- they're really the same as ordered equations under the hood, and it's just a choice of syntax. Maybe we can even have both. >> >> Now, on to individual points: >> >>> But this is terrible for type improvement!: >> >> I agree that desugaring to `case` expressions would harm type improvement. But it gives us a reliable semantics for type-level computation, something that is sorely lacking today. Can we reconcile these? Perhaps, but it will take some Hard Thought. In any case, any real implementation of these ideas would require the Hard Thought in order to be backward compatible. (This backward compatibility necessity is one of the reasons I love working with Haskell. When adding a feature to the language, we just can't take easy ways out!) >> >>> Closed families aren't extensible >>> when I declare a new type. >> >> Quite true, but it's easy enough to make an open type family that calls a closed type family. In the design of closed type families, we originally thought to have (what I called) branched instances, separating out the "closedness" with the overlapping equations. In the end, it seemed simpler to have closed families have the overlapping equations and dispense with branches instances. The big problem with branched instances is that it was awkward to describe the overlap between two branched instances. AntC might argue that, if we just had disequality guards, it would all be much simpler. He might be right. >> >> In retrospect, it would have been nice to have the proposals process active when designing closed type families; we might have come up with a better design. >> >>>> so I don't agree with calling [closed type families] a misfeature, ... >>> >>> I think there were plenty of people >>> suggesting other ways to achieve the same end. >>> If "something better" comes out of the experience, >>> we've lost 7~8 years of opportunity. >> >> By "misfeature", I didn't mean that I shouldn't have added closed type families. I'm more referring to some of the oddities pointed out in my draft paper linked above. My recollection at the time is that other approaches were more functional-dependency-like in character. (To wit: instance chains.) When I did the closed type family work, I was thinking that type families were better than functional dependencies; now, my view is much more nuanced (leaning strongly toward fundeps instead of partial type families). >> >> I'm not sure what you mean by "lost 7~8 years of opportunity". >> >>> I don't like calling it "type inequality". >>> It's proof of non-unifiability. >> >> I call it apartness! >> >>> I don't see what's so hard [about non-unifiability]. >> >> It's not nearly as hard from a fundep point of view. That's because there's a very key difference in fundep-land. Suppose we have >> >>> type family F a where >>> F Int = Bool >> >> and that's it. We can still use `F Char` in a type, even though it's nonsensical. Similarly, if a type family doesn't terminate, we can use the type family at a type that causes it to loop. If we translate the type families to fundeps, these problems go away (say, to `class C a b | a -> b; instance C Int Bool`), because a function with a type that mentions `C Char a` can never be called, as there is no `C Char xyz` instance. The key mistake behind the closed type families paper is, essentially, to assume that `F Char` is a type; all the apartness gobbledegook follows. In my draft paper, we reverse this assumption, cleaning up this theory quite nicely. >> >>> 5.13.2 says: "they [equality testing rules] cannot handle >>> the case where Equals a a reduces to True, >>> where a is locally bound type variable." >>> >>> ?? I thought GHC's equality test >>> requires types to be grounded, >>> i.e. not merely type vars, >>> in order to be judged equal. >>> Or did that change recently? >> >> >> No change here -- since the advent of closed type families, GHC has been able to reduce equality over non-ground types. That's the trouble. >> >>> Isn't that to do with impredicativity >>> and the dreaded monomorphism: >>> the same typevar might get a different >>> forall-qualified type in different use sites. >> >> Not sure what you're talking about here. GHC is resolutely predicative (in this manner, at least -- a logician would be highly flummoxed that we call a system with Type :: Type predicative!). >> >> >> I do have to say all this talk has made me think more about apartness constraints in FC, at least. They might be a touch simpler than the current story. >> >> Richard >> >> >>> On May 14, 2017, at 5:51 AM, Anthony Clayden <[hidden email]> wrote: >>> >>>> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote: >>> >>>> >>>> ... [in] closed type families. (We >>>> would also have to eliminate non-linear patterns, >>>> replacing them with some other first-class test for >>>> equality. >>> >>>> AntC's proposed disequality constraints then become >>>> straightforward pattern guards. >>> >>> Guards don't have to be just disequalities. >>> >>> If you want to eliminate non-linear patterns, >>> use _equality_ guards. Full example: >>> >>>> type family F a b where >>>> F a a = a >>>> F Int b = b >>>> F a Bool = a >>>> >>> >>> Translates to: >>> >>>> type instance F a b | a ~ b = a >>>> type instance F a b | a ~ Int, a /~ b = b >>>> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a >>> >>> (Each instance after the first >>> has disequality guards to negate the earlier instances' >>> equalities., i.e. the earlier instances 'shadow' the >>> overlap.) >>> >>>> It's currently unclear to me how to do this >>>> right. ... >>>> >>> >>> Assuming we have a primitive type-level >>> equality test (?~), returning type-level Bool; >>> we can use helper functions. >>> The first instance desugars to a call >>> >>>> ... = F_a_b_Eq (a ?~ b) a b >>> >>>> type instance F_a_b_Eq True a b = a >>> >>> (Needs UndecidableInstances.) >>> >>>> Section 5.13.2 of my thesis dwells on this, without >>>> much in the way of a concrete way forward.) >>> >>> We use type equality testing all the time. >>> In fact instance selection relies on it. >>> >>> 5.13.2 says: "they [equality testing rules] cannot handle >>> the case where Equals a a reduces to True, >>> where a is locally bound type variable." >>> >>> ?? I thought GHC's equality test >>> requires types to be grounded, >>> i.e. not merely type vars, >>> in order to be judged equal. >>> Or did that change recently? >>> >>> Isn't that to do with impredicativity >>> and the dreaded monomorphism: >>> the same typevar might get a different >>> forall-qualified type in different use sites. >>> >>> Contrast types can be judged dis-equal >>> without necessarily being grounded. >>> [HList paper section 9 refers.] >>> >>> >>> AntC >> >> _______________________________________________ >> Haskell-Cafe mailing list >> To (un)subscribe, modify options or view archives go to: >> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >> Only members subscribed via the mailman list are allowed to post. > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On May 15, 2017, at 9:26 PM, Anthony Clayden <[hidden email]> wrote: > > "Multidirectional type-level reasoning" is what all > functional languages do: from Robinson's unification > to Hindley-Milner to OutsideIn(X) > to System F-subscript-superscript. I disagree here: the dependently typed languages don't quite do this. For them, a type-level function is just that: it has an input that determines the output. These languages still do multi-directional type inference, but not all parts of their type system play so nicely with the multi-directional part. > > I think we can mechanically translate closed equations > to guards (equality and 'apart' tests). > The example in my earlier post > tried to show how. Agreed. > > For class instances (with overlaps), > I think there's also a mechanical translation, > but only for 'well-behaved' sets of instances. > (For Incoherent sets we don't have a chance.) > And of course as soon as some imported instance overlaps, > we have to start again to assess well-behavedness. Agreed. > > The backwards-compatibility I particularly > want to preserve is "distributed instances". > That is, putting the instance code > close to type decls and other functions that > build or consume that type. I think one other key difference between our viewpoints is that I view the whole idea of "type instance" to be a bit backward: I view type families as type-level functions. Like other functions, I want the defining equations to be all in one place. Of course, class methods are distributed in exactly the same way as type instances, but most of my work with type families has not needed the distributed aspect of them. This isn't to argue that my viewpoint is right or that other viewpoints are wrong. It's just a way to understand why we both see things the way we do. > I'd argue it's simpler to understand each instance > on its own grounds. Permit me to rewrite your sentence to something that resonates better with me: > I'd argue it's simpler to understand each *equation* > on its own grounds. I agree here, but it's a bit subtler. We aren't confused when we see > f [] = False > f _ = True even though the meaning of the second equation crucially depends on it appearing after the first. Functional programmers are used to ordering like this. But when things get more complicated, perhaps you're right. > > There was a huge and rather repetitive (unfortunately) > discussion > in several rounds 2009~2012, These dates might help to explain why I may be repeating old arguments. I became active in the community somewhere in 2012. > > I'm a little unsure what you mean at the top of the post > about the "idea" of FunDeps vs their specific syntax. By "idea", I mean traits like multidirectionality and attachment to classes. I maintain that the function-application syntax of type families is better than the relational syntax of fundeps. > A set of instances is well-behaved wrt overlap > iff for each pairing of instances, one of: Thanks for this analysis. I agree. > Rules for guards: > a) The guards are a comma-sep list > of equal (~) or apart (/~) comparisons. > b) The comparands must be same-kinded. > (I'll leave the poly kinded case for Richard ;-) > c) Can only use type vars from the head. > (I.e. not introduce extra vars, which contexts can do.) > d) No type functions -- too hard, and not injective. > e) Can use wildcard `_` as a type place-holder. > f) Can use Type constructors to arbitrary nesting. I agree here, too, though I'm not sure we need to allow ~ guards. (I think allowing them would cause confusion, with many people asking about the difference between an equality constraint and an equality guard. They're different, but I think the equality guard is useless [except as a type-level "let", I suppose].) >> The key observation is this: partiality in types is > bizarre, and we don't want it. ... > > Huh? Nearly all type families (and class instances) are > partial. > You perhaps mean "don't want it" as purist > type-theoreticians(?) Partial type families (including non-terminating ones) are bizarre because they cause wrinkles in the fabric of type families. Some of the strangeness of closed type families (Section 6 of the original Closed Type Families paper) and all of the strangeness of injective type families are caused by partiality. So I dislike partial type families for very practical reasons. Of course, when you protect a partial type family by a class constraint, then it's not troublesome: that's the point of the Constrained Type Families paper. > Sometimes I deliberately want there to be no instance > for some specific pattern. Indeed yes. And now you can, with TypeError (https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors, which is now available in GHC 8). The problem with instance chains is their backtracking capability, but we can have failure without backtracking. > Errk I see a fly in the ointment with these > 'closed classes'/associated types. Suppose: > > A class with two assoc types > * One assoc type needs the instances in a specific sequence. > * The other assoc type needs the instances in a different > sequence. > > Here's a simple (as in daft!) example: Hm. Interesting, illustrative example. Bottom line: You win. I'm convinced. Apartness guards (feel free to fight me on the name here -- I don't feel strongly, but somehow I like "apartness guards" more than "disequality guards") subsume OverlappingInstances (when the author of the instances has a particular desired way to resolve overlap) and closed type families. I think that the syntax of closed type families is often what the user wants, but I admit that CTFs don't cover all scenarios, especially in the context of Constrained Type Families. So I think we should keep CTFs (for now -- until Dependent Haskell is here) but add this new syntax as well, which would subsume the newly-proposed closed type classes. Even better, I think apartness guards would be very easy to implement. All the plumbing is already installed: we basically just have to add a switch. Next step: write a ghc-proposal. I'll support it. If I had the time, I'd even implement it. Thanks for getting me to think about all this in a new way! Richard _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Wed May 24 02:33:46 UTC 2017, Richard Eisenberg wrote:
> ... > Thanks for getting me to think about all this > in a new way! Thanks Richard, yes I think we have large areas of agreement. So I'll cut to where we differ. > > > On May 15, 2017, at 9:26 PM, Anthony Clayden wrote: > > "Multidirectional type-level reasoning" is what all > > functional languages do: from Robinson's unification > > to Hindley-Milner to OutsideIn(X) > > to System F-subscript-superscript. > > I disagree here: the dependently typed languages don't > quite do this. Then I guess I remain to be convinced of the value of dependent typing within Haskell. > ...These languages still do multi-directional type inference, I guess you mean as needed for superclass constraints and instance constraints, so perhaps there's no practical difference. > > > > The backwards-compatibility I particularly > > want to preserve is "distributed instances". > > That is, putting the instance code > > close to type decls and other functions that > > build or consume that type. > > I think one other key difference between our viewpoints is > that I view the whole idea of "type instance" to be a bit > backward: I view type families as type-level functions. > Like other functions, I want the defining equations to be > all in one place. I'd like term-level functions to be more like instances. That is, with the equations distributed, see your example below. (Yes the set of equations must be coherent overall. That's something the compiler can check for me.) > > This isn't to argue that my viewpoint is right or that > other viewpoints are wrong. It's just a way to understand > why we both see things the way we do. Yes. > > > I'd argue it's simpler to understand each instance > > on its own grounds. > > Permit me to rewrite your sentence to something that > resonates better with me: > > > I'd argue it's simpler to understand each *equation* > > on its own grounds. > > I agree here, but it's a bit subtler. > We aren't confused when we see > > > f [] = False > > f _ = True Oh, yes I think a lot of people are confused. I think they expect the second equation is equivalent to: > f (x:xs) = True Maybe even > f ~(x:xs) = True But in the presence of bottom, that's a dangerous delusion. I'd say: if you want the True result to mean there's a non-empty list, then put that explicitly. And then we have two equations that are 'apart'. And they don't need to be sequential. Furthermore that delusion is doubly dangerous for type equations, because GHC knows nothing of closed Data Kinds. > > There was a huge and rather repetitive (unfortunately) > > discussion in several rounds 2009~2012, > > These dates might help to explain why I may be repeating > old arguments. I became active in the community somewhere > > in 2012. No, you're not repeating old arguments. Type Families, and esp. CTFs really came later. IIRC, at the time, there was a lot of suggestions, but not much push-back from anybody disagreeing. There was some doubt whether there could be a type-level disequality test. Chiefly GHC HQ just ignored the whole thing. Somebody at the time did try to write it up (viz. moi) https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage And someone from GHC HQ (viz. you) did acknowledge it rather later. > > I'm a little unsure what you mean at the top of the post > > about the "idea" of FunDeps vs their specific syntax. > > By "idea", I mean traits like multidirectionality and > attachment to classes. I maintain that the > function-application syntax of type families is better > than the relational syntax of fundeps. > OK I think you're saying that a class decl with superclass (~) constraints to type functions is preferable/more aesthetic. I agree. Furthermore overlap interferes with fundeps (or perhaps I mean v.v.) in horrible ways. > ...I'm not sure we need to allow ~ guards. > (I think allowing them would cause confusion, with > many people asking about the difference between an > equality constraint and an equality guard. Yes I can see the dangers of confusion. We could of course use a different operator. > ... They're different, but I think the equality guard is useless I see two main uses/benefits: 1. avoids the need for non-linear patterns in the head 2. visually points up the 'non-apartness' vs an, um. "apartness guard" (When I was figuring out Andy A-M's 2013 example, I rewrote the non-linear patterns with ~ guards, so I could figure out the apartness guards esp for the semi-apart instances. I posted the later workings to your blog https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/#comment-712 ) > [except as a type-level "let", I suppose].) No, they're not doing that: deliberately I don't allow guards to introduce new type vars. > ... partial type families ... > Of course, when you protect a > partial type family by a class constraint, then it's not > troublesome: that's the point of the Constrained Type > Families paper. Yes I got that loud and clear, and I agree. So the remaining issue is _how_ to protect them. > > > Sometimes I deliberately want there to be no instance > > for some specific pattern. > > Indeed yes. And now you can, with TypeError > (https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomType > Errors, which is now available in GHC 8). Ok thanks, yes that helps. Nevertheless it seems disergonomic to write an instance for a type-equal case, even with a helpful error message; when what you want is: no such instance. > > Bottom line: You win. I'm convinced. Apartness guards > (feel free to fight me on the name here -- I don't feel > strongly, but somehow I like "apartness guards" more than > "disequality guards") subsume OverlappingInstances (when > the author of the instances has a particular desired way > to resolve overlap) and closed type families. I think that > the syntax of closed type families is often what the user > wants, but I admit that CTFs don't cover all scenarios, > especially in the context of Constrained Type Families. So > I think we should keep CTFs (for now -- until Dependent > Haskell is here) but add this new syntax as well, which > would subsume the newly-proposed closed type classes. I've been (mostly in my head) calling them "Instance Guards", because I want both an eq guard and an apartness guard. > > Even better, I think apartness guards would be very easy > to implement. All the plumbing is already installed: we > basically just have to add a switch. > Yes that's what I guessed from your write-up of CTFs and "coincident overlap". What I can see will be awkward is backwards compatibility: can a class/type family with guards coexist with CTFs and with classes using overlap? > Next step: write a ghc-proposal. I'll support it. If I had > the time, I'd even implement it. I'll have a crack at the proposal. But implementing it is entirely beyond me. So thanks for saying "you win". But I'm not celebrating 'til something actually happens. (Been bitten too many times.) AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Richard Eisenberg-4
I know I am just jumping in the middle of an already long discussion.
I would like to advise against this idea of apartness guards. I've tried myself some years ago, and I remember them being quite complicated to describe. The main problem is that apartness may end up introducing some sort of backtracking in the type checking process -- something completely undesirable. Furthermore, they make the work of the overlapping checks much harder. Alejandro _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Wed May 24 07:57:09 UTC 2017, Alejandro Serrano Mena
wrote: > I know I am just jumping in the middle of an already long > discussion. Hi Alejandro, your input is very welcome. I know there have been many posts, so Richard's right the idea now needs writing up in detail in one place. > > > > Bottom line: You win. I'm convinced. Apartness guards .. > > > > Even better, I think apartness guards would be very easy > > to implement. All the plumbing is already installed: we > > basically just have to add a switch. > > > I would like to advise against this idea of apartness > guards. I've tried myself some years ago, and I remember > them being quite complicated to describe. ... That's interesting. What did you try? How did you test for apartness? I roughed out the rules a few posts back. Bottom of https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127103.html The body of that post has worked examples. I can also translate guards into Haskell2010 + MPTCs, providing there's a primitive for type-level type comparison. (Which we could write today with Closed Type Families.) See https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127090.html discussion of (?~). This is essentially the 'case-preparing' technique from HList [2004]. > The main problem is that apartness may end up > introducing some sort of backtracking > in the type checking process -- something > completely undesirable. I agree that's not just undesirable, but unacceptable. (Backtracking is a weakness of Instance chains IMO.) With the guards I'm thinking of, an instance either applies at a usage site or does not (after taking guards into account). Or type refinement hasn't advanced enough to decide. Then that instance remains 'in play'. This is exactly the same process as currently. If an instance does apply (with guards) then it is guaranteed to be the only instance. IOW all other instances are excluded. So: > Furthermore, they make the work of > the overlapping checks much harder. The guards remove any need for overlapping checks. Instead the compiler must unify the usage site with the instance head, then substitute into the guards. If a guard comes out false under that subst, reject the instance. If all guards come out true, select the instance. If some guards come out 'not proven', it needs more type refinement. So you can't have OverlappingInstances as well as InstanceGuards. (Or at least not for the same class/type family. That's a bit of backwards compatibility awkwardness I mentioned.) AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
On Wed, May 24, 2017 at 3:13 AM, Anthony Clayden
<[hidden email]> wrote: > > > On Wed May 24 02:33:46 UTC 2017, Richard Eisenberg wrote: > > > I agree here, but it's a bit subtler. > > We aren't confused when we see > > > > > f [] = False > > > f _ = True > > Oh, yes I think a lot of people are confused. > I think they expect the second equation > is equivalent to: > > > f (x:xs) = True > > Maybe even > > > f ~(x:xs) = True > > But in the presence of bottom, > that's a dangerous delusion. I would argue those are equivalent. To get to the second equation, you would have had to reject the first equation, so at that point you already know the argument isn’t bottom. -- Dave Menendez <[hidden email]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On May 24, 2017, at 3:13 AM, Anthony Clayden <[hidden email]> wrote: > > Then I guess I remain to be convinced > of the value of dependent typing within Haskell. The existing dependently typed languages (I'm thinking of Coq, Adga, and Idris -- just not as familiar with F* and perhaps others) do type inference on a best-effort basis, with very little that I have found in the literature describing the type inference process. One of the major challenges of dependent types in Haskell is to continue Haskell's tradition of predictable, describable type inference. In other words, adding dependent types needn't take anything away from the fragment of Haskell you wish to work in. Indeed, the lack of injectivity for type families is the same kind of problem that exists in those other languages, so Haskell has already paid this price. > > I'd like term-level functions to be more like instances. > That is, with the equations distributed, see your example > below. > (Yes the set of equations must be coherent overall. > That's something the compiler can check for me.) I think it depends on the function. Some functions are defined by an ordered set of equations. Some (that is, class methods) are defined by an unordered set of equations, perhaps distributed across modules. Both models are useful. > > There was some doubt whether there could be a type-level > disequality test. And indeed this was hard! See "apartness". > >> ... [equality constraints and equality guards are] different, but I think the equality guard is > useless > > I see two main uses/benefits: > 1. avoids the need for non-linear patterns in the head Agreed that it would do this. But why is that important? > 2. visually points up the 'non-apartness' vs an, um. > "apartness guard" > > (When I was figuring out Andy A-M's 2013 example, > I rewrote the non-linear patterns with ~ guards, > so I could figure out the apartness guards > esp for the semi-apart instances. > I posted the later workings to your blog Somehow, this is more convincing. But I'm still not convinced on this point. Happily, you don't need to convince me -- put in the proposal what you like and then we can debate a concrete design. >> [except as a type-level "let", I suppose].) > > No, they're not doing that: > deliberately I don't allow guards > to introduce new type vars. They would work as "let", I think: > instance Either a a | a ~ SomethingBigAndUgly where ... Note that the `a` is not introduced in the guard. > Ok thanks, yes [TypeError] helps. > Nevertheless it seems disergonomic > to write an instance for a type-equal case, > even with a helpful error message; > when what you want is: no such instance. You could always view > instance TypeError ... => C Int Bool as sugar for > instance C Int Bool fails The first declaration isn't so bad, I think, that it warrants introducing new concrete syntax. > > What I can see will be awkward is backwards compatibility: > can a class/type family with guards > coexist with CTFs and with classes using overlap? Sure. There would be no problem with this. The new idea is just that: new. I don't see it as getting rid of anything we already have. Perhaps some day we could think about removing OverlappingInstances, but we certainly don't have to do that at the same time as introducing instance guards. (I do like that name, too.) > >> Next step: write a ghc-proposal. I'll support it. If I had >> the time, I'd even implement it. > > I'll have a crack at the proposal. Great. Thanks! Richard _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Alejandro Serrano Mena
Do you recall an example of where things went wrong? It seems to me that GHC does this today. If I have > instance C (Maybe a) where ... > instance {-# OVERLAPPING #-} C (Maybe Int) where ... then GHC won't choose the first instance unless it knows that `a` is apart from Int. Indeed, it is possible to write a program that is accepted with only the first instance in scope but is rejected when the second one is, too. Under instance guards, this could be written > instance C (Maybe a) | a /~ Int where ... > instance C (Maybe Int) where ... and then both instances stand alone and make sense independent of one another. Richard _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Tue May 30 19:43:30 UTC 2017, Richard Eisenberg wrote:
> > On May 24, 2017, at 3:13 AM, Anthony Clayden wrote: > ... Some functions are defined by an ordered set of equations. > Some (that is, class methods) are defined by > an unordered set of equations, perhaps distributed across modules. > Both models are useful. Sure. Let a 100 schools of thought contend. >>> ... [equality constraints and equality guards are] >>> different, but I think the equality guard is useless >> I agree adds nothing over repeating the typevar. And I've already agreed the potential for confusion with (~) constraints. So noted. I'll include it in the proposal, where a wider audience can bikeshed. >> I see two main uses/benefits: >> 1. avoids the need for non-linear patterns in the head > > Agreed that it would do this. But why is that important? > I was in part thinking of your wondering-out-loud earlier in the Partially applied thread https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127078.html If we want to part-apply a type Fun which has a non-linear lhs, how does that go with your case-equation style? Adapting that earlier example: > type family F a b where > F a a = () -- added an equation > F Int b = b > F a Bool = a would really mean > type F a b = case a of > _ -> case b of -- ?? _ match-all > a -> () -- ?? re-using typevar a > Int -> b > _ -> case b of > Bool -> a > _ -> F a b > > 2. visually points up the 'non-apartness' vs an, um. > > "apartness guard" > > > > (When I was figuring out Andy A-M's 2013 example, > > I rewrote the non-linear patterns with ~ guards, > > so I could figure out the apartness guards > > esp for the semi-apart instances. > > I posted the later workings to your blog > > Somehow, this is more convincing. But I'm still not > convinced on this point. Happily, you don't need to > convince me -- put in the proposal what you like and then > we can debate a concrete design. > > >> [except as a type-level "let", I suppose].) > > They would work as "let", I think: > > > instance Either a a | a ~ SomethingBigAndUgly where ... > > Note that the `a` is not introduced in the guard. Ah, OK. I get you. Equally that could be > instance Either a b | a ~ b, a ~ SomethingBigAndUgly where .. > > > Ok thanks, yes [TypeError] helps. > > Nevertheless it seems disergonomic > > to write an instance for a type-equal case, > > even with a helpful error message; > > when what you want is: no such instance. > > You could always view > > > instance TypeError ... => C Int Bool > > as sugar for > > > instance C Int Bool fails Yes I understand that. But no I don't want any instance. (Sugar on rotten fruit doesn't hide the smell.) There are (or at least used to be) all sorts of side-effects from there in effect being an instance that matched. > > What I can see will be awkward is backwards > > compatibility: can a class/type family with guards > > coexist with CTFs and with classes using overlap? > > Sure. There would be no problem with this. The new idea is > just that: new. I don't see it as getting rid of anything > we already have. Perhaps some day we could think about > removing OverlappingInstances, but we certainly don't have > to do that at the same time as introducing instance > guards. (I do like that name, too.) > OK. Perhaps you're seeing something I can't. To adapt your example from a parallel message, suppose: > module A > > class {-# INSTANCEGUARDS #-} C a where ... > instance C (Maybe a) | a /~ Int where ... > instance C (Maybe Int) where ... > > module B > -- knows nothing of InstanceGuards > import A > > instance {-# OVERLAPPABLE #-} C (Maybe Bool) where ... I want to reject that `(Maybe Bool)` instance. Even though it would legitimately be OVERLAPPABLE by (Maybe a) (that is, without the `a /~ Int` guard). Furthermore I might want a class to be InstanceGuarded, even though the instances I declare don't themselves need guards. (That is, I'm wanting to avoid 'future' overlaps in modules that import the class.) > > > > I'll have a crack at the proposal. > > Great. Thanks! (Likely I'll need some help with the protocols.) AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
> On May 31, 2017, at 12:31 AM, Anthony Clayden <[hidden email]> wrote: > > If we want to part-apply a type Fun > which has a non-linear lhs, > how does that go with your case-equation style? Problematically. This is why my thesis muses on -- but stops well short of solving -- the problem of non-linear patterns. I'm not sure how it all fits together. >> >> You could always view >> >>> instance TypeError ... => C Int Bool >> >> as sugar for >> >>> instance C Int Bool fails > > Yes I understand that. > But no I don't want any instance. > (Sugar on rotten fruit doesn't hide the smell.) I hereby pronounce > instance TypeError ... => C Int Bool as "not an instance". In other words, I'm not sure what you're getting at here other than concrete syntax. How does not having an instance differ than the TypeError solution? > > OK. Perhaps you're seeing something I can't. > To adapt your example from a parallel message, suppose: > <snip> What you're getting at here is that there may be interesting interplay between instance guards and OverlappingInstances. Indeed. This would have to be worked out (or left as an open question) in the proposal. Regardless, I think that hashing out this level of detail here is the wrong place. Put it in the proposal! That way, the ensuing debate involves more of the community and persists better. Richard _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by AntC
> On Fri Jun 2 02:32:39 UTC 2017, Richard Eisenberg wrote:
> > > On May 31, 2017, at 12:31 AM, Anthony Clayden wrote: > > >> You could always view > >> > >>> instance TypeError ... => C Int Bool > >> > >> as sugar for > >> > >>> instance C Int Bool fails > > > > Yes I understand that. > > But no I don't want any instance. > > (Sugar on rotten fruit doesn't hide the smell.) > > I hereby pronounce > > > instance TypeError ... => C Int Bool > > as "not an instance". ... Hmm. I'd be interested how you're going to stop the compiler matching some usage site to it. > In other words, I'm not sure what > you're getting at here other than concrete syntax. > How does not having an instance differ > than the TypeError solution? Good question. I've been struggling to explain it. Re-reading the Instance Chains paper has clarified the issue for me. And looking at Garrett's later 'Variations on Variants' paper. (Clarified, because that's a non-solution.) It's the Expression Problem: Once I have a catch-all instance (even if it has an impossible-to-fulfill constraint) the compiler is committed to selecting that instance. I can't introduce a new data type and new instance for it, because it'll overlap the catch-all instance. IIUC, Instance Chain's 'fail' is more powerful, it triggers back-tracking to look for another instance that doesn't fail. But we don't want to introduce backtracking into Haskell search for instances. Nevertheless, I can only write one Instance Chain per class. So I can't (say in another module) introduce a new datatype with instances. Sometimes closed/chained instances are the right solution. (That's the case for HList, for example. But even there I'm not convinced. I might want as well as HNil, HCons, a constructor with explicit type-labelling.) But sometimes closed instances are not right. I would say that where closed instances are needed, you can still achieve that with a 'catch-all' stand-alone instance, suitably guarded, of course. So I disagree with Garrett: not only do Instance Chains fail to solve the expression problem, they actually exacerbate it. (Same for Closed Type Families, or Closed Class Instances.) > > OK. Perhaps you're seeing something I can't. > > To adapt your example from a parallel message, suppose: > > <snip> > > What you're getting at here is that there may be > interesting interplay between instance guards and > OverlappingInstances. Indeed. This would have to be worked > out (or left as an open question) in the proposal. > > Regardless, I think that hashing out this level of detail > here is the wrong place. ... OK, fair enough. > Put it in the proposal! That way, the ensuing > debate involves more of the community and > persists better. > Oh! that I had "Deserts of vast eternity" to write the thing. As it is, it's easier to tackle as bite-size pieces on the forum. AntC _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |