Fundeps and overlapping instances

[Simon Peyton-Jones]

Oleg points out, and Martin also mentions, that functional dependencies appear to interact OK with overlapping instances, but type families do not. I this impression is mistaken, and I’ll try to explain why in this message, in the hope of exposing any flaws in my reasoning.

 

We can’t permit overlap for type families because it is unsound to do so (ie you can break “well typed programs don’t go wrong”). But if it’s unsound for type families, it would not be surprising if it was unsound for fundeps too.  (I don’t think anyone has done a soundness proof for fundeps + local constraints + overlapping instances, have they?)  And indeed I think it is. 

 

So the short summary of this message is: if it works for fundeps it works for type families, and vice versa.  (NB this equivalence is not true about GHC’s current implementation, however.   GHC doesn’t support the combination of fundeps and local constraints at all.)

 

Such an equivalence doesn’t argue against fundeps; I’m only suggesting the that the two really are very closely equivalent.   I much prefer type families from a programming-style point of view, but that’s a subjective opinion.

 

Simon

 

 

Imagine a system “FDL” that has functional dependencies and local type constraints.  The big deal about this is that you get to exploit type equalities in *given* constraints.  Consider Oleg’s example, cut down a bit:

 

class C a b | a -> b

instance C Int Bool

newtype N2 a = N2 (forall b. C a b => b)

 

t2 :: N2 Int

t2 = N2 True

 

We end up type-checking (True :: forall b. C Int b => b).   From the functional dependency we know that (b~Bool), so the function should typecheck.  GHC rejects this program; FDL would not.

 

But making use of these extra equalities in “given” constraints is quite tricky.  To see why look first at Example 1:  

 

module X where

   class C a b | a -> b

 

   data T a where

     MkT :: C a b => b -> T a

 

 

module M1 where

  import X

  instance C Int Char where ...

  f :: Char -> T Int

  f c = MkT c

 

module M2 where

  import X

  instance C Int Bool

  g :: T Int -> Bool

  g (MkT x) = x

 

module Bad where

  import M1

  import M2

  bad :: Char -> Bool

  bad = g . f

 

This program is unsound: it lets you cast an Int to a Bool; result is a seg-fault.

                                                                                                                                                                     

You may say that the problem is the inconsistent functional dependencies in M1 and M2.  But GHC won’t spot that.  For type families, to avoid this we “eagerly” check for conflicts in type-family instances.  In this case the conflict would be reported when compiling module Bad, because that is the first time when both instances are visible together.

 

So any FDL system should also make this eager check for conflicts.

 

What about overlap?  Here’s Example 2:

 

{-# LANGUAGE IncoherentInstances #-}

module Bad where

  import X

  -- Overlapping instances

  instance C Int Bool         -- Instance 1

  instance C a [a]               -- Instance 2

 

  f :: Char -> T Int

  f c = MkT c                       -- Uses Instance 1

 

  g :: T a -> a

  g (MkT x) = x                    -- Uses Instance 2

 

  bad :: Char -> Int

  bad = g . f

 

Again, a seg fault if it typechecks.  But will it?  When typechecking ‘g’, we get a constraint (C a ?), where ‘a’ is a skolem constant.  Without IncoherentInstances GHC would reject the program on the grounds that it does not know what instance to choose.  But *with* IncoherentInstances it would probably go through, which is unsound.  So IncoherentInstances has moved from causing varying dynamic behaviour to causing seg faults.

 

Very well, so FDL must get rid of IncoherentInstances altogether, at least for classes that have functional dependencies (or that have superclasses that do).  

 

But at the moment GHC makes an exception for *existentials*.  Consider Example 3:

 

  class C a b | a -> b

 

  -- Overlapping instances

  instance C Int Bool         -- Instance 1

  instance C a [a]               -- Instance 2

 

  data T where

    MkT :: C a b => a -> b -> T

 

  f :: Bool -> T

  f x = MkT (3::Int) x          -- Uses Instance 1

 

  g :: T -> T

  g (MkT n x) = MkT n (reverse x)   -- Uses Instance 2

 

  bad :: Bool -> T

  bad = g . f

 

In the pattern match for MkT in g we have the constraint (C a b), where ‘a’ is existentially bound.   So under GHC’s current rules it’ll choose the (C a [a]) instance, and conclude that (b ~ [a]).  So it’s ok to reverse x.  But it isn’t; see function bad!

 

So to avoid unsoundness we must not choose a particular instance from an overlapping set unless we know, absolutely positively, that the other cases cannot match.  

 

(GHC’s exception for existentials was introduced in response to user demand. Usually, overlapping instances are somehow semantically coherent, and with an existential we are *never* going to learn more about the instantiating type, so choosing the best available seems like a good thing to do.)

 

But even nuking IncoherentInstances altogether is not enough.  Consider this variant of Example 3, call it Example 4:

 module M where

  class C a b | a -> b

 

  instance C a [a]               -- Instance 2

 

  data T where

    MkT :: C a b => a -> b -> T

 

  g :: T -> T

  g (MkT n x) = MkT n (reverse x)   -- Uses Instance 2

 

module Bad where

  import M

  instance C Int Bool         -- Instance 1

 

  f :: Bool -> T

  f x = MkT (3::Int) x          -- Uses Instance 1

 

  bad :: Bool -> T

  bad = g . f

 

This is nasty.  In module M we have only one instance declaration for C, so there’s no overlap, and function g typechecks fine. 

Now module Bad adds an overlapping instance declaration and ‘f’ uses it; moreover, it’s clear that the new instance declaration is the right one to use.

 

It’s not clear how to fix this.  The only way I can think of is to insist that all the instances appear in a single module, so that you cannot add more “later”. But that loses part of the point of overlap in the first place, namely to provide a generic instance and then later override it.

 

 

So FDL must

·        embody eager checking for inconsistent instances, across modules

·        never resolve overlap until only a unique instance can possibly match

·        put all overlapping instances in a single module

 

Type families already implement the first of these.    I believe that if we added the second and third, then overlap of type families would be fine.  (I may live to eat my words here.) 

 

I’d be interested to know what Chameleon does on these examples.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[AntC]

Simon Peyton-Jones <simonpj <at> microsoft.com> writes:

> [from 7 Jul 2010. I've woken up this thread at Oleg's instigation
> http://www.haskell.org/pipermail/haskell-prime/2011-July/003491.html ]
>

I'm not going to talk about Fundeps. This is about introducing overlapping
instances into type families. But I mean dis-overlapped overlaps, with dis-
equality guards on the instances:
http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html
This is essentially the same proposal as the July 2011 discussion, but a
little updated with actual experience of type families in their more mature
form.

Example type family equations:
        type instance F Int = Bool
        type instance F a | a /~ Int = [a]  -- explicit dis-equality guard


The July 2010 thread shows how prescient SPJ was about introducing overlaps
into type families (or FunDeps). The requirements he ends up with are spot-on,
and I believe I have anticipated them in the proposal for dis-overlapped
overlaps.

>
> Imagine a system “FDL” that has functional dependencies
> and local type constraints.  The big deal about this is that you get to
exploit

> type equalities in *given* constraints.  Consider Oleg’s
> example, cut down a bit:
>
> class C a b | a -> b
>
> instance C Int Bool
>
> newtype N2 a = N2 (forall b. C a b => b)
>
> t2 :: N2 Int
>
> t2 = N2 True
>
> We end up type-checking (True :: forall b. C Int b =>
> b).   From the functional dependency we know that (b~Bool), so the
> function should typecheck.  GHC rejects this program; FDL would not.
>

GHC 7.2.1 still rejects this program, but accepts a version re-written to use
type families:
    type family CF a
    type instance CF Int = Bool

    newtype N2 a = N2 (CF a)    -- could be = N2 (forall b. b ~ CF a => b)

    t2 :: N2 Int
    t2 = N2 True

>
> But making use of these extra equalities in “given”
> constraints is quite tricky.  To see why look first at ... [snip]
>
SPJ works through 4 examples, gathering "tricky" and "nasty" situations that
are unsound.

The examples involve overlaps, so can't be rewritten to use type families.
(And GHC rejects attempts to encode them with type classes avoiding fundeps
+ "a functional-dependency-like mechanism (but using equalities) for the
result type".)

So let me cut to SPJ's conclusions, and compare them against dis-overlapped
overlaps ...
>
> So FDL must
>
> ·  embody eager checking for inconsistent instances, across modules
>
     (Type families already implement this, SPJ notes below.)

     Yes: I expect dis-overlapped overlaps to do this.
     (Eager checking is Hugs' approach FWIW, and although at first it seems
      a nuisance, it leads to more 'crisp' development.
      Contrast GHC compiles inconsistent instances, but then you find
      you can't reach them, or get obscure failures.)
     Eager checking also detects and blocks the irksome imported-instances-
     silently-changing-behaviour behaviour.

> ·  never resolve overlap until only a unique instance can possibly
>              match
>
     Yes-ish -- instance matching doesn't have to be as strict as that:
     type inference must gather evidence of the dis-equality(s)
     in the guards before matching to the type function equation.
     Because the instances can't overlap, it's safe to apply the instance,
     as soon as the dis-equality(s) are discharged, and the head matches.

> ·  put all overlapping instances in a single module
>
     I don't think we need this, providing each instance 'stands alone'
     with its dis-equality guards.
     Instead, for each imported module, we validate that its instances,
     do not overlap, taking the guards into account.
     [SPJ admits that such a restriction "loses part of the point of
      overlap in the first place."]
>  
>
> Type families already implement the first of these.   
> I believe that if we added the second and third, then overlap of type
families would
> be fine.  (I may live to eat my words here.) 
>

AntC


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Twan van Laarhoven]

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

> Simon Peyton-Jones<simonpj<at>  microsoft.com>  writes:
>
>> [from 7 Jul 2010. I've woken up this thread at Oleg's instigation
>> http://www.haskell.org/pipermail/haskell-prime/2011-July/003491.html ]
>>
>
> I'm not going to talk about Fundeps. This is about introducing overlapping
> instances into type families. But I mean dis-overlapped overlaps, with dis-
> equality guards on the instances:
> http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html
> This is essentially the same proposal as the July 2011 discussion, but a
> little updated with actual experience of type families in their more mature
> form.
>
> Example type family equations:
>          type instance F Int = Bool
>          type instance F a | a /~ Int = [a]  -- explicit dis-equality guard
>

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]

The last 'otherwise' clause is mandatory, matching should never fall through.
Perhaps it could be an error if that were to happen, which would allow you to
write closed type functions. Note that Otherwise could be declared in the library as
     type Otherwise = () :: Constraint

I think this variant is almost equivalent to your proposal (so maybe it's just
bikeshedding). It is also very similar to the IFEQ proposal, and you can desugar
one in terms of the other.

I also don't know how hard something like this would be to implement. The
matching of type instances would be done in the same way as now, only their
expanding is changed. The compiler will at this point have to look which guards
are satisfied. In this example the first guard is a~Int, and this can not be
checked until more is known about a. So, even though we have a known matching
instance, it can not yet be expanded. Perhaps the notation "instance F a | a /~
Int" is better, because then a type family application can be expanded iff there
is a matching instance.


Twan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Gábor Lehel]

On Fri, May 25, 2012 at 7:06 AM, AntC <[hidden email]> wrote:
> 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.

If you're referring to the NewAxioms work Simon linked to in the other
thread, I don't see it explicitly stated that all instances have to be
within a single module. Especially section 3.3 (Translation) of the
pdf[1] seems to suggest otherwise. Though it also doesn't seem to be
the same as what you're asking for. As far as I can tell, with
NewAxioms, wherever you could currently have a type instance, you
could instead have a type instance group. Within a group you could
have unrestricted overlap with the first matching instance being
selected, while between groups overlap would continue to be forbidden.
Relative to explicit disequality guards it seems both more and less
powerful: you couldn't have overlap between modules (but could still
split instances among modules as long as they *don't* overlap), but
overlap within a module would be more powerful (or at least more
convenient). It seems vaguely similar to a paper on instance chains[2]
I saw once.

(Apologies in advance if any of this is inaccurate, I'm just going by
what I can see.)

[1] https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl
[2] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.170.9113&rep=rep1&type=pdf

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[AntC]

Gábor Lehel <illissius <at> gmail.com> writes:

>
> On Fri, May 25, 2012 at 7:06 AM, AntC <anthony_clayden <at> clear.net.nz>
wrote:
> > But it looks like the work SPJ pointed to is using closed style. ...
>
> If you're referring to the NewAxioms work Simon linked to in the other
> thread, I don't see it explicitly stated that all instances have to be
> within a single module. Especially section 3.3 (Translation) of the
> pdf[1] seems to suggest otherwise. Though it also doesn't seem to be
> the same as what you're asking for. As far as I can tell, with
> NewAxioms, wherever you could currently have a type instance, you
> could instead have a type instance group. ... [snip]

Thanks Gábor, I think you could be right. (It needs some pretty close reading
of the equations.) I think in this case an example would be worth a thousand
typevars - double-barred of course.

    I told them in Hebrew, I told them in Dutch,
    I told them in Latin and Greek,
    But I clear forgot (and it vexes me much),
    That Haskell is what they speak.

The NewAxioms (draft) paper has a reference to Oleg's HList, but not his Type-
level Typeable, nor to Salzmann & Stuckey (2002), Chameleon, nor the myriad
discussions in the cafe and Haskell Prime.

It would be nice to see a statement along the lines of: we looked at X, Y and
Z, and didn't follow that approach because ...; or we believe that approach
can be incorporated like this ...

I thought it was a good research discipline to start with a literature survey,
to avoid re-inventing the wheel(?)

> It seems vaguely similar to a paper on instance chains[2]
> I saw once.
>
Thanks, I saw that a while back but didn't look into it much at the time.

There's heaps of approaches out there to type-safe overlaps. Perhaps they're
all logically equivalent(?) So perhaps we're only bikeshedding about surface
syntax(??)

AntC






_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[AntC]

Gábor Lehel <illissius <at> gmail.com> writes:

>
> If you're referring to the NewAxioms work Simon linked to ... [snip]
> ... It seems vaguely similar to a paper on instance chains[2]
> I saw once.

Thanks Gábor for the reference, but I don't think they're very comparable.

The instance chains is in context of fundeps and overlaps (as you'd expect
from MPJ, since it was him who first introduced fundeps). I know fundeps
are 'theoretically' equivalent to type families. But I think the instance
chains paper is a good demonstration of why I find fundeps so awkward to
follow at the superficial syntax level for type-level programming:
- you have to look first to the end of the instance to find the head;
- and assume (hope!) that the 'result' is the rightmost typevar;
- then backtrack through the list of constraints;
- some are only validation limits on the instance;
- some are calculating intermediate results (again with their result at right).

Instance chains include:
- not only resolving overlaps (yes, that's similar to NewAxioms);
- but also choosing instances based on type class membership;
  (often asked for by newbies, but really difficult to implement)
- and explicit failure leading to backtracking search

(Explicit failure is missing from NewAxioms. I don't mean backtracking, but at
least treating certain conditions as no instance match. Oleg's HList work
needs that (for example in the Lacks constraint), but has to fudge it by
putting a fake instance with a fake constraint.)

Does the overall instance chain structure guarantee termination of type
inference? I don't follow the algebra enough to be sure.

Morris & Jones' examples seem to me contrived: they've set up overlapping
instances where you could avoid them, and even where they seem harder to
follow. Yes, their solution is simpler than the problem they start with; but
no, the problem didn't need to be that complex in the first case. (I'm looking
especially at the GCD/Subt/Lte example -- I think I could get that to work in
Hugs with fundeps and no overlaps.)

I'm surprised there isn't a Monad Transformer example: [3] by MPJ uses
overlaps for MonadT. And MonadT was (I thought) what gave all the trouble with
overlaps and default instances and silently changing behaviour. (There's a
brief example in Morris' supporting survey - ref [11] in [2].)

Anybody out there can explain further?

AntC

>
> [2] http://citeseerx.ist.psu.edu/viewdoc/download?
doi=10.1.1.170.9113&rep=rep1&type=pdf
>
  [3] Functional Programming with Overloading and Higher-Order Polymorphism
      Mark P. Jones, 1995




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Iavor Diatchki]

Hello,

On Wed, Jul 7, 2010 at 2:14 PM, Simon Peyton-Jones <[hidden email]> wrote:

We can’t permit overlap for type families because it is unsound to do so (ie you can break “well typed programs don’t go wrong”). But if it’s unsound for type families, it would not be surprising if it was unsound for fundeps too.  (I don’t think anyone has done a soundness proof for fundeps + local constraints + overlapping instances, have they?)  And indeed I think it is. 

It would be unsound only if the functional dependencies are not checked properly (which, as you say, is similar to the check for type families).  Here is an example of a sound overlap:

class C a b | a -> b

instance C String Char

instance C [a] a

Indeed, it would be OK to allow this sort of overlap for type families too, although there it would not be useful, because the more general case already provides the same information as the more specific one.   In the case of overlapping instances, the more specific instance might provide a different implementation for the class methods, as usual.  (disclaimer:  I'm not a fan of overlapping instances----I think that some of the alternative proposals, such as the instance chains work, are nicer, but one would have to do same sort of checks there too).

 

Imagine a system “FDL” that has functional dependencies and local type constraints.  The big deal about this is that you get to exploit type equalities in *given* constraints.  Consider Oleg’s example, cut down a bit:

 

class C a b | a -> b

instance C Int Bool

newtype N2 a = N2 (forall b. C a b => b)

 

t2 :: N2 Int

t2 = N2 True

 

We end up type-checking (True :: forall b. C Int b => b).   From the functional dependency we know that (b~Bool), so the function should typecheck.  GHC rejects this program; FDL would not.

 

But making use of these extra equalities in “given” constraints is quite tricky.  To see why look first at Example 1:  

 

module X where

   class C a b | a -> b

 

   data T a where

     MkT :: C a b => b -> T a

 

 

module M1 where

  import X

  instance C Int Char where ...

  f :: Char -> T Int

  f c = MkT c

 

module M2 where

  import X

  instance C Int Bool

  g :: T Int -> Bool

  g (MkT x) = x

 

module Bad where

  import M1

  import M2

  bad :: Char -> Bool

  bad = g . f

 

This program is unsound: it lets you cast an Int to a Bool; result is a seg-fault.

                                                                                                                                                                     

You may say that the problem is the inconsistent functional dependencies in M1 and M2.  But GHC won’t spot that.  For type families, to avoid this we “eagerly” check for conflicts in type-family instances.  In this case the conflict would be reported when compiling module Bad, because that is the first time when both instances are visible together.

 

So any FDL system should also make this eager check for conflicts.

I completely agree with this---we should never allow inconsistent instances to exist in the same scope.

 

 

What about overlap?  Here’s Example 2:

 

{-# LANGUAGE IncoherentInstances #-}

module Bad where

  import X

  -- Overlapping instances

  instance C Int Bool         -- Instance 1

  instance C a [a]               -- Instance 2

 

  f :: Char -> T Int

  f c = MkT c                       -- Uses Instance 1

 

  g :: T a -> a

  g (MkT x) = x                    -- Uses Instance 2

 

  bad :: Char -> Int

  bad = g . f

 

As in the above example, this program violates the functional dependency on class C and should be rejected, because the two instances are not consistent with each other.

 

But at the moment GHC makes an exception for *existentials*.  Consider Example 3:

 

  class C a b | a -> b

 

  -- Overlapping instances

  instance C Int Bool         -- Instance 1

  instance C a [a]               -- Instance 2

 

  data T where

    MkT :: C a b => a -> b -> T

 

  f :: Bool -> T

  f x = MkT (3::Int) x          -- Uses Instance 1

 

  g :: T -> T

  g (MkT n x) = MkT n (reverse x)   -- Uses Instance 2

 

  bad :: Bool -> T

  bad = g . f

 

This program is malformed for the same reason as the previous one: the two instances violate the functional dependency on the class.

 

 

But even nuking IncoherentInstances altogether is not enough.  Consider this variant of Example 3, call it Example 4:

 module M where

  class C a b | a -> b

 

  instance C a [a]               -- Instance 2

 

  data T where

    MkT :: C a b => a -> b -> T

 

  g :: T -> T

  g (MkT n x) = MkT n (reverse x)   -- Uses Instance 2

 

module Bad where

  import M

  instance C Int Bool         -- Instance 1

 

  f :: Bool -> T

  f x = MkT (3::Int) x          -- Uses Instance 1

 

  bad :: Bool -> T

  bad = g . f

 

We must be thinking about these examples in a rather different way :-)   Like the others, I'd say that this program should be rejected because it violates the functional dependency on the class and should be rejected.

The way I think of a functional dependency on a class is that it restricts what instances are allowed to co-exist in the same scope.  So GHC needs to ensure that its instance database never contains instances that violate the functional dependency property.  This amounts to three checks:

1. Check that an instance is consistent with itself.  For example, this should be rejected:

instance C a b

because it allows C Int Bool and C Int Char which violate the functional dependency.

2. Check that an instance is consistent with all other instances in scope.  Note that this is orthogonal to the overlapping check: instances need to be consistent with the fun. dep. independent of overlap.

3. Check that instances imported from different modules are consistent with each other.  This is really a special case of 2, and GHC must already be doing some checking at this point to avoid duplicated instances.

It is important that the checks for consistency are sound.  They are not likely to be complete (i.e., we might reject some programs that do not really violate the fun.dep. but GHC can't see it),

but that's OK.   The usual rule, I forget its name, falls in this category.

Finally for the payoff of all this:  because we know that GHC is going to enforce the fun. dep. invariant, we can use it when we type check things.  For example, consider the standard example:

f :: (C a b, C a c) => a -> b -> c

f x y = y

This is OK, but only as long as GHC ensures that all instances of C satisfy the fun. dep. invariant. If the invariant is satisfied, however, then we know that whenever "f" is used, the instances that will be used to discharge its constraints are going the satisfy the fun. dep. and so "b" and "c" will be the same.

-Iavor

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Etienne Laurin]

Hello,

I disagree with your example.

> 1. Check that an instance is consistent with itself.  For example, this
> should be rejected:
>
> instance C a b
>
> because it allows C Int Bool and C Int Char which violate the functional
> dependency.

Functional dependencies are not used to pick types, they are used to
pick instances.

class C a b | a → b where
  k ∷ a
  f ∷ a → Maybe b

The functional dependency allows you to have a method such as k that
doesn't use all the arguments of the class.

I expect to be able to make a instance that works for any b.

instance C Int b where
  k = 2
  f _ = Nothing

Etienne Laurin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Iavor Diatchki]

Hello,

the notion of a functional dependency is well established, and it was used well before it was introduced to Haskell (for example, take a look at http://en.wikipedia.org/wiki/Functional_dependency).  So I'd be weary to redefine it lightly.

Note that placing a functional dependency constraint is just one way to allow class methods that don't mention all class variables.  If the instances for the class do not satisfy the functional dependency (as in your example), you can refactor your class hierarchy, instead.  For example:

class D a where  k :: a

class D a => C a b where  f :: a -> b

instance D Int where k = 2

instance C Int b where f _ = Nothing

I hope this helps,

-Iavor

On Wed, May 30, 2012 at 1:31 PM, Etienne Laurin <[hidden email]> wrote:

Hello,

I disagree with your example.

> 1. Check that an instance is consistent with itself.  For example, this
> should be rejected:
>
> instance C a b
>
> because it allows C Int Bool and C Int Char which violate the functional
> dependency.

Functional dependencies are not used to pick types, they are used to
pick instances.

class C a b | a → b where
 k ∷ a
 f ∷ a → Maybe b

The functional dependency allows you to have a method such as k that
doesn't use all the arguments of the class.

I expect to be able to make a instance that works for any b.

instance C Int b where
 k = 2
 f _ = Nothing

Etienne Laurin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Etienne Laurin]

2012/5/31 Iavor Diatchki <[hidden email]>:
> Hello,
>
> the notion of a functional dependency is well established, and it was used
> well before it was introduced to Haskell (for example, take a look
> at http://en.wikipedia.org/wiki/Functional_dependency).  So I'd be weary to
> redefine it lightly.

Indeed, GHC's functional dependencies are not the same. I see you have
already talked about this on the GHC bug tracker.

http://hackage.haskell.org/trac/ghc/ticket/1241

> 1. Check that an instance is consistent with itself.  For example, this should be rejected:
>
> instance C a b
>
> because it allows C Int Bool and C Int Char which violate the functional dependency.

This check may not always be as straightforward. When would this be a
valid instance?

instance K a b ⇒ C a b

With a few extra extensions, K could be a type family.

C currently has the kind (a -> b -> Constraint), with no mention of
functional dependencies. Perhaps the kind of C should include the
functional dependencies of C?

Etienne Laurin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[AntC]

Iavor Diatchki <iavor.diatchki <at> gmail.com> writes:

>
> Hello,
>
> the notion of a functional dependency is well established, and it was used
well before it was introduced to Haskell (for example, take a look
at http://en.wikipedia.org/wiki/Functional_dependency).  So I'd be weary to
redefine it lightly.

Yes functional dependency is well established in relational algebra (set
theory actually) -- it's about values in attributes. But there's nothing
corresponding to typevars (I suppose you might call those patterns of values);
there's nothing like overlaps.

Perhaps instances with Fundeps should only use H98-style arguments? Perhaps we
should disallow overlaps with Fundeps (as Hugs does pretty-much)?

I can only understand tricky Fundeps by mentally translating them into type-
level functions (and I was doing that before type families/associated types
came along).

    class C a b    | a -> b            ===> type family CF a
    instance C a b                     ===> type instance CF a = b

And that type instance is rejected because `b' is not in scope.

Currently there are all sorts of tricks in instance declarations with overlaps
and Fundeps, to achieve the effect of type-level functions. You do end up with
instance arguments being all typevars, because the instance selection logic is
really going on inside the constraints, with type-level 'helper functions'.

Some of Oleg's instances are awesome (and almost impenetrable -- the TTypeable
code is a tour de force).

It's all so *dys-functional* (IMO).

My take is that we should abandon Fundeps, and concentrate on introducing
overlaps into type functions in a controlled way (what I've called 'dis-
overlapped overlaps'.)

AntC



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Iavor Diatchki]

Hello,

There is no problem if an instances uses a type family in it's assumption---the instances should be accepted only if GHC can see enough of the definition of the type family to ensure that the functional dependency holds.  This is exactly the same as what it would do to check that a super class constraint holds.

-Iavor

On Wed, May 30, 2012 at 11:14 PM, Etienne Laurin <[hidden email]> wrote:

2012/5/31 Iavor Diatchki <[hidden email]>:

> Hello,
>
> the notion of a functional dependency is well established, and it was used
> well before it was introduced to Haskell (for example, take a look
> at http://en.wikipedia.org/wiki/Functional_dependency).  So I'd be weary to
> redefine it lightly.

Indeed, GHC's functional dependencies are not the same. I see you have
already talked about this on the GHC bug tracker.

http://hackage.haskell.org/trac/ghc/ticket/1241

> 1. Check that an instance is consistent with itself.  For example, this should be rejected:
>
> instance C a b
>
> because it allows C Int Bool and C Int Char which violate the functional dependency.

This check may not always be as straightforward. When would this be a
valid instance?

instance K a b ⇒ C a b

With a few extra extensions, K could be a type family.

C currently has the kind (a -> b -> Constraint), with no mention of
functional dependencies. Perhaps the kind of C should include the
functional dependencies of C?

Etienne Laurin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Etienne Laurin]

Hello,

2012/6/1 Iavor Diatchki <[hidden email]>:
> There is no problem if an instances uses a type family in it's
> assumption---the instances should be accepted only if GHC can see enough of
> the definition of the type family to ensure that the functional dependency
> holds.  This is exactly the same as what it would do to check that a super
> class constraint holds.

GHC cannot see enough of the definition because type families are
open. The type instances are not guaranteed to all be in scope when
the class instance is defined.

2012/6/1 AntC <[hidden email]>:
> Some of Oleg's instances are awesome (and almost impenetrable -- the TTypeable
> code is a tour de force).
>
> It's all so *dys-functional* (IMO).

It's like a typed Prolog with a different order of evaluation.

> My take is that we should abandon Fundeps, and concentrate on introducing
> overlaps into type functions in a controlled way (what I've called 'dis-
> overlapped overlaps'.)

Abandoning fundeps would be a sad day for type-level programming.
There are many things other than overlaps that you can do with fundeps
and constraint kinds that you cannot currently do with type families,
such as:

- Partial application or higher-order programming.
- Short-circuit evaluation, lazy evaluation or type-level case.

To study the differences, I have been porting parts of the Prelude to
both type classes and type families.

http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type.hs
http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type/Families.hs

Etienne Laurin

> On Wed, May 30, 2012 at 11:14 PM, Etienne Laurin <[hidden email]> wrote:
>> > 1. Check that an instance is consistent with itself.  For example, this
>> > should be rejected:
>> >
>> > instance C a b
>> >
>> > because it allows C Int Bool and C Int Char which violate the functional
>> > dependency.
>>
>> This check may not always be as straightforward. When would this be a
>> valid instance?
>>
>> instance K a b ⇒ C a b
>>
>> With a few extra extensions, K could be a type family.
>>
>> C currently has the kind (a -> b -> Constraint), with no mention of
>> functional dependencies. Perhaps the kind of C should include the
>> functional dependencies of C?

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Simon Peyton-Jones]

| > My take is that we should abandon Fundeps, and concentrate on
| > introducing overlaps into type functions in a controlled way (what
| > I've called 'dis- overlapped overlaps'.)
|
| Abandoning fundeps would be a sad day for type-level programming.
| There are many things other than overlaps that you can do with fundeps
| and constraint kinds that you cannot currently do with type families,
| such as:
|
| - Partial application or higher-order programming.
| - Short-circuit evaluation, lazy evaluation or type-level case.

Etienne, I think it would be a good service to make Haskell wiki page describing the difference between fundeps and type families, and in particular describing things that can be done with the former but not the latter.

The standard encoding of fundeps using type families is this:

With fundeps
        class C a b | a -> b
With type failies
        class (F a ~ b) => C a b where
        type F a

The merit of a wiki page would be to be a single place to find the discussion, the "standard encoding" and examples of where the standard encoding fails.

Simon
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[AntC]

Simon Peyton-Jones <simonpj <at> microsoft.com> writes:

>
> | > My take is that we should abandon Fundeps, and concentrate on
> | > introducing overlaps into type functions in a controlled way (what
> | > I've called 'dis- overlapped overlaps'.)
> |
> | Abandoning fundeps would be a sad day for type-level programming.
> | There are many things other than overlaps that you can do with fundeps
> | and constraint kinds that you cannot currently do with type families,
> | such as:
> |
> | - Partial application or higher-order programming.
> | - Short-circuit evaluation, lazy evaluation or type-level case.
>
> Etienne, I think it would be a good service to make Haskell wiki page

describing the difference between
> fundeps and type families, and in particular describing things that can be
done with the former but not the latter.
>
>
> Simon
>
+1 That would be great. I'll link to Etienne's wiki from the Discussion page
I've started for NewAxioms http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

In particular, it would be good to tease out where we're getting interference
or inter-dependence between different type-level extensions:
    Overlaps
    Fundeps
    UndecidableInstances (that is, breaking the coverage conditions)
    ScopedTypeVariables

Given that that the Fundeps idea is taken from relational theory, and
relations is just another way of representing functions, there ought to be
close correspondence to type-level functions.

To me, NewAxioms is aiming at type-level case, to provide a different style of
defining type functions, as well as dis-overlapping overlaps.

AntC


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Etienne Laurin]

>> | Abandoning fundeps would be a sad day for type-level programming.
>> | There are many things other than overlaps that you can do with fundeps
>> | and constraint kinds that you cannot currently do with type families,
>> | such as:
>> |
>> | - Partial application or higher-order programming.
>> | - Short-circuit evaluation, lazy evaluation or type-level case.
>>
>> Etienne, I think it would be a good service to make Haskell wiki page
> describing the difference between
>> fundeps and type families, and in particular describing things that can be
> done with the former but not the latter.
>>
>>
>> Simon

Thanks for the idea. Here it is.

http://hackage.haskell.org/trac/ghc/wiki/TFvsFD

I posted my comments on the matter along with many additional comments
and examples that I found.

> +1 That would be great. I'll link to Etienne's wiki from the Discussion page
> I've started for NewAxioms http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
>
> In particular, it would be good to tease out where we're getting interference
> or inter-dependence between different type-level extensions:
>    Overlaps
>    Fundeps
>    UndecidableInstances (that is, breaking the coverage conditions)
>    ScopedTypeVariables

I did not check what extensions were turned on in my examples.

> Given that that the Fundeps idea is taken from relational theory, and
> relations is just another way of representing functions, there ought to be
> close correspondence to type-level functions.

I put a few examples of the unexpected behaviour of Fundeps on the Wiki page.

> To me, NewAxioms is aiming at type-level case, to provide a different style of
> defining type functions, as well as dis-overlapping overlaps.

I am eager to see that in action.

Etienne Laurin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Gábor Lehel]

On Tue, Jun 5, 2012 at 4:18 AM, Etienne Laurin <[hidden email]> wrote:
>
> Thanks for the idea. Here it is.
>
> http://hackage.haskell.org/trac/ghc/wiki/TFvsFD
>
> I posted my comments on the matter along with many additional comments
> and examples that I found.
>

Thanks!

One part is confusing me.

In the section on "Partial application", you write:

> Type synonyms can manipulate constraint kinds but can not use them. The following code doesn't make sense.
> class (f :<$>: a) ~ b =>  FMap (f :: * -> * -> Constraint) a b
>  where type f :<$>: a
> instance FMap f (HJust a) b
>   where type f :<$>: (HJust a) = f a b => b

The class definition looks like it's meant to parallel the earlier FDs
version of FMap by using the "standard encoding" of FDs with TFs, but
the instance declaration doesn't. Is it meant to be demonstrating
something else?

The encoded version would be:

instance (f a b) => FMap f (HJust a) (HJust b)
  where type f :<$>: (HJust a) = HJust b

and I think this actually demonstrates a *different* limitation, namely that

> The RHS of an associated type declaration mentions type variable `b'
>   All such variables must be bound on the LHS

which means that the standard encoding doesn't work for this case.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Gábor Lehel]

On Tue, Jun 5, 2012 at 2:25 PM, Gábor Lehel <[hidden email]> wrote:

> The encoded version would be:
>
> instance (f a b) => FMap f (HJust a) (HJust b)
>  where type f :<$>: (HJust a) = HJust b
>
> and I think this actually demonstrates a *different* limitation, namely that
>
>> The RHS of an associated type declaration mentions type variable `b'
>>   All such variables must be bound on the LHS
>
> which means that the standard encoding doesn't work for this case.

From a reddit comment[1] by Reiner Pope it turns out you can actually do this:

instance (f a b) => FMap f (HJust a) (HJust b) where
    type f :<$>: (HJust a) = HJust (f :<$>: a)

A bit more awkward to write, but we're back to TFs not having any
expressivity problem in this department.

[1] http://www.reddit.com/r/haskell/comments/ut85i/a_few_typefamilies_nuggets/c4ygefh

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe