New-to-Haskell, i.e. elementary, Haskell questions; extended discussions

headers Ryan Ingram | 31 Jul 2012 03:38

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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).

 <oleg <at> 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

> 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.

 <oleg <at> 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)"

> 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.

 <oleg <at> 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

 <oleg <at> 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

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.)

CRIP: the Curiously Reoccuring Instance Pattern

CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern

Re: CRIP: the Curiously Reoccuring Instance Pattern