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

[oleg at okmij.org]

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