[Haskell-cafe] Fundeps and overlapping instances

[AntC]

Twan van Laarhoven <twanvl <at> gmail.com> writes:

> 
> On 24/05/12 14:14, AntC wrote:
> > Simon Peyton-Jones<simonpj<at>  microsoft.com>  writes:
> >
> 
> Have you considered the alternative notation where multiple guards are 
allowed, 
> as in normal function definitions? Something like:
> 
>      type instance F a
>          | a ~ Int   = Bool
>          | Otherwise = [a]
> 

Hi Twan, there's various style amongst the discussions -- trace the links back 
from my previous post to Haskell-prime.

And see SPJ's surprise (to me) announcement that there's some work in 
progress, which gives something very like it.

But no, I don't like it: it means I can't put different instances in different 
modules (so far as I can tell).


> ..., which would allow you to write closed type functions.

Please explain (because I haven't seen this stated anywhere): what is the use 
case for closed type functions? As opposed to explicitly dis-overlapped type 
functions.

> 
> I think this variant is almost equivalent to your proposal ...

No: closed functions mean you have to declare all your instances in the same 
place, in the same module. The whole point of the instance mechanism (or so I 
thought) is that it's expandable.

To see why, consider my example with a 2-argument type function.
http://www.haskell.org/pipermail/haskell-prime/2012-May/003690.html

(I haven't seen enough detail from the closed type func or IFEQ styles to know 
whether we could be 'open' on the first arg, but closed on the second.)

> I also don't know how hard something like this would be to implement. ...

Indeed! I've proposed implication constraints, see
http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html

That's from the Sulzmann and Stuckey 2002 paper, and I think available for 
type reasoning in such things as Chameleon. Implication Constraints are used 
for the OutsideIn(X) approach to implement GADT's with local constraints. (But 
what I've added is a dis-equality test in the antecedent.)

The evidence we need to satisfy the dis-equality guards does not have to be a 
fully-grounded type, it just needs to be enough that the types can't be equal 
(typically, the outermost constructor).

But it looks like the work SPJ pointed to is using closed style. If all 
they're trying to do is support HList and similar, I guess that's good enough.
 
I tried to explain all this the best part of a year ago. (Admittedly my 
explanation was a bit turgid, re-reading it today. And not that I was saying 
anything that hadn't been said by others -- it's resurfaced several times.) 
Funny how GHC-central just barrels ahead and ignores all those ideas, 
apparently without explaining why.

AntC