[Haskell-cafe] CRIP: the Curiously Reoccuring Instance Pattern

[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