Re: [Haskell-cafe] Fundeps and overlapping instances

Twan van Laarhoven writes:

On 24/05/12 14:14, AntC wrote:

...

Simon Peyton-Jones 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