Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
Anthony Clayden wrote: > So three questions in light of the approach of abandoning FunDeps and > therefore not getting interference with overlapping: > A. Does TTypeable need to be so complicated? > B. Is TTypeable needed at all? > C. Does the 'simplistic' version of type equality testing suffer possible > IncoherentInstances? It is important to keep in mind that Type Families (and Data Families) are _strictly_ more expressive than Functional dependencies. For example, there does not seem to be a way to achieve the injectivity of Leibniz equality http://okmij.org/ftp/Computation/extra-polymorphism.html#injectivity without type families (and relaying instead on functional dependencies, implemented with TypeCast or directly). I'd like to be able to write data Foo a = Foo (SeqT a) where SeqT Bool = Integer SeqT a= [a] otherwise (A sequence of Booleans is often better represented as an Integer). A more practical example is http://okmij.org/ftp/Haskell/GMapSpec.hs http://okmij.org/ftp/Haskell/TTypeable/GMapSpecT.hs It is possible to sort of combine overlapping with associated types, but is quite ungainly. It is not possible to have overlapping associated types _at present_. Therefore, at present, TTYpeable is necessary and it has to be implemented as it is. You point out New Axioms. They will change things. I have to repeat my position however, which I have already stated several times. TTypeable needs no new features from the language and it is available now. There is no problem of figuring out how TTypeable interacts with existing features of Haskell since TTypeable is implemented with what we already have. New Axioms add to the burden of checking how this new feature interacts with others. There have been many examples when one feature, excellent by itself, badly interacts with others. (I recall GADT and irrefutable pattern matching.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
okmij.org> writes:
>
> > I think instead you should have:
> > - abandoned FunDeps
> > - embraced Overlapping more!
>
> Well, using TypeCast to emulate all FunDeps was demonstrated three
> years later after HList (or even sooner -- I don't remember when
> exactly the code was written):
>
> http://okmij.org/ftp/Haskell/TypeClass.html#Haskell1
>
Yes, I see the same idiom. I'll use it below in the definition of the TypeEq
predicate.
>
> > So here's my conjecture:
> > 1. We don't need FunDeps, except to define TypeCast.
> >(And GHC now has equality constraints, which are prettier.)
> > 2. Without FunDeps, overlapping works fine.
> > ...
>
> I agree on point 1 but not on point 2. The example of incoherence
> described in Sec `7.6.3.4. Overlapping instances' of the GHC User
> Guide has nothing to do with functional dependencies.
>
The question a couple of months ago was: do we need Type-level TypeRep? And
you had made a case before that for the TTypeable approach. And TTypeable
started life as 'A representation-based equality predicate', Section 9 of the
HList paper. And the justification for it was 'Overlapping banned', Section 6.
So three questions in light of the approach of abandoning FunDeps and
therefore not getting interference with overlapping:
A. Does TTypeable need to be so complicated?
B. Is TTypeable needed at all?
C. Does the 'simplistic' version of type equality testing suffer possible
IncoherentInstances?
A. I conjecture that TTypeable does not need the TC_code family,
nor the phantom type to drive it, nor the NAT encoding.
Instead let each type stand for itself, then we just need TYPEOF:
type instance TYPEOF () = ( (), NIL )
type instance TYPEOF [a]= ( [()], (TYPEOF a) :/ NIL )
type instance TYPEOF (IO a) = ( IO (), (TYPEOF a) :/ NIL )
-- etc
-- I guess TH could generate those instances?
Then for testing type equality, we can use a simple overlapping test:
type family TypeEq a b :: Bool where
{ TypeEq a a = True
; TypeEq _ _ = False
}
This uses the proposed NewAxiom style of type function.
Equivalently with a class:
instance (TypeCast p TTrue) => TypeEq a a p-- works in Hugs 2002!
instance (TypeCast p TFalse) => TypeEq a b p
No risk of incoherent instances because the arguments have to be
instantiated via TYPEOF.
The approach of putting unit as dummy argument to the type constructors
means we can also test the 'shape' of the types.
2. But (apart from testing the shape) have we gained anything here
over testing the types directly, rather than going via TYPEOF?
If the type isn't grounded enough to test for equality
(as observed in Section 9 'By chance or by design?'),
then neither is it grounded enough to instantiate for TYPEOF.
3. The incoherent instances example in Sec 7.6.3.4 is because of instances
defined in separate modules.
The simplistic test for type equality declares its two instances together.
Is there some way an incoherent instance could slip through?
If not, what is the TTypeable mechanism gaining?
And by the way, I couldn't help trying a bit of 'compiler archaeology'. I dug
out Hugs version November 2002. My revised hDeleteMany works fine, as does
my 'repair' to the example in 'Ended up in murky water'.
So I can't see a need for TTypeable even back in 2004.
AntC
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
okmij.org> writes: > > > I think instead you should have: > > - abandoned FunDeps > > - embraced Overlapping more! > > Well, using TypeCast to emulate all FunDeps was demonstrated three > years later after HList (or even sooner -- I don't remember when > exactly the code was written): > > http://okmij.org/ftp/Haskell/TypeClass.html#Haskell1 > Yikes! Thank you Oleg, more formidable code to get my head round. > > > So here's my conjecture: > > 1. We don't need FunDeps, except to define TypeCast. > >(And GHC now has equality constraints, which are prettier.) > > 2. Without FunDeps, overlapping works fine. > > ... > > I agree on point 1 but not on point 2. The example of incoherence > described in Sec `7.6.3.4. Overlapping instances' of the GHC User > Guide has nothing to do with functional dependencies. > Well, I meant overlapping as used in HList. But fair point, and goes back to a much earlier discussion: a) Don't switch on IncoherentInstances. b) Make instance validation 'eager' and 'strict' like Hugs does, not 'optimistic'/'lax' like GHC. (That is, validate at point of declaration of the instance.) c) Reject instances that are not explicitly dis-overlapped. The mechanism for dis-overlap is disequality restraints. So for the multi- module MyShow example in 7.6.3.4. reject the overlap: instance MyShow [T] -- in module Main is OK, providing -- instance MyShow [a] -- in module Help must be dis-overlapped to instance MyShow [a] | a /~ T where ... The work-in-progress NewAxioms is aiming for something similar, but only for type functions. Perhaps in the longer term we use that to build helper functions, then banish overlapping type classes? (I still think that explicitly dis-overlapped instances would be easier to understand.) AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
> I think instead you should have: > - abandoned FunDeps > - embraced Overlapping more! Well, using TypeCast to emulate all FunDeps was demonstrated three years later after HList (or even sooner -- I don't remember when exactly the code was written): http://okmij.org/ftp/Haskell/TypeClass.html#Haskell1 We demonstrate that removing from Haskell the ability to define typeclasses leads to no loss of expressivity. Haskell restricted to a single, pre-defined typeclass with only one method can express all of Haskell98 typeclass programming idioms including constructor classes, as well as multi-parameter type classes and even some functional dependencies. The addition of TypeCast as a pre-defined constraint gives us all functional dependencies, bounded existentials, and even associated data types. Besides clarifying the role of typeclasses as method bundles, we propose a simpler model of overloading resolution than that of Hall et al. > So here's my conjecture: > 1. We don't need FunDeps, except to define TypeCast. >(And GHC now has equality constraints, which are prettier.) > 2. Without FunDeps, overlapping works fine. > ... I agree on point 1 but not on point 2. The example of incoherence described in Sec `7.6.3.4. Overlapping instances' of the GHC User Guide has nothing to do with functional dependencies. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
okmij.org> writes: > > > > > I implemented hDeleteMany without FunDeps -- and it works in Hugs (using > > TypeCast -- but looks prettier in GHC with equality constraints). > > It is nice that hDeleteMany works on Hugs. I forgot if we tried it > back in 2004. Thanks Oleg -- but it was only 8 years ago ;-) Yes you did try it: the HList paper gives it as evidence for "We gave up on persuading Hugs." and "Overlapping Banned" [Section 6, p7]. I think you were premature, which is why I'm using it as an example. I've also 'repaired' the example in "Ended up in murky water", and got that working in Hugs. Let me say straight away that I'm not trying to 'knock' the work you and Ralf put into HList. It's a formidable, and formidably impressive piece of work (as can be seen from the number of papers that reference it). I've built record- like systems using it. But the HList paper goes on to abandon overlapping, and bring in (essentially) the TTypeable approach for type equality. I'm saying (in the discussion a couple of months ago) that TTypeable is unnecessary, and that overlapping instances are robust -- except when they get mixed up with FunDeps. I think instead you should have: - abandoned FunDeps - embraced Overlapping more! > To be sure some HList code did work on Hugs. We even had > a special subset of HList specifically for Hugs (which I removed from > the distribution some time ago). The problem was that Hugs > inexplicably would fail in some other HList code. Perhaps 2006 version > is better in that respect, and more or all of HList would work on it. > Yeah, I'm not trying to 'rehabilitate' Hugs. No point in doing 'compiler archeology' on whether/when anything got fixed. To come back to the CRIP Ryan has spotted: - It got 'blessed' by SPJ in amongst the 'Records in Haskell' proposals [1] - Certainly equality constraints make the technique easier; - but TypeCast (in the HList paper) achieved the same thing back in 2004 (and the HList paper discusses earlier approaches for typecast). - So HList used the technique to get round some of the issues with overlapping. - I'm saying you could have got round more of the issues. - And perhaps have got the whole of HList working in Hugs. So here's my conjecture: 1. We don't need FunDeps, except to define TypeCast. (And GHC now has equality constraints, which are prettier.) 2. Without FunDeps, overlapping works fine. 3. (Also we don't get into trouble with transitive chains of FunDeps.) 4. Instead of FunDeps, put TypeCasts on all of the instances. (Or other Class constraints to 'chain' typevars.) 5. And all of the instances must be framed with a bare typevar in the 'result'. (That is, a typevar distinct from any others in the head.) 6. (As you said to Ryan) we still sometimes need repeated typevars in the head, for instances that are (in effect) testing for equality. But these should only be in the 'argument' position. AntC [1] http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Higherr anktypesandtypefunctions see "functional-dependency-like mechanism (but using equalities)" ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
> did you see this, and the discussion around that time? > http://www.haskell.org/pipermail/haskell-prime/2012-May/003688.html > > I implemented hDeleteMany without FunDeps -- and it works in Hugs (using > TypeCast -- but looks prettier in GHC with equality constraints). I'm afraid I didn't see that -- I was on travel during that time. It is nice that hDeleteMany works on Hugs. I forgot if we tried it back in 2004. To be sure some HList code did work on Hugs. We even had a special subset of HList specifically for Hugs (which I removed from the distribution some time ago). The problem was that Hugs inexplicably would fail in some other HList code. Perhaps 2006 version is better in that respect, and more or all of HList would work on it. Thank you. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
okmij.org> writes: > > [... snip] > > Of course instances above are overlapping. And when we add functional > dependencies (since we really want type-functions rather type > relations), they stop working at all. We had to employ work-arounds, > which are described in detail in the HList paper (which is 8 years old > already). > Yes, it's adding the FunDeps that puts the spanner in the works. Oleg, did you see this, and the discussion around that time? http://www.haskell.org/pipermail/haskell-prime/2012-May/003688.html I implemented hDeleteMany without FunDeps -- and it works in Hugs (using TypeCast -- but looks prettier in GHC with equality constraints). Essentially it's a FunDep-like mechanism without FunDeps (as SPJ calls it), to achieve what Ryan's talking about. But you are quite right that we still need overlapping instances for parts of the type-level logic. AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
Ryan Ingram wrote: > I've been seeing this pattern in a surprising number of instance > definitions lately: > > instance (a ~ ar, b ~ br) => Mcomp a ar b br [1] > instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a [2] And here are a few more earlier instances of the same occurrence: http://okmij.org/ftp/Haskell/typecast.html > What I'm wondering is--are there many cases where you really want the > non-constraint-generating behavior? It seems like (aside from contrived, > ahem, instances) whenever you have instance CLASS A B where A and B share > some type variables, that there aren't any valid instances of the same > class where they don't share the types in that way. Instances of the form class C a b class C a a class C a b are very characteristic of (emulation) of disequality constraints. Such instances occur, in a hidden form, all the time in HList -- when checking for membership in a type-level list, for example. There are naturally two cases: when the sought type is at the head of the list, or it is (probably) at the tail of the list. class Member (h :: *) (t :: List *) instance Member h (Cons h t) instance Member h t => Member h (Cons h' t) Of course instances above are overlapping. And when we add functional dependencies (since we really want type-functions rather type relations), they stop working at all. We had to employ work-arounds, which are described in detail in the HList paper (which is 8 years old already). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern
With apologies to Jim Coplien :) I've been seeing this pattern in a surprising number of instance definitions lately: instance (a ~ ar, b ~ br) => Mcomp a ar b br [1] instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a [2] The trick is that since instance selection is done entirely on the instance head, these instances are strictly more general than the ones they replace: instance Mcomp a a b b instance CanFilterFunc b => CanFilter (b -> b) a The compiler has to do a lot more work to select these instances; it has to prove that the matching types actually match before it can select the instance; if it can't, it won't select an instance, and instead will complain about no instance "CLASS Int a". But with the CRIP, you help the compiler--it chooses the general instance, and then gets a constraint to solve. The constraint forces the two types to unify, or else there is a type error. What I'm wondering is--are there many cases where you really want the non-constraint-generating behavior? It seems like (aside from contrived, ahem, instances) whenever you have instance CLASS A B where A and B share some type variables, that there aren't any valid instances of the same class where they don't share the types in that way. For example, I've never really seen a class in practice with instances like class Foo a b instance Foo a a instance Foo ConcreteTypeA ConcreteTypeB Note that it's very difficult to use polymorphic types in the second instance without risking overlap. TL;DR: I, for one, welcome our new type equality constraint overlords. -- ryan [1] http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/99611 [2] http://www.yesodweb.com/blog/2012/07/classy-prelude ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
