New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Instance apartness guards #56

Closed
wants to merge 22 commits into
base: master
from

Conversation

Projects
None yet
8 participants
@AntC2

AntC2 commented Jun 15, 2017

This proposal tackles the thorny topic of Overlapping instances, for both type classes and Type Families/Associated types, by annotating instance heads with type-level apartness Guards. Type-level disequality predicates appear in Sulzmann & Stuckey 2002; in the type-level ‘case selection’ in HList 2004; and in various guises in Haskell cafe discussions in following years. This proposal builds on the apartness testing implemented as part of the Closed Type Families work.

rendered

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jun 19, 2017

To assess this proposal against SPJ's 2010 desiderata (message also linked from 'Motivation', at "well-known") at foot of message:

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

('FDL' is an imagined Haskell with Functional Dependencies, overlapping instances and L = local type constraints, such as inside existentials or GADTs. For historical context note that as at 2010 Haskell had Type Functions but no overlapping/Closed Type Functions; superclass constraints with Type Functions and equality constraints (~) were understood/under development, but not released. So there was no 'road miles' on using that combo instead of FunDeps. The bulk of the message considers the effect on instance selection for class constraints within GADTs under various overlapping/imported instances scenarios.)

  1. Yes this proposal specifies eager checking for inconsistent FD and overlapping instances, across modules. (That is, after taking guards into account.)
    So at import time, all instances must be cross-checked, even if the importing module does not declare instances itself. (This catches the notorious diamond imports.) This eager checking is as Type Families apply currently.

  2. Yes overlap (of instance heads) is only resolved once a unique instance can match, after taking guards into account. Because each instance must be apart from each other (after taking guards into account), once a wanted constraint is resolved to an instance, that must be the unique instance.

  3. No this proposal does not require all (overlapping) instance be in the same module; nor (if they are in the same module) that they be in a closed cluster as with Closed Type Families or Instance Chains. Essentially because there are no overlapping instances (after taking guards into account).

To explain some of the motivation around requiring overlapping instances in the same module:

But that [insisting on a single module] loses part of the point of overlap in the first place, namely to provide a generic instance and then later override it.

Yes providing a generic instance was the style at the time. (I'd say that style was already in decline by 2010, precisely because of the importing/overlapping difficulties.) Notice that the generic instance could only be using bare type vars in the instance head:

class C a b c | a b -> c  where ...
instance (TypeCast c T) => C a b c where ...     -- constraint to 'improve' c under the FD, same effect as (~)

So the instance body could know nothing about the types of a b c; and really all it could do would be to issue a type-level error message. That message could at best be more helpful than "No instance for ...".

Contrast that HList's catch-all instances at least know there's a constructor HCons e' l'.

Under this proposal, you still can't write generic 'catch-all' instances like that; unless you know all the possible type constructors that you intend it to overlap; then you can explicitly push the not-so-generic instance apart from them.

Does anybody still write in that catch-all generic instance style? What are the use cases?

AntC2 commented Jun 19, 2017

To assess this proposal against SPJ's 2010 desiderata (message also linked from 'Motivation', at "well-known") at foot of message:

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

('FDL' is an imagined Haskell with Functional Dependencies, overlapping instances and L = local type constraints, such as inside existentials or GADTs. For historical context note that as at 2010 Haskell had Type Functions but no overlapping/Closed Type Functions; superclass constraints with Type Functions and equality constraints (~) were understood/under development, but not released. So there was no 'road miles' on using that combo instead of FunDeps. The bulk of the message considers the effect on instance selection for class constraints within GADTs under various overlapping/imported instances scenarios.)

  1. Yes this proposal specifies eager checking for inconsistent FD and overlapping instances, across modules. (That is, after taking guards into account.)
    So at import time, all instances must be cross-checked, even if the importing module does not declare instances itself. (This catches the notorious diamond imports.) This eager checking is as Type Families apply currently.

  2. Yes overlap (of instance heads) is only resolved once a unique instance can match, after taking guards into account. Because each instance must be apart from each other (after taking guards into account), once a wanted constraint is resolved to an instance, that must be the unique instance.

  3. No this proposal does not require all (overlapping) instance be in the same module; nor (if they are in the same module) that they be in a closed cluster as with Closed Type Families or Instance Chains. Essentially because there are no overlapping instances (after taking guards into account).

To explain some of the motivation around requiring overlapping instances in the same module:

But that [insisting on a single module] loses part of the point of overlap in the first place, namely to provide a generic instance and then later override it.

Yes providing a generic instance was the style at the time. (I'd say that style was already in decline by 2010, precisely because of the importing/overlapping difficulties.) Notice that the generic instance could only be using bare type vars in the instance head:

class C a b c | a b -> c  where ...
instance (TypeCast c T) => C a b c where ...     -- constraint to 'improve' c under the FD, same effect as (~)

So the instance body could know nothing about the types of a b c; and really all it could do would be to issue a type-level error message. That message could at best be more helpful than "No instance for ...".

Contrast that HList's catch-all instances at least know there's a constructor HCons e' l'.

Under this proposal, you still can't write generic 'catch-all' instances like that; unless you know all the possible type constructors that you intend it to overlap; then you can explicitly push the not-so-generic instance apart from them.

Does anybody still write in that catch-all generic instance style? What are the use cases?

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jun 20, 2017

I guess type inference (instance selection) needs to provide an evidence term for the selection. For apartness guards, that means evidence that α /~ (Maybe _), for example (where α is some skolem).

That could look like α ~ ( α1, α2). That is, refined only so far as to find a type constructor that's apart.

For a guard like f /~ (_ _), we need evidence like α ~ Int, for example. That is, refined far enough to find a type constructor that has no arguments. (Note we require comparands to be same-kinded.)

AntC2 commented Jun 20, 2017

I guess type inference (instance selection) needs to provide an evidence term for the selection. For apartness guards, that means evidence that α /~ (Maybe _), for example (where α is some skolem).

That could look like α ~ ( α1, α2). That is, refined only so far as to find a type constructor that's apart.

For a guard like f /~ (_ _), we need evidence like α ~ Int, for example. That is, refined far enough to find a type constructor that has no arguments. (Note we require comparands to be same-kinded.)

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jun 20, 2017

Another possible solution for the awkward equation in the gnarly example. This treats the arguments symmetrically:

type instance Equiv (t d) (t' e) | t /~ t'                             = False    -- 4c
type instance Equiv  f     g     | f /~ g, (f, g) /~ ((_ _), (_ _))   = False    -- 4d

Not all the comparands are whole parameters from the head. For 4a we could go (t d) /~ (t' _). That pile-up of wildcards for 4d makes me queazy.

AntC2 commented Jun 20, 2017

Another possible solution for the awkward equation in the gnarly example. This treats the arguments symmetrically:

type instance Equiv (t d) (t' e) | t /~ t'                             = False    -- 4c
type instance Equiv  f     g     | f /~ g, (f, g) /~ ((_ _), (_ _))   = False    -- 4d

Not all the comparands are whole parameters from the head. For 4a we could go (t d) /~ (t' _). That pile-up of wildcards for 4d makes me queazy.

@MarLinn

This comment has been minimized.

Show comment
Hide comment
@MarLinn

MarLinn Jun 24, 2017

I don't see the reason why the inequality needs funny syntax. Can't it be a normal constraint?

class {-# INSTANCEGUARDS #-} C a b where f :: a -> b -> String
instance C Int b                   where f _ _ = "C Int b"
instance (a /~ Int) => C a Bool    where f _ _ = "C a Bool"

That should make the semantics quite obvious.

MarLinn commented Jun 24, 2017

I don't see the reason why the inequality needs funny syntax. Can't it be a normal constraint?

class {-# INSTANCEGUARDS #-} C a b where f :: a -> b -> String
instance C Int b                   where f _ _ = "C Int b"
instance (a /~ Int) => C a Bool    where f _ _ = "C a Bool"

That should make the semantics quite obvious.

@mniip

This comment has been minimized.

Show comment
Hide comment
@mniip

mniip Jun 24, 2017

@MarLinn Ironically, if we kept the current instance selection rules (which I suppose are the ones you're calling "quite obvious"), your code would never work.

An instance is first selected - by looking only at the instance head, and then its constraints are added. If the constraints fail to satisfy, that's a type error. There is no backtracking and another instance is not selected.

So your proposed syntax either 1) introduces backtracking into instance resolution 2) introduces semantics that are anything but obvious (during instance resolution we have to scan for apartness constraints in potentially nested tuple of constraints).

In fact, you can define a (/~) :: k -> l -> Constraint right now:

type family Eqs :: k -> l -> Bool where
    Eqs a a = True
    Eqs a b = False

type (/~) a b = Eqs a b ~ False

The whole idea of this proposal is to make use of such inequality during instance selection.

mniip commented Jun 24, 2017

@MarLinn Ironically, if we kept the current instance selection rules (which I suppose are the ones you're calling "quite obvious"), your code would never work.

An instance is first selected - by looking only at the instance head, and then its constraints are added. If the constraints fail to satisfy, that's a type error. There is no backtracking and another instance is not selected.

So your proposed syntax either 1) introduces backtracking into instance resolution 2) introduces semantics that are anything but obvious (during instance resolution we have to scan for apartness constraints in potentially nested tuple of constraints).

In fact, you can define a (/~) :: k -> l -> Constraint right now:

type family Eqs :: k -> l -> Bool where
    Eqs a a = True
    Eqs a b = False

type (/~) a b = Eqs a b ~ False

The whole idea of this proposal is to make use of such inequality during instance selection.

@MarLinn

This comment has been minimized.

Show comment
Hide comment
@MarLinn

MarLinn Jun 24, 2017

@mniip I guess I was arguing on a different level of semantics. Not precise semantics of evaluation but intuitive semantics.
"Intuition" is arguable, so to clarify: it appears to me that quite a few people have been bitten by this fact that constraints are "added" post-resolution. Once you know it it's a nice trick to work around shortcomings of the resolver – but it's neither very useful beyond that, nor does it make sense until you take a look under the hood. In other words, it's an implementation detail that leaks out. Which, in my book, is a good argument to change it.

Checking constraints is a necessary step anyway. So the simplest implementation would be to keep options around and just defer the pruning to later. That's not precisely backtracking, but along the line. It also doesn't sound very performant yet. But it has the benefit of adding more value to existing syntax instead of introducing new syntax just because of some implementation details.

Or approached from another side: After this proposal, there will be two possible types of constraints to add on the right-hand side. No equality constraints yet, no type family applications yet, but it appears like it's only a matter of time until they're proposed. Before long, left-hand-side and right-hand-side constraints will probably converge. Now it might be that this separation still makes sense then, and that there are qualitative differences between intra-selection and post-selection constraints that I don't see or understand right now. Quite possibly. In this case, it might be worth exploring what we know about these differences right now and at least discuss how this proposal fits into that current knowledge in an appendix. Not for me, but as documentation for those that will want to add more of them.

MarLinn commented Jun 24, 2017

@mniip I guess I was arguing on a different level of semantics. Not precise semantics of evaluation but intuitive semantics.
"Intuition" is arguable, so to clarify: it appears to me that quite a few people have been bitten by this fact that constraints are "added" post-resolution. Once you know it it's a nice trick to work around shortcomings of the resolver – but it's neither very useful beyond that, nor does it make sense until you take a look under the hood. In other words, it's an implementation detail that leaks out. Which, in my book, is a good argument to change it.

Checking constraints is a necessary step anyway. So the simplest implementation would be to keep options around and just defer the pruning to later. That's not precisely backtracking, but along the line. It also doesn't sound very performant yet. But it has the benefit of adding more value to existing syntax instead of introducing new syntax just because of some implementation details.

Or approached from another side: After this proposal, there will be two possible types of constraints to add on the right-hand side. No equality constraints yet, no type family applications yet, but it appears like it's only a matter of time until they're proposed. Before long, left-hand-side and right-hand-side constraints will probably converge. Now it might be that this separation still makes sense then, and that there are qualitative differences between intra-selection and post-selection constraints that I don't see or understand right now. Quite possibly. In this case, it might be worth exploring what we know about these differences right now and at least discuss how this proposal fits into that current knowledge in an appendix. Not for me, but as documentation for those that will want to add more of them.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jun 25, 2017

Thanks @mniip , you're quite correct.

I'm very carefully not describing these guards as "constraints", because that would indeed be confusing. If you want a different word: "restraints" -- that is, they restrain the instance from applying.

it appears to me that quite a few people have been bitten by this fact that constraints are "added" post-resolution.

Yes they have. It's a common newbie's mistake. So I've deliberately used syntax to the right of the instance head, to look as much as possible like guards at the term level. If you think that's still too confusing, by all means suggest alternative syntax.

... it's an implementation detail that leaks out. ...

Type improvement/type inference is hardly a "detail", IMO. It's why we have FunDeps and Type Families and equality constraints (~), so the programmer can guide improvement.

Which, in my book, is a good argument to change it.

The merit of this proposal is it doesn't change any of the underlying semantics. It's chiefly providing prettier/more readable syntax for what you can write already. (And in a significant number of cases, you can avoid adding post-resolution constraints altogther. I'm sure you'll see that as a Good Thing. ;-)

If you want to change the semantics of pre-/post- instance selection, that would be a very different subject for a proposal. I note that none of the Alternatives considered are proposing anything like that.

Before long, left-hand-side and right-hand-side constraints will probably converge.

Well, Type Family equations don't have (left-hand-side) constraints, so no. And guards are not "constraints", so no again. Guards can only be type comparisons, no class applications, so no a third time. (Compare that at the term level, I can put arbitrarily complex expressions in guards: just the same sort of expressions as I can put to the right of the -> in the case body. Does that confuse anybody?) Perhaps if we could go back 25+ years instance syntax should look more like term-level case branches like this:

instance C a b | a /~ Int  => (b ~ Bool) where ...

(I hear howls of anguish coming from GHC HQ.)

AntC2 commented Jun 25, 2017

Thanks @mniip , you're quite correct.

I'm very carefully not describing these guards as "constraints", because that would indeed be confusing. If you want a different word: "restraints" -- that is, they restrain the instance from applying.

it appears to me that quite a few people have been bitten by this fact that constraints are "added" post-resolution.

Yes they have. It's a common newbie's mistake. So I've deliberately used syntax to the right of the instance head, to look as much as possible like guards at the term level. If you think that's still too confusing, by all means suggest alternative syntax.

... it's an implementation detail that leaks out. ...

Type improvement/type inference is hardly a "detail", IMO. It's why we have FunDeps and Type Families and equality constraints (~), so the programmer can guide improvement.

Which, in my book, is a good argument to change it.

The merit of this proposal is it doesn't change any of the underlying semantics. It's chiefly providing prettier/more readable syntax for what you can write already. (And in a significant number of cases, you can avoid adding post-resolution constraints altogther. I'm sure you'll see that as a Good Thing. ;-)

If you want to change the semantics of pre-/post- instance selection, that would be a very different subject for a proposal. I note that none of the Alternatives considered are proposing anything like that.

Before long, left-hand-side and right-hand-side constraints will probably converge.

Well, Type Family equations don't have (left-hand-side) constraints, so no. And guards are not "constraints", so no again. Guards can only be type comparisons, no class applications, so no a third time. (Compare that at the term level, I can put arbitrarily complex expressions in guards: just the same sort of expressions as I can put to the right of the -> in the case body. Does that confuse anybody?) Perhaps if we could go back 25+ years instance syntax should look more like term-level case branches like this:

instance C a b | a /~ Int  => (b ~ Bool) where ...

(I hear howls of anguish coming from GHC HQ.)

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Jun 27, 2017

Contributor

This is a long proposal (which I encouraged @AntC2 to write), and I'm surprised it hasn't attracted more commentary. Perhaps a summary is in order:

This proposal introduces instance guards, a new form of type constraint that can be used during instance selection (that is, before committing to an instance). This applies to all kinds of instances: of classes, type families, and data families. Only one form of guard is currently proposed: an apartness constraint. So, if we have

instance C a b | b /~ Bool

then this instance is chosen only when b is apart from Bool.

Because it's hard to see how to marry instance guards with overlapping instances, these features cannot be used in concert. To avoid this possibility, classes whose instances (may) have guards are required to be marked with the {-# INSTANCEGUARDS #-} pragma. Writing an overlapping instance of such a class is an error. The overlap check here is eager, like it is for type family instances.

Note that, due to the way apartness is defined, this new feature does not induce backtracking into the solver and can be implemented straightforwardly, in my opinion.

Contributor

goldfirere commented Jun 27, 2017

This is a long proposal (which I encouraged @AntC2 to write), and I'm surprised it hasn't attracted more commentary. Perhaps a summary is in order:

This proposal introduces instance guards, a new form of type constraint that can be used during instance selection (that is, before committing to an instance). This applies to all kinds of instances: of classes, type families, and data families. Only one form of guard is currently proposed: an apartness constraint. So, if we have

instance C a b | b /~ Bool

then this instance is chosen only when b is apart from Bool.

Because it's hard to see how to marry instance guards with overlapping instances, these features cannot be used in concert. To avoid this possibility, classes whose instances (may) have guards are required to be marked with the {-# INSTANCEGUARDS #-} pragma. Writing an overlapping instance of such a class is an error. The overlap check here is eager, like it is for type family instances.

Note that, due to the way apartness is defined, this new feature does not induce backtracking into the solver and can be implemented straightforwardly, in my opinion.

@danidiaz danidiaz referenced this pull request Jul 1, 2017

Closed

Custom type errors #59

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jul 5, 2017

Thank you @goldfirere for the excellent (brief!) summary.

A detail that might have escaped: guards can help in applying the FunDep consistency conditions, by 'pushing apart' the argument side of FunDeps that would otherwise overlap and thereby give inconsistent result sides.

GHC's FunDep consistency checking is currently rather lax. And for good reason: there's lots of code exploiting that; I've written plenty myself. With guards there's an opportunity to tighten that check. I haven't writen that into the proposal (yet). I'd appreciate feedback ...

As a result of the laxness, there's some corner cases of FunDeps you can write that cannot be equivalently expressed using Type Families and Equality constraints, not even with Closed Type Families. Trac #10675 is an example. Richard's comment is the example is "bogus". I agree. But it's difficult to pin-point the bogusness and 'fix' the consistency check without breaking (legitimate?) code that exploits the laxness. So #10675 remains unfixed.

Currently the FunDep consistency check goes:

  • If the argument side of two instances overlap;
  • unify those arguments, yielding a substitution;
  • apply that substitution to the result side.
  • If the results unify, they're consistent, so pass the check.

Arguably that last check should be:

  • If the results are identical, they're consistent; but
  • if they merely unify, that's not consistent enough.

Trac #10675's example is:

class C x a b | a -> b where
  op :: x -> a -> b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]

These instances do not overlap. Nevertheless the argument sides of the FunDep a -> b in this case don't just overlap, they're identical [x]. So GHC succeeds in unifying the result sides [x] ~ [Maybe y], getting the substitution x :-> Maybe y. Then an expression like:

f x = op True [x]

(which should use only the first instance) gets an inferred signature f :: Maybe x -> [Maybe x]. Definitely bogus.

With the tighter check on FunDep consistency, as above, those instances must be rejected: the result sides after substitution are not identical [x] /= [Maybe y].

But under those tighter rules, code like this (relied on by many type-level hackers) would also fail the check:

class TypeEq a b (p :: Bool) | a b -> p
instance                TypeEq a a True
instance (p ~ False) => TypeEq a b p

The argument sides of the FunDep unify, with substitution a ~ b. Under that substitution, the result sides unify on p ~ True; but are not identical. Furthermore the consistency check ignores the constraint (p ~ False), which would/should make the consistency check fail: p ~ True not unifiable with p ~ False.

With the tighter consistency check and Instance Guards, that relied-on code goes:

class {-# INSTANCEGUARDS #-}TypeEq a b (p :: Bool) | a b -> p
instance TypeEq a a True
instance TypeEq a b False | a /~ b

(Firstly note this is easier to read: the result False is directly in the instance head, not deferred to an Equality constraint. Also it no longer needs UndecidableInstances.) Applying the FunDep consistency check, we can unify the argument sides on a ~ b. But before substituting into the result sides, substitute into the guard: a /~ a. A contradiction, so accept the instances; don't consider the result sides.

AntC2 commented Jul 5, 2017

Thank you @goldfirere for the excellent (brief!) summary.

A detail that might have escaped: guards can help in applying the FunDep consistency conditions, by 'pushing apart' the argument side of FunDeps that would otherwise overlap and thereby give inconsistent result sides.

GHC's FunDep consistency checking is currently rather lax. And for good reason: there's lots of code exploiting that; I've written plenty myself. With guards there's an opportunity to tighten that check. I haven't writen that into the proposal (yet). I'd appreciate feedback ...

As a result of the laxness, there's some corner cases of FunDeps you can write that cannot be equivalently expressed using Type Families and Equality constraints, not even with Closed Type Families. Trac #10675 is an example. Richard's comment is the example is "bogus". I agree. But it's difficult to pin-point the bogusness and 'fix' the consistency check without breaking (legitimate?) code that exploits the laxness. So #10675 remains unfixed.

Currently the FunDep consistency check goes:

  • If the argument side of two instances overlap;
  • unify those arguments, yielding a substitution;
  • apply that substitution to the result side.
  • If the results unify, they're consistent, so pass the check.

Arguably that last check should be:

  • If the results are identical, they're consistent; but
  • if they merely unify, that's not consistent enough.

Trac #10675's example is:

class C x a b | a -> b where
  op :: x -> a -> b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]

These instances do not overlap. Nevertheless the argument sides of the FunDep a -> b in this case don't just overlap, they're identical [x]. So GHC succeeds in unifying the result sides [x] ~ [Maybe y], getting the substitution x :-> Maybe y. Then an expression like:

f x = op True [x]

(which should use only the first instance) gets an inferred signature f :: Maybe x -> [Maybe x]. Definitely bogus.

With the tighter check on FunDep consistency, as above, those instances must be rejected: the result sides after substitution are not identical [x] /= [Maybe y].

But under those tighter rules, code like this (relied on by many type-level hackers) would also fail the check:

class TypeEq a b (p :: Bool) | a b -> p
instance                TypeEq a a True
instance (p ~ False) => TypeEq a b p

The argument sides of the FunDep unify, with substitution a ~ b. Under that substitution, the result sides unify on p ~ True; but are not identical. Furthermore the consistency check ignores the constraint (p ~ False), which would/should make the consistency check fail: p ~ True not unifiable with p ~ False.

With the tighter consistency check and Instance Guards, that relied-on code goes:

class {-# INSTANCEGUARDS #-}TypeEq a b (p :: Bool) | a b -> p
instance TypeEq a a True
instance TypeEq a b False | a /~ b

(Firstly note this is easier to read: the result False is directly in the instance head, not deferred to an Equality constraint. Also it no longer needs UndecidableInstances.) Applying the FunDep consistency check, we can unify the argument sides on a ~ b. But before substituting into the result sides, substitute into the guard: a /~ a. A contradiction, so accept the instances; don't consider the result sides.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Aug 1, 2017

Contributor

That's a a mega-proposal. Well written and thorough. But a bid daunting.

In some ways it's less modular than overlapping instances. Eg today I can say instance {-# OVERLAPPABLE #-} Eq [a], and later decide what overlaps to add. With guards I must say which cases this instance does not handle. So I must think of these instances together. Would some form of closed instance declarations be better? e.g. The translation of closed family Equiv to guards make me love closed families more than guards!

If we put all this in, is there anything else we can take out?

Can I say instance C a | a /~ [b] meaning "a is apart from list-of-anything"? The proposal says not, but I don't know why.

I don't have a clear verdict.

Contributor

simonpj commented Aug 1, 2017

That's a a mega-proposal. Well written and thorough. But a bid daunting.

In some ways it's less modular than overlapping instances. Eg today I can say instance {-# OVERLAPPABLE #-} Eq [a], and later decide what overlaps to add. With guards I must say which cases this instance does not handle. So I must think of these instances together. Would some form of closed instance declarations be better? e.g. The translation of closed family Equiv to guards make me love closed families more than guards!

If we put all this in, is there anything else we can take out?

Can I say instance C a | a /~ [b] meaning "a is apart from list-of-anything"? The proposal says not, but I don't know why.

I don't have a clear verdict.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Aug 1, 2017

That's a mega-proposal. Well written and thorough. But a bid daunting.

Thank you, and fair comment. I've been (over-)thinking this since at least 2012 alternative to Closed Type Families/see "Disequality constraints"

In some ways it's less modular than overlapping instances. Eg today I can say instance {-# OVERLAPPABLE #-} Eq [a], and later decide what overlaps to add. ...

That's the danger point with overlaps: I put instance Eq [a] in module A, and all calls in that module resolve to it. I put instance Eq [Int] in module B which imports A. Now an identical call in B does something different.

EDIT: Errk! I might have misunderstood Simon's point. He said {-# OVERLAPPABLE #-}. Adding 'wider' instances later/elsewhere is fine/no problem. Just go instance Eq a | a /~ [_] to de-overlap the already-declared instance.

With guards I must say which cases this instance does not handle. So I must think of these instances together. Would some form of closed instance declarations be better?

Yes you must think of those instances together. So exactly the same as closed instances. I think the two approaches are very similar within a single module. What I can't do with closed instances is put all instance Eq [<whatever>] in module A and all the instance Eq (Maybe <whatever>) in module B. Or instance Eq (T <whatever>) in module C, which is where I declare type T. IOW closed instances must be globally all-in-one-place. (Instance Chains, Morris+Jones, are more flexible.)

I think I could spec a mechanical translation from closed instances to apartness guards. (That's why the proposal works through an example in detail. As I understand from Richard, CTFs under the hood are using a similar mechanism to guards, to try to help progress.) But less hope of a translation for overlapping type class instances (esp Incoherent ones).

e.g. The translation of closed family Equiv to guards make me love closed families more than guards!

For Type Families, I agree the equations are easier to read (each on a line). But you should also look aesthetically at Instance Chains (or Morris+Eisenberg Closed Classes). Now the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic. To understand each instance, you have to read through the chain to understand what pattern of types this applies for. Horrible!

If we put all this in, is there anything else we can take out?

Yes (long term plan): take out Closed Type Families (or translate them to apartness guards); take out IncoherentInstances; take out OverlappingInstances; take out UndecidableInstances. Possibly no need to implement "Dysfunctional Functional Dependencies". Resolve Iavor's concerns wrt GHC's dubious "Instances inconsistent with Functional Dependencies" check for non-full dependencies -- by making GHC behave like Jones' original spec for FunDeps/the FDs through CHRs paper. Resolve some of the long-standing tickets around the interaction of overlaps and FunDeps. Make 'Orphan Instances' less problematic, because they can't overlap or get overlapped.

Oh, and I think we have a better basis for Injective Type Families (that is, where result with one arg determines the other arg).

It would have been better to put in this proposal before all that other stuff -- circa 1998. There might have been a different ''History of Haskell: being guarded with class'' ;-).

(I'm a little miffed at your "all this": there's no new type-level technology; the mechanisms are only unification and substitution and apartness checks; you can achieve this today in GHC, as does HList, it would be just very fiddly and verbose. In fact you could achieve it in 2004. The type theory was sketched in 2002, Sulzmann+Stuckey/Chameleon.)

Can I say instance C a | a /~ [b] meaning "a is apart from list-of-anything"? The proposal says not, but I don't know why.

Yes you can say instance C a | a /~ [_] (underscore is wildcard point 4) to mean that. The proposal says merely that you cannot introduce a new type var (viz b) within the guard. Precisely because if all type inference knows is a /~ [b] then a is not a list so it's meaningless (and unsafe!) to talk about the list's based-on type.

I don't have a clear verdict.

Thank you very much for taking the time to review.

AntC2 commented Aug 1, 2017

That's a mega-proposal. Well written and thorough. But a bid daunting.

Thank you, and fair comment. I've been (over-)thinking this since at least 2012 alternative to Closed Type Families/see "Disequality constraints"

In some ways it's less modular than overlapping instances. Eg today I can say instance {-# OVERLAPPABLE #-} Eq [a], and later decide what overlaps to add. ...

That's the danger point with overlaps: I put instance Eq [a] in module A, and all calls in that module resolve to it. I put instance Eq [Int] in module B which imports A. Now an identical call in B does something different.

EDIT: Errk! I might have misunderstood Simon's point. He said {-# OVERLAPPABLE #-}. Adding 'wider' instances later/elsewhere is fine/no problem. Just go instance Eq a | a /~ [_] to de-overlap the already-declared instance.

With guards I must say which cases this instance does not handle. So I must think of these instances together. Would some form of closed instance declarations be better?

Yes you must think of those instances together. So exactly the same as closed instances. I think the two approaches are very similar within a single module. What I can't do with closed instances is put all instance Eq [<whatever>] in module A and all the instance Eq (Maybe <whatever>) in module B. Or instance Eq (T <whatever>) in module C, which is where I declare type T. IOW closed instances must be globally all-in-one-place. (Instance Chains, Morris+Jones, are more flexible.)

I think I could spec a mechanical translation from closed instances to apartness guards. (That's why the proposal works through an example in detail. As I understand from Richard, CTFs under the hood are using a similar mechanism to guards, to try to help progress.) But less hope of a translation for overlapping type class instances (esp Incoherent ones).

e.g. The translation of closed family Equiv to guards make me love closed families more than guards!

For Type Families, I agree the equations are easier to read (each on a line). But you should also look aesthetically at Instance Chains (or Morris+Eisenberg Closed Classes). Now the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic. To understand each instance, you have to read through the chain to understand what pattern of types this applies for. Horrible!

If we put all this in, is there anything else we can take out?

Yes (long term plan): take out Closed Type Families (or translate them to apartness guards); take out IncoherentInstances; take out OverlappingInstances; take out UndecidableInstances. Possibly no need to implement "Dysfunctional Functional Dependencies". Resolve Iavor's concerns wrt GHC's dubious "Instances inconsistent with Functional Dependencies" check for non-full dependencies -- by making GHC behave like Jones' original spec for FunDeps/the FDs through CHRs paper. Resolve some of the long-standing tickets around the interaction of overlaps and FunDeps. Make 'Orphan Instances' less problematic, because they can't overlap or get overlapped.

Oh, and I think we have a better basis for Injective Type Families (that is, where result with one arg determines the other arg).

It would have been better to put in this proposal before all that other stuff -- circa 1998. There might have been a different ''History of Haskell: being guarded with class'' ;-).

(I'm a little miffed at your "all this": there's no new type-level technology; the mechanisms are only unification and substitution and apartness checks; you can achieve this today in GHC, as does HList, it would be just very fiddly and verbose. In fact you could achieve it in 2004. The type theory was sketched in 2002, Sulzmann+Stuckey/Chameleon.)

Can I say instance C a | a /~ [b] meaning "a is apart from list-of-anything"? The proposal says not, but I don't know why.

Yes you can say instance C a | a /~ [_] (underscore is wildcard point 4) to mean that. The proposal says merely that you cannot introduce a new type var (viz b) within the guard. Precisely because if all type inference knows is a /~ [b] then a is not a list so it's meaningless (and unsafe!) to talk about the list's based-on type.

I don't have a clear verdict.

Thank you very much for taking the time to review.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Aug 2, 2017

Contributor

Please don't be miffed. It's good work -- just has a lot of implications.

That's the danger point with overlaps

I wasn't clear enough. Today with overlapping instances I can declare

instance {-# OVERLAPPABLE #-} Show a => Show [a]

in a library module, and then override it in a client module, written separately, later, by a different author

data T = ...
instance {-# OVERLAPPING #-} Show T

With guards I have to anticipate all the other instances, writing (I suppose)

instance Show [a] | a /~ T, a /~ S, a /~ whatever

Not only is that tiresome and anti-modular, it may not even be possible if the clients haven't been written when the library is designed. So I anticipate that there will be pressure to keep overlapping instances. Is that right or have I misunderstood?

What I can't do with closed instances is put all instance Eq [] in module A and all the instance Eq (Maybe ) in module B

I think you can!

module A where

class EqList a where
  (==) :: [a] -> [a] -> Bool

instance EqList a => Eq [a]
  (==) = A.(==)

and similarly for module B. We simply delegate to a specialised class. Now we can put all the instances for EqList in one place. We came across this for type families, where we wondered about "partly closed" families where you could have scattered sets of ordered equations something like

type instance F [a] where
  F [Int] = t1
  F [a]   = t1

type instance F (Maybe a) where
  F (Maybe Int) = t3
  F (Maybe a)   = t4

but then we realised that instead we can just make specialised closed families FList, FMaybe and so on. Much simpler!

Now the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic

I agree that is horrible. But writing guards is also tricky; that's why we have closed type families and top-to-bottom matching for term-level functions. If closed type families work well for the type-family case, I wonder if it'd be worth looking for a closed-instance syntax that was less horrible. eg

closed instance EqList a where
  instance EqList T = i1
  instance EqList S = i2
  instance EqList a = i3

instance i1 :: EqList T where ...
instance i2 :: EqList S where ...
instance i3 :: EqList a where ...

I'm just thinking aloud here. Having named instances could be useful in other ways (selective export).

Yes (long term plan)

I for one would find it helpful to have these impressively long list of points enumerated, with more info about each to show how the problem is solved. Killing many birds with one stone makes a proposal stronger.

Contributor

simonpj commented Aug 2, 2017

Please don't be miffed. It's good work -- just has a lot of implications.

That's the danger point with overlaps

I wasn't clear enough. Today with overlapping instances I can declare

instance {-# OVERLAPPABLE #-} Show a => Show [a]

in a library module, and then override it in a client module, written separately, later, by a different author

data T = ...
instance {-# OVERLAPPING #-} Show T

With guards I have to anticipate all the other instances, writing (I suppose)

instance Show [a] | a /~ T, a /~ S, a /~ whatever

Not only is that tiresome and anti-modular, it may not even be possible if the clients haven't been written when the library is designed. So I anticipate that there will be pressure to keep overlapping instances. Is that right or have I misunderstood?

What I can't do with closed instances is put all instance Eq [] in module A and all the instance Eq (Maybe ) in module B

I think you can!

module A where

class EqList a where
  (==) :: [a] -> [a] -> Bool

instance EqList a => Eq [a]
  (==) = A.(==)

and similarly for module B. We simply delegate to a specialised class. Now we can put all the instances for EqList in one place. We came across this for type families, where we wondered about "partly closed" families where you could have scattered sets of ordered equations something like

type instance F [a] where
  F [Int] = t1
  F [a]   = t1

type instance F (Maybe a) where
  F (Maybe Int) = t3
  F (Maybe a)   = t4

but then we realised that instead we can just make specialised closed families FList, FMaybe and so on. Much simpler!

Now the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic

I agree that is horrible. But writing guards is also tricky; that's why we have closed type families and top-to-bottom matching for term-level functions. If closed type families work well for the type-family case, I wonder if it'd be worth looking for a closed-instance syntax that was less horrible. eg

closed instance EqList a where
  instance EqList T = i1
  instance EqList S = i2
  instance EqList a = i3

instance i1 :: EqList T where ...
instance i2 :: EqList S where ...
instance i3 :: EqList a where ...

I'm just thinking aloud here. Having named instances could be useful in other ways (selective export).

Yes (long term plan)

I for one would find it helpful to have these impressively long list of points enumerated, with more info about each to show how the problem is solved. Killing many birds with one stone makes a proposal stronger.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Aug 2, 2017

That's the danger point with overlaps

I wasn't clear enough. Today with overlapping instances I can declare ...

instance {-# OVERLAPPABLE #-} Show a => Show [a]

in a library module, and then override it in a client module, written separately, later, by a different author

data T = ...
instance {-# OVERLAPPING #-} Show T

With guards I have to anticipate all the other instances, writing (I suppose)

Um, those instances don't overlap. Did you mean instance Show [T]?

What you describe is how the mtl library used to work. Except it didn't work, so it was rewritten to not use overlaps like that. The problem with writing a 'catch-all' instance in the library module is it leads to all sorts of surprising incoherence/silently changing behaviour from imports.

instance Show [a] | a /~ T, a /~ S, a /~ whatever

Not only is that tiresome and anti-modular, it may not even be possible if the clients haven't been written when the library is designed. ...

I'm not sure you've picked a strong example: instance Show [a] where { ...; show xs = showList xs; ...}. Now I can write the instance Show T where {...; showList xs = ...} to do custom stuff in my client module, don't need to change the library. That could be the basis for a design pattern.

Anyway, overlapping instances do tend to be tiresome and anti-modular. Closed instances don't address this requirement either. So adding guards to the catch-all instance in the library has the same burden as adding instances within the closed set.

So I anticipate that there will be pressure to keep overlapping instances. Is that right or have I misunderstood?

Yes I am anticipating in the short term, people will want to continue to use overlapping instances. In the longer term they can piecemeal (class-by-class) change over, replacing the overlap pragmas with guards -- only for the instances that do actually overlap.

What I can't do with closed instances is put all instance Eq [] in module A and all the instance Eq (Maybe ) in module B

I think you can!

module A where

class EqList a where
  (==) :: [a] -> [a] -> Bool

instance EqList a => Eq [a]
  (==) = A.(==)

and similarly for module B. We simply delegate to a specialised class. Now we can put all the instances for EqList in one place. We came across this for type families, ...

Yeah OK. (And RIchard made a similar point.) Now that I've seen it coded out, I'm even more put off by how verbose and non-perspicuous it is.

where we wondered about "partly closed" families where you could have scattered sets of ordered equations something like

type instance F [a] where
  F [Int] = t1
  F [a]   = t1

type instance F (Maybe a) where
  F (Maybe Int) = t3
  F (Maybe a)   = t4

Yes I recognise that proposal. It came from me. I continue to be disappointed it never happened. (But I prefer apartness guards.)

but then we realised that instead we can just make specialised closed families FList, FMaybe and so on. Much simpler!

Maybe simpler for the compiler-writers. You haven't convinced me it's simpler for the instance-writers.

Now (with closed classes) the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic

I agree that is horrible. But writing guards is also tricky; ...

Firstly, I think it's much easier to write the logic for an instance+guard stand-alone. More importantly the reader can understand it stand-alone. Secondly, the compiler can validate it is genuinely apart from any other instance. With a sequence of instances (especially if they're widely spread out with method overloads in-between), the logic is not so clear. And I think it's prone for the reader to mistake which patterns get selected by which instance decls. I'm saying this based on looking at some of the examples in the 'Instance Chains' paper. (Admittedly that has a lot of other fancy conditioning, like instance-level if and fail = backtrack.)

that's why we have closed type families and top-to-bottom matching for term-level functions.

With respect, I don't think you do exactly have top-to-bottom matching: In order to make progress with solving, CTF resolution tries to look for 'coincident overlap' by considering all of the equations, not necessarily in top-to-bottom sequence. From Richard's description, I think it's ended up working a lot more like apartness guards. My mental model is that all instances are 'competing' to be selected. Ordered equations is one way to prefer an instance out of several that might apply. Overlapping instances is another way (and not a very good one). The trouble with both those ways is the compiler has to entertain several instances that might apply. The advantage of apartness guards is the compiler knows the instance definitions are non-overlapping (after taking guards into account), so it can keep improving the types until at most one instance applies. Importantly, this doesn't involve search or backtracking.

If closed type families work well for the type-family case, ...

Yes they do work well from the equation-writer's point of view. Not so much under the hood. IMO it's confusing having two mechanisms: both stand-alone TF instances, associated type instances within stand-alone class instances and closed instances. I'd prefer to write more of my type instances as associated types; but currently that clashes horribly with overlaps.

I wonder if it'd be worth looking for a closed-instance syntax that was less horrible. eg (elided) ...

I'm just thinking aloud here. Having named instances could be useful in other ways (selective export).

Aargh! No never introduce named/scoped instances. It's a total can of worms. (People claim it was implicit in Kaes' or Wadler's original designs 1988; I think that's a mis-reading.)

There is a legitimate reason currently for wanting selective export: I've a 'private' instance that overlaps instances my clients want to write. Yes that's one of the (many) awkwardnesses with overlaps. Solve it the proper way with instance guards. So we have global coherence and global non-overlap (after taking guards into account).

Yes (long term plan) ...

I for one would find it helpful to have these impressively long list of points enumerated, with more info about each to show how the problem is solved. Killing many birds with one stone makes a proposal stronger.

OK I'm happy to do that. And I can quote the ticket numbers. Are you sure you want the proposal to be even longer?

AntC2 commented Aug 2, 2017

That's the danger point with overlaps

I wasn't clear enough. Today with overlapping instances I can declare ...

instance {-# OVERLAPPABLE #-} Show a => Show [a]

in a library module, and then override it in a client module, written separately, later, by a different author

data T = ...
instance {-# OVERLAPPING #-} Show T

With guards I have to anticipate all the other instances, writing (I suppose)

Um, those instances don't overlap. Did you mean instance Show [T]?

What you describe is how the mtl library used to work. Except it didn't work, so it was rewritten to not use overlaps like that. The problem with writing a 'catch-all' instance in the library module is it leads to all sorts of surprising incoherence/silently changing behaviour from imports.

instance Show [a] | a /~ T, a /~ S, a /~ whatever

Not only is that tiresome and anti-modular, it may not even be possible if the clients haven't been written when the library is designed. ...

I'm not sure you've picked a strong example: instance Show [a] where { ...; show xs = showList xs; ...}. Now I can write the instance Show T where {...; showList xs = ...} to do custom stuff in my client module, don't need to change the library. That could be the basis for a design pattern.

Anyway, overlapping instances do tend to be tiresome and anti-modular. Closed instances don't address this requirement either. So adding guards to the catch-all instance in the library has the same burden as adding instances within the closed set.

So I anticipate that there will be pressure to keep overlapping instances. Is that right or have I misunderstood?

Yes I am anticipating in the short term, people will want to continue to use overlapping instances. In the longer term they can piecemeal (class-by-class) change over, replacing the overlap pragmas with guards -- only for the instances that do actually overlap.

What I can't do with closed instances is put all instance Eq [] in module A and all the instance Eq (Maybe ) in module B

I think you can!

module A where

class EqList a where
  (==) :: [a] -> [a] -> Bool

instance EqList a => Eq [a]
  (==) = A.(==)

and similarly for module B. We simply delegate to a specialised class. Now we can put all the instances for EqList in one place. We came across this for type families, ...

Yeah OK. (And RIchard made a similar point.) Now that I've seen it coded out, I'm even more put off by how verbose and non-perspicuous it is.

where we wondered about "partly closed" families where you could have scattered sets of ordered equations something like

type instance F [a] where
  F [Int] = t1
  F [a]   = t1

type instance F (Maybe a) where
  F (Maybe Int) = t3
  F (Maybe a)   = t4

Yes I recognise that proposal. It came from me. I continue to be disappointed it never happened. (But I prefer apartness guards.)

but then we realised that instead we can just make specialised closed families FList, FMaybe and so on. Much simpler!

Maybe simpler for the compiler-writers. You haven't convinced me it's simpler for the instance-writers.

Now (with closed classes) the instance heads are spread out and the bodies/method overloads are mixed in with the instance logic

I agree that is horrible. But writing guards is also tricky; ...

Firstly, I think it's much easier to write the logic for an instance+guard stand-alone. More importantly the reader can understand it stand-alone. Secondly, the compiler can validate it is genuinely apart from any other instance. With a sequence of instances (especially if they're widely spread out with method overloads in-between), the logic is not so clear. And I think it's prone for the reader to mistake which patterns get selected by which instance decls. I'm saying this based on looking at some of the examples in the 'Instance Chains' paper. (Admittedly that has a lot of other fancy conditioning, like instance-level if and fail = backtrack.)

that's why we have closed type families and top-to-bottom matching for term-level functions.

With respect, I don't think you do exactly have top-to-bottom matching: In order to make progress with solving, CTF resolution tries to look for 'coincident overlap' by considering all of the equations, not necessarily in top-to-bottom sequence. From Richard's description, I think it's ended up working a lot more like apartness guards. My mental model is that all instances are 'competing' to be selected. Ordered equations is one way to prefer an instance out of several that might apply. Overlapping instances is another way (and not a very good one). The trouble with both those ways is the compiler has to entertain several instances that might apply. The advantage of apartness guards is the compiler knows the instance definitions are non-overlapping (after taking guards into account), so it can keep improving the types until at most one instance applies. Importantly, this doesn't involve search or backtracking.

If closed type families work well for the type-family case, ...

Yes they do work well from the equation-writer's point of view. Not so much under the hood. IMO it's confusing having two mechanisms: both stand-alone TF instances, associated type instances within stand-alone class instances and closed instances. I'd prefer to write more of my type instances as associated types; but currently that clashes horribly with overlaps.

I wonder if it'd be worth looking for a closed-instance syntax that was less horrible. eg (elided) ...

I'm just thinking aloud here. Having named instances could be useful in other ways (selective export).

Aargh! No never introduce named/scoped instances. It's a total can of worms. (People claim it was implicit in Kaes' or Wadler's original designs 1988; I think that's a mis-reading.)

There is a legitimate reason currently for wanting selective export: I've a 'private' instance that overlaps instances my clients want to write. Yes that's one of the (many) awkwardnesses with overlaps. Solve it the proper way with instance guards. So we have global coherence and global non-overlap (after taking guards into account).

Yes (long term plan) ...

I for one would find it helpful to have these impressively long list of points enumerated, with more info about each to show how the problem is solved. Killing many birds with one stone makes a proposal stronger.

OK I'm happy to do that. And I can quote the ticket numbers. Are you sure you want the proposal to be even longer?

@int-index

This comment has been minimized.

Show comment
Hide comment
@int-index

int-index Feb 27, 2018

Contributor

I was thinking of instances of the following form:

class T k

instance T k | k /~ Constraint
instance T Type

When Constraint and Type are not apart, the first instance won't be selected when looking for T Type (because Type /~ Constraint condition does not hold), and all is well. But after making them apart, the first instance is selected as well as the second one, and the program is rejected due to overlapping instances.

Contributor

int-index commented Feb 27, 2018

I was thinking of instances of the following form:

class T k

instance T k | k /~ Constraint
instance T Type

When Constraint and Type are not apart, the first instance won't be selected when looking for T Type (because Type /~ Constraint condition does not hold), and all is well. But after making them apart, the first instance is selected as well as the second one, and the program is rejected due to overlapping instances.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 27, 2018

I'm not proposing any change to how GHC decides whether two type (scheme)s are unifiable or apart. If there's bogusness now, that presumably affects ordinary instance selection:

instance T Constraint
instance T Type              -- so these two are reported as overlapping?

If #32 is going to fix the bogusness, I'll still follow however GHC decides: apartness guards will follow the #32 rules. Because instance selection must be consistent with the behaviour for classes and instances that don't use apartness guards.

EDIT: I don't need to express an opinion on how Constraint, Type behave: it's orthogonal to instance selection. They'll behave either like Int, Bool or like String, [Char]. (I see #32 just got submitted to the Committee, but I'm not clear how the decision landed.)

I'm simple-minded; I like nominative typing: I expect Type /~ Constraint to hold because they're spelled different. So I'm alarmed to read #32. To my eye, your two instances do overlap, I expect the program to be rejected. All is not well if those instances are accepted. Never the less I'm not going to make #32 a precondition for this proposal, because I'll blindly follow GHC rules for instance selection.

AntC2 commented Feb 27, 2018

I'm not proposing any change to how GHC decides whether two type (scheme)s are unifiable or apart. If there's bogusness now, that presumably affects ordinary instance selection:

instance T Constraint
instance T Type              -- so these two are reported as overlapping?

If #32 is going to fix the bogusness, I'll still follow however GHC decides: apartness guards will follow the #32 rules. Because instance selection must be consistent with the behaviour for classes and instances that don't use apartness guards.

EDIT: I don't need to express an opinion on how Constraint, Type behave: it's orthogonal to instance selection. They'll behave either like Int, Bool or like String, [Char]. (I see #32 just got submitted to the Committee, but I'm not clear how the decision landed.)

I'm simple-minded; I like nominative typing: I expect Type /~ Constraint to hold because they're spelled different. So I'm alarmed to read #32. To my eye, your two instances do overlap, I expect the program to be rejected. All is not well if those instances are accepted. Never the less I'm not going to make #32 a precondition for this proposal, because I'll blindly follow GHC rules for instance selection.

@int-index

This comment has been minimized.

Show comment
Hide comment
@int-index

int-index Feb 28, 2018

Contributor

I don't need to express an opinion on how Constraint, Type behave: it's orthogonal to instance selection. They'll behave either like Int, Bool or like String, [Char].

No, that's not correct. Int and Bool are apart, while String and [Char] are equal. Under #32, Type and Constraint will be neither apart nor equal, with intention to make them apart in the future.

Making them apart in the future is not a breaking change currently (at least that's what Richard says), but it will become a breaking change if we introduce apartness guards (as I demonstrated by the example above).

Contributor

int-index commented Feb 28, 2018

I don't need to express an opinion on how Constraint, Type behave: it's orthogonal to instance selection. They'll behave either like Int, Bool or like String, [Char].

No, that's not correct. Int and Bool are apart, while String and [Char] are equal. Under #32, Type and Constraint will be neither apart nor equal, with intention to make them apart in the future.

Making them apart in the future is not a breaking change currently (at least that's what Richard says), but it will become a breaking change if we introduce apartness guards (as I demonstrated by the example above).

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 28, 2018

Contributor

I agree with @int-index here. With the feature proposed here, making more types apart is a potentially breaking change. However, this is such a corner case that I'm not worried about it one way or another.

As to @AntC2's quandary: I agree that it's unclear how to proceed here. Simon's "mega-proposal" comments was, I believe, more about the length of the text, not the difficulty of the implementation. I don't think the implementation would be all that hard. (I wish I could say otherwise, but I agree with the "less than a handful of [busy] people could implement this" -- we need more type-checker grease-monkeys!)

I recommend submitting to the committee for a decision. If accepted, yes, this may wallow about for a while waiting for an implementor, but that's just the way of things. If you wish to submit, do be sure to mention @ nomeata, the committee secretary.

Contributor

goldfirere commented Feb 28, 2018

I agree with @int-index here. With the feature proposed here, making more types apart is a potentially breaking change. However, this is such a corner case that I'm not worried about it one way or another.

As to @AntC2's quandary: I agree that it's unclear how to proceed here. Simon's "mega-proposal" comments was, I believe, more about the length of the text, not the difficulty of the implementation. I don't think the implementation would be all that hard. (I wish I could say otherwise, but I agree with the "less than a handful of [busy] people could implement this" -- we need more type-checker grease-monkeys!)

I recommend submitting to the committee for a decision. If accepted, yes, this may wallow about for a while waiting for an implementor, but that's just the way of things. If you wish to submit, do be sure to mention @ nomeata, the committee secretary.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Mar 1, 2018

Contributor

Can the proposal please include a BNF for all the proposed changes to the source language syntax? E.g it looks as if the guards are always of form a ~/ ty where a is a type variable. Is that right?

I'm unclear about the precise rules for how to handle fundeps when we have instance guards. (And if you say that GHC does not have precise rules for how fundeps are handled anyway, your'd be right. But perhaps we can take the opportunity to fix that problem.)

Contributor

simonpj commented Mar 1, 2018

Can the proposal please include a BNF for all the proposed changes to the source language syntax? E.g it looks as if the guards are always of form a ~/ ty where a is a type variable. Is that right?

I'm unclear about the precise rules for how to handle fundeps when we have instance guards. (And if you say that GHC does not have precise rules for how fundeps are handled anyway, your'd be right. But perhaps we can take the opportunity to fix that problem.)

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Mar 1, 2018

Contributor

Simon's "mega-proposal" comments was...

Yes, you shouldn't take me too seriously on this. It is a brand-new bit of technology that has to attach to every instance decl. But that should not be too hard.

I dislike that it overlaps so much with the functionality of closed type families. But desugaring a closed type family into bunch of open family instances with suitable guards is (I think, not routine).

Earlier you wrote

Yes (long term plan): take out Closed Type Families (or translate them to apartness guards); take out IncoherentInstances; take out OverlappingInstances; take out UndecidableInstances. Possibly no need to implement "Dysfunctional Functional Dependencies". Resolve Iavor's concerns wrt GHC's dubious "Instances inconsistent with Functional Dependencies" check for non-full dependencies -- by making GHC behave like Jones' original spec for FunDeps/the FDs through CHRs paper. Resolve some of the long-standing tickets around the interaction of overlaps and FunDeps. Make 'Orphan Instances' less problematic, because they can't overlap or get overlapped. Oh, and I think we have a better basis for Injective Type Families (that is, where result with one arg determines the other arg).

I'd love to see this vision articulated explicitly in the proposal. It becomes much more attractive if it allows us to simplify the language by (say) deprecating or removing features. Making that explicit as a medium term goal might elicit responses from people who are relying on those features and think, for some reason, that apartness guards will not solve their problem.

I'm not arguing strongly against. But it's a relatively big feature in a part of the type checker that is already complicated.

Contributor

simonpj commented Mar 1, 2018

Simon's "mega-proposal" comments was...

Yes, you shouldn't take me too seriously on this. It is a brand-new bit of technology that has to attach to every instance decl. But that should not be too hard.

I dislike that it overlaps so much with the functionality of closed type families. But desugaring a closed type family into bunch of open family instances with suitable guards is (I think, not routine).

Earlier you wrote

Yes (long term plan): take out Closed Type Families (or translate them to apartness guards); take out IncoherentInstances; take out OverlappingInstances; take out UndecidableInstances. Possibly no need to implement "Dysfunctional Functional Dependencies". Resolve Iavor's concerns wrt GHC's dubious "Instances inconsistent with Functional Dependencies" check for non-full dependencies -- by making GHC behave like Jones' original spec for FunDeps/the FDs through CHRs paper. Resolve some of the long-standing tickets around the interaction of overlaps and FunDeps. Make 'Orphan Instances' less problematic, because they can't overlap or get overlapped. Oh, and I think we have a better basis for Injective Type Families (that is, where result with one arg determines the other arg).

I'd love to see this vision articulated explicitly in the proposal. It becomes much more attractive if it allows us to simplify the language by (say) deprecating or removing features. Making that explicit as a medium term goal might elicit responses from people who are relying on those features and think, for some reason, that apartness guards will not solve their problem.

I'm not arguing strongly against. But it's a relatively big feature in a part of the type checker that is already complicated.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 5, 2018

Simon's "mega-proposal" comments was...

Yes, you shouldn't take me too seriously on this.

I'm thinking that if @simonpj's reaction is there's a lot to read, other Committee members will just give up: so much text; then it must be complicated/too violent a change. Whereas ...

It is a brand-new bit of technology ...

What (I think) I'm doing is finding a way to express the logic that's already in effect for overlapping instances, and in effect for closed type families; and explains ghc's spurious 'instances inconsistent with fundeps' rejections. A new formalism, maybe; but not new technology.

I'm happy to articulate more motivations in the proposal. I think in fact most already is. But you've not seen it because there's just too much darned text.

I dislike that it overlaps so much with the functionality of closed type families.

I'm not expecting anyone will abandon closed type families, or overlaps, or UndecidableInstances in a hurry. Perhaps @goldfirere's plan is better to sneak the mechanism in under the covers -- for both type families and overlapping instances -- then expose the surface syntax.

AntC2 commented Mar 5, 2018

Simon's "mega-proposal" comments was...

Yes, you shouldn't take me too seriously on this.

I'm thinking that if @simonpj's reaction is there's a lot to read, other Committee members will just give up: so much text; then it must be complicated/too violent a change. Whereas ...

It is a brand-new bit of technology ...

What (I think) I'm doing is finding a way to express the logic that's already in effect for overlapping instances, and in effect for closed type families; and explains ghc's spurious 'instances inconsistent with fundeps' rejections. A new formalism, maybe; but not new technology.

I'm happy to articulate more motivations in the proposal. I think in fact most already is. But you've not seen it because there's just too much darned text.

I dislike that it overlaps so much with the functionality of closed type families.

I'm not expecting anyone will abandon closed type families, or overlaps, or UndecidableInstances in a hurry. Perhaps @goldfirere's plan is better to sneak the mechanism in under the covers -- for both type families and overlapping instances -- then expose the surface syntax.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 5, 2018

Can the proposal please include a BNF for all the proposed changes to the source language syntax? E.g it looks as if the guards are always of form a ~/ ty where a is a type variable. Is that right?

OK will do. Guards are often of the form a /~ ty, but in general the intuition is: anything that can appear with ~ in equality constraints. (Using type vars only from the head. Excluding type family applications.) I use _ for wildcards, but with entirely different meaning vs PartialTypeSignatures or extra-constraints wildcard.

Here's an example where the a /~ ty form is not expressive enough:

class C a b
instance C Int (Maybe b')
instance {-# OVERLAPPING #-} C a b

<===>

class {-# INSTANCEGUARDS #-} C2 a b
instance C2 Int (Maybe b')                       -- as above
instance C2 a b | (a, b) /~ (Int, Maybe _)      -- note the `_` wildcard

If there's some reason why a /~ ty would be easier to implement, that could be expressed (awkwardly) as:

class {-# INSTANCEGUARDS #-} C3 a b
instance C3 Int (Maybe b')                       -- as above
instance C3 Int b | b /~ (Maybe _)
instance C3 a (Maybe b') | a /~ Int
instance C3 a b | a /~ Int, b /~ (Maybe _) 

AntC2 commented Mar 5, 2018

Can the proposal please include a BNF for all the proposed changes to the source language syntax? E.g it looks as if the guards are always of form a ~/ ty where a is a type variable. Is that right?

OK will do. Guards are often of the form a /~ ty, but in general the intuition is: anything that can appear with ~ in equality constraints. (Using type vars only from the head. Excluding type family applications.) I use _ for wildcards, but with entirely different meaning vs PartialTypeSignatures or extra-constraints wildcard.

Here's an example where the a /~ ty form is not expressive enough:

class C a b
instance C Int (Maybe b')
instance {-# OVERLAPPING #-} C a b

<===>

class {-# INSTANCEGUARDS #-} C2 a b
instance C2 Int (Maybe b')                       -- as above
instance C2 a b | (a, b) /~ (Int, Maybe _)      -- note the `_` wildcard

If there's some reason why a /~ ty would be easier to implement, that could be expressed (awkwardly) as:

class {-# INSTANCEGUARDS #-} C3 a b
instance C3 Int (Maybe b')                       -- as above
instance C3 Int b | b /~ (Maybe _)
instance C3 a (Maybe b') | a /~ Int
instance C3 a b | a /~ Int, b /~ (Maybe _) 
@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 5, 2018

I'm unclear about the precise rules for how to handle fundeps when we have instance guards.

No change to how fundeps generate the 'result' types, once an instance is selected. (Yes I know that's not an answer.) There is a change to validation for Instances inconsistent with Functional Dependencies, meaning fewer sets of instances will get rejected: see example then how validation is improved at "These instances are consistent with FunDeps ...".

(And if you say that GHC does not have precise rules for how fundeps are handled anyway, your'd be right. But perhaps we can take the opportunity to fix that problem.)

Ah, so now you want a conference paper. Where can I find a sponsor? ;-)

Turns out the rule (or at least a possible rule) has been hiding in plain sight since 2000:

class C a b | a -> b

<===>

class ( forall b'. C a b' => b' ~ b ) => C a b

This more or less follows Mark P Jones' original paper; and coincides with the Relational Database predicate logic characterisation for Functional Dependencies. So all we need to tackle is how to get GHC to validate a set of instances with this cycle in superclass constraints; and quite possibly cycles in the instance constraints.

I think GHC does have precise rules. Partly documented in the 'FDs via CHRs' paper, supplemented with comments in the code that you've been diligent enough to copy on to various Trac tickets -- for example the 'bogus consistency check'.

Which bits do you think are not precise enough? I must admit that once you switch on UndecidableInstances (and the instance breaks the coverage conditions) there does seem to be 'magic happens'.

AntC2 commented Mar 5, 2018

I'm unclear about the precise rules for how to handle fundeps when we have instance guards.

No change to how fundeps generate the 'result' types, once an instance is selected. (Yes I know that's not an answer.) There is a change to validation for Instances inconsistent with Functional Dependencies, meaning fewer sets of instances will get rejected: see example then how validation is improved at "These instances are consistent with FunDeps ...".

(And if you say that GHC does not have precise rules for how fundeps are handled anyway, your'd be right. But perhaps we can take the opportunity to fix that problem.)

Ah, so now you want a conference paper. Where can I find a sponsor? ;-)

Turns out the rule (or at least a possible rule) has been hiding in plain sight since 2000:

class C a b | a -> b

<===>

class ( forall b'. C a b' => b' ~ b ) => C a b

This more or less follows Mark P Jones' original paper; and coincides with the Relational Database predicate logic characterisation for Functional Dependencies. So all we need to tackle is how to get GHC to validate a set of instances with this cycle in superclass constraints; and quite possibly cycles in the instance constraints.

I think GHC does have precise rules. Partly documented in the 'FDs via CHRs' paper, supplemented with comments in the code that you've been diligent enough to copy on to various Trac tickets -- for example the 'bogus consistency check'.

Which bits do you think are not precise enough? I must admit that once you switch on UndecidableInstances (and the instance breaks the coverage conditions) there does seem to be 'magic happens'.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Mar 5, 2018

Contributor

If there's some reason why a /~ ty would be easier to implement, that could be expressed (awkwardly) as:

Good example! Add it, pointing out that this avoids an at-least-linear growth in the number of equations.

Contributor

simonpj commented Mar 5, 2018

If there's some reason why a /~ ty would be easier to implement, that could be expressed (awkwardly) as:

Good example! Add it, pointing out that this avoids an at-least-linear growth in the number of equations.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Mar 5, 2018

Contributor

Which bits do you think are not precise enough?

Fair question. Let me try to be more specific.

With fundeps, if we have

class C a b | a -> b
instance blah => C t1 t2

then when we have a constraint C s1 s2 and s1 is a substitution instance of t1, then we generate a extra equality s2 ~ S(t2), where S is the instantiating substitution.

How does that rule change when we add instance guards?

We coverage and consistency rules for fundeps. How do they change?

Better than specifying changes (as diffs from a baseline that may vary between readers) would be specifying the new rules.

Contributor

simonpj commented Mar 5, 2018

Which bits do you think are not precise enough?

Fair question. Let me try to be more specific.

With fundeps, if we have

class C a b | a -> b
instance blah => C t1 t2

then when we have a constraint C s1 s2 and s1 is a substitution instance of t1, then we generate a extra equality s2 ~ S(t2), where S is the instantiating substitution.

How does that rule change when we add instance guards?

We coverage and consistency rules for fundeps. How do they change?

Better than specifying changes (as diffs from a baseline that may vary between readers) would be specifying the new rules.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 5, 2018

Good example! Add it, ...

already there see "deMorgan".

AntC2 commented Mar 5, 2018

Good example! Add it, ...

already there see "deMorgan".

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 5, 2018

How does that rule [for generating fundep result] change when we add instance guards?

No change. As I said.

We coverage [rules for fundeps] ...

No change. But because the consistency rule is different [below], it is less likely you'll need to write a 'catch-all' overlapping instance which needs UndecidableInstances. See the example I linked to in earlier comment.

... and consistency rules for fundeps. How do they change?

Given

class C2 a b | a -> b
instance blah1 => C2 t1 t2
instance blah2 => C2 t3 t4 | t3 /~ t5           -- t3 overlaps t1

The check for consistency (pairwise between instances):

  • Generate S2, the instantiating substitution that unifies t1, t3.
  • Apply S2 to t2, t4. Does that result in the same type? Then the instances are confluent OK. (same rule as currently EDIT: Actually stricter than currently, which only checks the resulting types are unifiable -- this is the 'bogus consistency check' noted in Trac #10675.)
  • Else apply S2 to the guard, both sides of t3 /~ t5. Does that yield a contradiction? Then it doesn't matter that the instance heads are non-confluent: no wanted constraint C s1 s2 can have s1 as a substitution instance of both t1 and t3 and t3 /~ t5.
  • (If t3 were apart from t1 then the instances are consistent under the fundep, as currently.)

Again, see the bigger example I linked to in earlier comment.

It's the "apply S2 to the guard" that GHC can't do with overlapping instances. Because there's no way to express: in case of overlap, select this instance rather than that one; and therefore apply this instance's instantiating substitution for the fundep.

AntC2 commented Mar 5, 2018

How does that rule [for generating fundep result] change when we add instance guards?

No change. As I said.

We coverage [rules for fundeps] ...

No change. But because the consistency rule is different [below], it is less likely you'll need to write a 'catch-all' overlapping instance which needs UndecidableInstances. See the example I linked to in earlier comment.

... and consistency rules for fundeps. How do they change?

Given

class C2 a b | a -> b
instance blah1 => C2 t1 t2
instance blah2 => C2 t3 t4 | t3 /~ t5           -- t3 overlaps t1

The check for consistency (pairwise between instances):

  • Generate S2, the instantiating substitution that unifies t1, t3.
  • Apply S2 to t2, t4. Does that result in the same type? Then the instances are confluent OK. (same rule as currently EDIT: Actually stricter than currently, which only checks the resulting types are unifiable -- this is the 'bogus consistency check' noted in Trac #10675.)
  • Else apply S2 to the guard, both sides of t3 /~ t5. Does that yield a contradiction? Then it doesn't matter that the instance heads are non-confluent: no wanted constraint C s1 s2 can have s1 as a substitution instance of both t1 and t3 and t3 /~ t5.
  • (If t3 were apart from t1 then the instances are consistent under the fundep, as currently.)

Again, see the bigger example I linked to in earlier comment.

It's the "apply S2 to the guard" that GHC can't do with overlapping instances. Because there's no way to express: in case of overlap, select this instance rather than that one; and therefore apply this instance's instantiating substitution for the fundep.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Mar 5, 2018

Contributor

No change. As I said.

Ok good. Can you just write the new rules in the "Proposed specification" section? Then my questions are answered explicitly by the proposal rather then in the comment stream.

(Adding section numbers would be super helpful; a one-line change.)

Contributor

simonpj commented Mar 5, 2018

No change. As I said.

Ok good. Can you just write the new rules in the "Proposed specification" section? Then my questions are answered explicitly by the proposal rather then in the comment stream.

(Adding section numbers would be super helpful; a one-line change.)

AntC2 added some commits Mar 6, 2018

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Mar 17, 2018

ref @MarLinn's comment way back when, and @mniip's reply: even when a disequality constraint (not guard) would be enough to block an instance, you can't always write one. Consider this (pathological) case from the User Guide on UndecidableInstances

class D a
class F a b | a->b
instance F [a] [[a]]
instance (D c, F a c) => D [a]   -- 'c' is not mentioned in the head

Even though the instance for D [a] needs UndecidableInstances, there are sensible use cases with the same structure. (One's given for Show just before it.) I would say it's the instance for F [a] [[a]] that is dodgy, even though it doesn't need UndecidableInstances: its FunDep has the effect of inflating the argument; so this program causes the typechecker to loop.

Let's say class F and its instances are locked away in a library we can't change; we're writing class D and we want to at least innoculate D's instances from typechecker loopiness.

Assuming type operator (/~) :: k -> l -> Constraint defined as mniip gives back at that link, let's try to constrain the instance for D to block if its parameter is a list of lists -- that is, if [a] ~ [[a']] for some a'.

instance (a /~ [_], D c, F a c) => D [a]

But you can't put a wildcard _, because they're not allowed in contexts like that. Can we put a /~ [a']? But a' is not mentioned in the head, and unlike for c we can't write any other constraint to determine it. For the very good reason that if you want a not to be a list of anything, then there's nothing you can tell it not to be a list of.

You can get away (maybe) by switching on AllowAmbiguousTypes. But you're liable to just shift the error can't infer the type for a' to some use site for D [a]. You can write a more-specific instance to catch it

instance (TypeError (Text "F constraint would give typechecker loop")) => D [[a]]

I find an apartness guard more to the point

instance (D c, F a c) => D [a] | a /~ [_]

AntC2 commented Mar 17, 2018

ref @MarLinn's comment way back when, and @mniip's reply: even when a disequality constraint (not guard) would be enough to block an instance, you can't always write one. Consider this (pathological) case from the User Guide on UndecidableInstances

class D a
class F a b | a->b
instance F [a] [[a]]
instance (D c, F a c) => D [a]   -- 'c' is not mentioned in the head

Even though the instance for D [a] needs UndecidableInstances, there are sensible use cases with the same structure. (One's given for Show just before it.) I would say it's the instance for F [a] [[a]] that is dodgy, even though it doesn't need UndecidableInstances: its FunDep has the effect of inflating the argument; so this program causes the typechecker to loop.

Let's say class F and its instances are locked away in a library we can't change; we're writing class D and we want to at least innoculate D's instances from typechecker loopiness.

Assuming type operator (/~) :: k -> l -> Constraint defined as mniip gives back at that link, let's try to constrain the instance for D to block if its parameter is a list of lists -- that is, if [a] ~ [[a']] for some a'.

instance (a /~ [_], D c, F a c) => D [a]

But you can't put a wildcard _, because they're not allowed in contexts like that. Can we put a /~ [a']? But a' is not mentioned in the head, and unlike for c we can't write any other constraint to determine it. For the very good reason that if you want a not to be a list of anything, then there's nothing you can tell it not to be a list of.

You can get away (maybe) by switching on AllowAmbiguousTypes. But you're liable to just shift the error can't infer the type for a' to some use site for D [a]. You can write a more-specific instance to catch it

instance (TypeError (Text "F constraint would give typechecker loop")) => D [[a]]

I find an apartness guard more to the point

instance (D c, F a c) => D [a] | a /~ [_]
@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Apr 28, 2018

Contributor

@AntC2, I am scheduled to ping on the status of this?

I feel like this is this kind of language innovation that would be well suited for an academically reviewed paper that comes with an example implementation that thoroughly explores the design, and can afterwards go through the GHC proposal process. But the effort that takes is probably too much for anyone who does not write papers for a living…

But if you think your proposal is done and in a good shape, you can certainly submit it to the committee!

Contributor

nomeata commented Apr 28, 2018

@AntC2, I am scheduled to ping on the status of this?

I feel like this is this kind of language innovation that would be well suited for an academically reviewed paper that comes with an example implementation that thoroughly explores the design, and can afterwards go through the GHC proposal process. But the effort that takes is probably too much for anyone who does not write papers for a living…

But if you think your proposal is done and in a good shape, you can certainly submit it to the committee!

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Apr 29, 2018

the status of this?

Thanks @nomeata, not ready yet to submit: there's a couple of requests outstanding from @simonpj. The committee seems to have plenty on its plate, so I'm not feeling any sense of urgency.

... academically reviewed paper that comes with an example implementation ...

Yes, or a project by someone under (say) @goldfirere's direction that uses the idea to implement Closed Type Families and/or Overlapping Instances within a module; we expose the surface syntax later.

I'm happy to help anybody/anything that will get a bit of traction.

AntC2 commented Apr 29, 2018

the status of this?

Thanks @nomeata, not ready yet to submit: there's a couple of requests outstanding from @simonpj. The committee seems to have plenty on its plate, so I'm not feeling any sense of urgency.

... academically reviewed paper that comes with an example implementation ...

Yes, or a project by someone under (say) @goldfirere's direction that uses the idea to implement Closed Type Families and/or Overlapping Instances within a module; we expose the surface syntax later.

I'm happy to help anybody/anything that will get a bit of traction.

AntC2 added some commits May 28, 2018

summary of syntax changes and their semantics
In progress don't look yet.
As requested by spj.
Trying to format as a table for quick reference, but ReST's formatting is just terrible. (And it's taking ages.)
Syntax/semantics summary continued (in progress)
Simplify the table, formatting still dodgy.
Summary of syntax, semantics, restrictions: done.
Quick-reference table at start of Secion 2 'Proposed Change Specification'.
@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 May 28, 2018

Replying to @simonpj

Can you just write the new rules in the "Proposed specification" section?

Quick-reference table for the syntax here. The formatting is the best that ReST seems capable of -- unless anyone knows how to stop it throwing random italics and bold.

And section-numbered, as requested.

AntC2 commented May 28, 2018

Replying to @simonpj

Can you just write the new rules in the "Proposed specification" section?

Quick-reference table for the syntax here. The formatting is the best that ReST seems capable of -- unless anyone knows how to stop it throwing random italics and bold.

And section-numbered, as requested.

Summarise the longer-term plan, from the discussion
That is, bring together the logic that underpins instance selection and type improvement.
@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 May 28, 2018

Replying to @simonpj

vision articulated explicitly in the proposal

I had written up that vision point-by-point above. Now summarised in a new section.

AntC2 commented May 28, 2018

Replying to @simonpj

vision articulated explicitly in the proposal

I had written up that vision point-by-point above. Now summarised in a new section.

AntC2 added some commits May 29, 2018

formatting, typos, tweaks
hurray! sussed the formatting.
summarise rules for instance validation
Must not overlap after taking guards into account.
@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jun 4, 2018

This comment is bugging me:

desugaring a closed type family into bunch of open family instances with suitable guards is (I think, not routine).

I feel an algorithm is possible (and would also be useful for making further progress with Injective TFs and to turn 'Closed Type Classes' (possible future) into open class instances). Here's a stab. I'll use the language and notation of the Closed Type Families paper.

The basic idea

  • The first equation in a CTF sequence goes across as stands.
  • Later equations must exclude (using guards) any overlap with prior equations.
  • Except that if the prior equation's LHS is apart, that's excluded automatically (no need for guards); or
  • if the LHSs are unifiable "and their RHSs are the same under the substitution induced by the unification.", the guard would be pointless.
  • The CTF paper calls this apart-or-same-under-substitution condition compatible.

Supposing a guard is needed, how to generate it?

  • Wrap the two LHS type patterns into tuples.
  • Unify them leaving the current equation's tyvars as is, and substituting those tyvars into the prior equation's LHS.
  • Where there's no tyvar from current equation's LHS corresponding to a position in the prior's, use wildcard _.
  • 'cancel down' any common elements.
  • Generate the guard as LHS-canceled-down /~ RHS-canceled-down.

Some examples:

From section 3.5 Optimized matching of the paper

type family F a where
  F Int  = Char                         -- (1)
  F Bool = Bool                         -- (2)
  F x    = Int                          -- (3)

type family {-# INSTANCEGUARDS #-} F a
type instance F Int  = Char             -- first equation take as is
type instance F Bool = Bool             -- LHS is apart from (1), so take as is
type instance F x    | x /~ Int, x /~ Bool         -- exclude (1), exclude (2)
                     = Int

From the wiki

type family F2 a where
  F2 Int  = Bool
  F2 Bool = Char
  F2 a    = Bool

type family {-# INSTANCEGUARDS #-} F2 a
type instance F2 Int  = Bool             -- first equation take as is
type instance F2 Bool = Char             -- LHS is apart from first, so take as is
type instance F2 a    | a /~ Bool        -- RHS same as first, so guard only against second
                      = Bool

from the paper section 2 (adapted)

type family F3 a b where
  F3 Int  b    = Bool
  F3 a    Bool = Char

For the second equation, wrapping the instance heads as tuples and unifying gives (a, Bool) /~ (Int, Bool). That can be 'canceled down'.

type family {-# INSTANCEGUARDS #-} F3 a b
type instance F3 Int  b    = Bool
type instance F3 a    Bool | a /~ Int     -- 'cancel down' common elements
                           = Char

Two further wrinkles for the algorithm (to be demo'd in the final example below)

  • If there's a prior equation whose LHS is strictly more general than one higher still, no need to generate a guard for the less general case. The more general 'shadows' the less. Providing the more general was not passed over because its RHS is the same under unifying substitution. (In that case, still pass over the more general, to generate a guard agains the less general.)
  • If there's a prior equation using repeated tyvars on LHS, and it's not shadowed by a later equation using distinct tyvars in those same positions, need to generate an equation with distinct tyvars.
    (If a tyvar appears more than twice; or two distinct tyvars each appear repeated, need to generate equations for all the perms/combs of distinctness. I can expand this comment if needs be.)

Those two points suggest the algorithm should precompute by running down the equations looking for those conditions before generating guards.

Final example is the gnarly one from the proposal. Using the algorithm generates guards that are symmetric, rather pleasingly:

data T a
type family Equiv x y :: Bool where
  Equiv a      a     = True                -- 1
  Equiv (T b)  (T c) = True                -- 2
  Equiv (t d)  (t e) = Equiv d e           -- 3  -- note repeated tyvars, shadows 2
  Equiv f      g     = False               -- 4

type family {-# INSTANCEGUARDS #-} Equiv x y :: Bool
type instance a     a      = True
type instance (T b) (T c)  = True          -- RHS same as 1, so no guard
type instance (t d) (t e)  | d /~ e        -- cancel down from ((t d), (t e)) /~ ((t d),(t d)) unifying with 1
                           , t /~ T        -- cancel down from((t d), (t e)) /~ ((T d), (T e)) unifying with 2
                           = Equiv d e
type instance (t d) (t' e) | (t' e) /~ (t d) -- generated instance 4a from 3 with distinct tyvars
                           , t' /~ t       -- annoying that this guard subsumes the line above
                           = False         -- same result as 4
type instance f     g      | f /~ g        -- instance 4b from 4
                           , (f, g) /~ ((_ _), (_ _))  -- obtained from unifying with 3; not 4a because passed over
                           = False

The guards for 4a are obtained from cancelling down:

  • unifying 4a with 1 gives guard ((t d), (t' e)) /~ ((t d), (t d)).
  • unifying with 3 gives guard ((t d), (t' e)) /~ ((t d), (t e)).

AntC2 commented Jun 4, 2018

This comment is bugging me:

desugaring a closed type family into bunch of open family instances with suitable guards is (I think, not routine).

I feel an algorithm is possible (and would also be useful for making further progress with Injective TFs and to turn 'Closed Type Classes' (possible future) into open class instances). Here's a stab. I'll use the language and notation of the Closed Type Families paper.

The basic idea

  • The first equation in a CTF sequence goes across as stands.
  • Later equations must exclude (using guards) any overlap with prior equations.
  • Except that if the prior equation's LHS is apart, that's excluded automatically (no need for guards); or
  • if the LHSs are unifiable "and their RHSs are the same under the substitution induced by the unification.", the guard would be pointless.
  • The CTF paper calls this apart-or-same-under-substitution condition compatible.

Supposing a guard is needed, how to generate it?

  • Wrap the two LHS type patterns into tuples.
  • Unify them leaving the current equation's tyvars as is, and substituting those tyvars into the prior equation's LHS.
  • Where there's no tyvar from current equation's LHS corresponding to a position in the prior's, use wildcard _.
  • 'cancel down' any common elements.
  • Generate the guard as LHS-canceled-down /~ RHS-canceled-down.

Some examples:

From section 3.5 Optimized matching of the paper

type family F a where
  F Int  = Char                         -- (1)
  F Bool = Bool                         -- (2)
  F x    = Int                          -- (3)

type family {-# INSTANCEGUARDS #-} F a
type instance F Int  = Char             -- first equation take as is
type instance F Bool = Bool             -- LHS is apart from (1), so take as is
type instance F x    | x /~ Int, x /~ Bool         -- exclude (1), exclude (2)
                     = Int

From the wiki

type family F2 a where
  F2 Int  = Bool
  F2 Bool = Char
  F2 a    = Bool

type family {-# INSTANCEGUARDS #-} F2 a
type instance F2 Int  = Bool             -- first equation take as is
type instance F2 Bool = Char             -- LHS is apart from first, so take as is
type instance F2 a    | a /~ Bool        -- RHS same as first, so guard only against second
                      = Bool

from the paper section 2 (adapted)

type family F3 a b where
  F3 Int  b    = Bool
  F3 a    Bool = Char

For the second equation, wrapping the instance heads as tuples and unifying gives (a, Bool) /~ (Int, Bool). That can be 'canceled down'.

type family {-# INSTANCEGUARDS #-} F3 a b
type instance F3 Int  b    = Bool
type instance F3 a    Bool | a /~ Int     -- 'cancel down' common elements
                           = Char

Two further wrinkles for the algorithm (to be demo'd in the final example below)

  • If there's a prior equation whose LHS is strictly more general than one higher still, no need to generate a guard for the less general case. The more general 'shadows' the less. Providing the more general was not passed over because its RHS is the same under unifying substitution. (In that case, still pass over the more general, to generate a guard agains the less general.)
  • If there's a prior equation using repeated tyvars on LHS, and it's not shadowed by a later equation using distinct tyvars in those same positions, need to generate an equation with distinct tyvars.
    (If a tyvar appears more than twice; or two distinct tyvars each appear repeated, need to generate equations for all the perms/combs of distinctness. I can expand this comment if needs be.)

Those two points suggest the algorithm should precompute by running down the equations looking for those conditions before generating guards.

Final example is the gnarly one from the proposal. Using the algorithm generates guards that are symmetric, rather pleasingly:

data T a
type family Equiv x y :: Bool where
  Equiv a      a     = True                -- 1
  Equiv (T b)  (T c) = True                -- 2
  Equiv (t d)  (t e) = Equiv d e           -- 3  -- note repeated tyvars, shadows 2
  Equiv f      g     = False               -- 4

type family {-# INSTANCEGUARDS #-} Equiv x y :: Bool
type instance a     a      = True
type instance (T b) (T c)  = True          -- RHS same as 1, so no guard
type instance (t d) (t e)  | d /~ e        -- cancel down from ((t d), (t e)) /~ ((t d),(t d)) unifying with 1
                           , t /~ T        -- cancel down from((t d), (t e)) /~ ((T d), (T e)) unifying with 2
                           = Equiv d e
type instance (t d) (t' e) | (t' e) /~ (t d) -- generated instance 4a from 3 with distinct tyvars
                           , t' /~ t       -- annoying that this guard subsumes the line above
                           = False         -- same result as 4
type instance f     g      | f /~ g        -- instance 4b from 4
                           , (f, g) /~ ((_ _), (_ _))  -- obtained from unifying with 3; not 4a because passed over
                           = False

The guards for 4a are obtained from cancelling down:

  • unifying 4a with 1 gives guard ((t d), (t' e)) /~ ((t d), (t d)).
  • unifying with 3 gives guard ((t d), (t' e)) /~ ((t d), (t e)).
@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Jul 31, 2018

Withdrawn; and withdrawing.

This proposal has sat around over a year. There's been some polite comment but no uptake. Addressing Functional Dependencies and instance overlaps and their interplay just doesn't fit with the direction of travel for GHC. Indeed the difficulties and disfluencies in GHC's behaviour wrt those extensions -- that were apparent from over a dozen years ago -- have received no love.

Then I might as well start afresh from that time, with a better-disciplined Haskell. And I'm finding it surprisingly easy to engineer.

@nomeata I presume that closing this doesn't lose it entirely from the proposals process(?) I'm happy for and would support somebody to take up the ideas later.

If I'm frank with myself: GHC-Haskell is no longer the language through which I became enthusastic about Functional Programming. Still the records system is an embarrassment. (How many attempts have there been to make progress?) Meanwhile GHC has become bloated with abstruse features. Most of those features are of small benefit to me. Each seems to have come with significant downsides in added complexity and impenetrable error messages -- even when I didn't think I was using that extension. QuantifiedConstraints, which I had high expectations for, has turned out a damp squib. The pointy-heads have taken over the asylum.

Now that I've discovered it's not so difficult to hack (some) compiler, I'm going back to a simpler Haskell vintage ~2006.

AntC2 commented Jul 31, 2018

Withdrawn; and withdrawing.

This proposal has sat around over a year. There's been some polite comment but no uptake. Addressing Functional Dependencies and instance overlaps and their interplay just doesn't fit with the direction of travel for GHC. Indeed the difficulties and disfluencies in GHC's behaviour wrt those extensions -- that were apparent from over a dozen years ago -- have received no love.

Then I might as well start afresh from that time, with a better-disciplined Haskell. And I'm finding it surprisingly easy to engineer.

@nomeata I presume that closing this doesn't lose it entirely from the proposals process(?) I'm happy for and would support somebody to take up the ideas later.

If I'm frank with myself: GHC-Haskell is no longer the language through which I became enthusastic about Functional Programming. Still the records system is an embarrassment. (How many attempts have there been to make progress?) Meanwhile GHC has become bloated with abstruse features. Most of those features are of small benefit to me. Each seems to have come with significant downsides in added complexity and impenetrable error messages -- even when I didn't think I was using that extension. QuantifiedConstraints, which I had high expectations for, has turned out a damp squib. The pointy-heads have taken over the asylum.

Now that I've discovered it's not so difficult to hack (some) compiler, I'm going back to a simpler Haskell vintage ~2006.

@AntC2 AntC2 closed this Jul 31, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment