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

Quantified constraints #109

Merged
merged 17 commits into from Apr 24, 2018

Conversation

Projects
None yet
9 participants
@Gertjan423
Contributor

Gertjan423 commented Feb 1, 2018

Rendered

@Ericson2314

This comment has been minimized.

Show comment
Hide comment
@Ericson2314

Ericson2314 Feb 1, 2018

Would RankNConstraints be a more consistent extension name?

Ericson2314 commented Feb 1, 2018

Would RankNConstraints be a more consistent extension name?

@RyanGlScott

This comment has been minimized.

Show comment
Hide comment
@RyanGlScott

RyanGlScott Feb 2, 2018

Contributor

Adapting a question from https://phabricator.haskell.org/D4353#121358:

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not. For instance, this program:

{-# LANGUAGE QuantifiedConstraints  #-}
module T2893 where

f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
{-# NOINLINE f #-}
f x = x==x

g x = f [x]

data Rose f x = Rose x (f (Rose f x))

instance (Eq a, forall b. Eq b => Eq (f b))
      => Eq (Rose f a)  where
  (Rose x1 rs1) == (Rose x2 rs2)
    = x1==x2 && rs1 == rs2

Works without UndecidableInstances, but the following program does require UndecidableInstances:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where

data Some f where
  Some :: f a -> Some f

deriving instance (forall a. Show (f a)) => Show (Some f)
Bug.hs:9:19: error:
    • The constraint ‘forall a. Show (f a)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the stand-alone deriving instance for
        ‘(forall a. Show (f a)) => Show (Some f)’
  |
9 | deriving instance (forall a. Show (f a)) => Show (Some f)
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It's hard for me to tell why the former doesn't require it, but the latter does. If there is some rhyme or reason behind it, perhaps we should spell it out in the proposal somewhere.

Contributor

RyanGlScott commented Feb 2, 2018

Adapting a question from https://phabricator.haskell.org/D4353#121358:

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not. For instance, this program:

{-# LANGUAGE QuantifiedConstraints  #-}
module T2893 where

f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
{-# NOINLINE f #-}
f x = x==x

g x = f [x]

data Rose f x = Rose x (f (Rose f x))

instance (Eq a, forall b. Eq b => Eq (f b))
      => Eq (Rose f a)  where
  (Rose x1 rs1) == (Rose x2 rs2)
    = x1==x2 && rs1 == rs2

Works without UndecidableInstances, but the following program does require UndecidableInstances:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where

data Some f where
  Some :: f a -> Some f

deriving instance (forall a. Show (f a)) => Show (Some f)
Bug.hs:9:19: error:
    • The constraint ‘forall a. Show (f a)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the stand-alone deriving instance for
        ‘(forall a. Show (f a)) => Show (Some f)’
  |
9 | deriving instance (forall a. Show (f a)) => Show (Some f)
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It's hard for me to tell why the former doesn't require it, but the latter does. If there is some rhyme or reason behind it, perhaps we should spell it out in the proposal somewhere.

@treeowl

This comment has been minimized.

Show comment
Hide comment
@treeowl

treeowl Feb 2, 2018

Contributor

As I understand it, there can be some implementation issues with implication constraints. If we're given C => Dand we need D, we don't know whether to try to resolve D directly or whether to try to resolve C to use the given implication. Has this been resolved satisfactorily?

Another question: would it make sense to split this proposal? Quantified constraints and implication constraints seem like separate features, although they certainly go well together.

Contributor

treeowl commented Feb 2, 2018

As I understand it, there can be some implementation issues with implication constraints. If we're given C => Dand we need D, we don't know whether to try to resolve D directly or whether to try to resolve C to use the given implication. Has this been resolved satisfactorily?

Another question: would it make sense to split this proposal? Quantified constraints and implication constraints seem like separate features, although they certainly go well together.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 2, 2018

Contributor

As I understand it, there can be some implementation issues with implication constraints. If we're given C => Dand we need D, we don't know whether to try to resolve D directly or whether to try to resolve C to use the given implication. Has this been resolved satisfactorily?

I'm afraid I could not understand this sentence. Could you give a concrete example? I don't think there is a problem there. BTW have you read the paper? It's lays out many details.

Contributor

simonpj commented Feb 2, 2018

As I understand it, there can be some implementation issues with implication constraints. If we're given C => Dand we need D, we don't know whether to try to resolve D directly or whether to try to resolve C to use the given implication. Has this been resolved satisfactorily?

I'm afraid I could not understand this sentence. Could you give a concrete example? I don't think there is a problem there. BTW have you read the paper? It's lays out many details.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 2, 2018

Contributor

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not

You are absolutely right. This should form part of the proposal.

The question is this: what restrictions on the context of an instance decl ensure that constraint solving is guaranteed to terminate? The rules that GHC uses are laid out in the user manual. We need new rules for quantified constraints.

I think the rules might be

  • The quantified constraint must (taken independently) obey the termination rules for an instance decl).

  • The head of the quantified constraint (ie the bit after the =>) must obey the Paterson conditions.

I'm not certain. But I am certain we should specify it.

(The current implementation is not a good guide.)

Contributor

simonpj commented Feb 2, 2018

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not

You are absolutely right. This should form part of the proposal.

The question is this: what restrictions on the context of an instance decl ensure that constraint solving is guaranteed to terminate? The rules that GHC uses are laid out in the user manual. We need new rules for quantified constraints.

I think the rules might be

  • The quantified constraint must (taken independently) obey the termination rules for an instance decl).

  • The head of the quantified constraint (ie the bit after the =>) must obey the Paterson conditions.

I'm not certain. But I am certain we should specify it.

(The current implementation is not a good guide.)

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Feb 2, 2018

Contributor

I would welcome a discussion of type class coherence: Are there ways of breaking it with quantified constraints? If not, why?

Contributor

nomeata commented Feb 2, 2018

I would welcome a discussion of type class coherence: Are there ways of breaking it with quantified constraints? If not, why?

@Ericson2314

This comment has been minimized.

Show comment
Hide comment
@Ericson2314

Ericson2314 Feb 2, 2018

Another question: would it make sense to split this proposal? Quantified constraints and implication constraints seem like separate features, although they certainly go well together.

Per the revised proposal, It looks like this is just implication constraints, and this + whatever adding explicit foralls is qualified constraints. Not to force silly bike-shedding, but this steers me more towards wanting to call it RankNConstraints, as it is exactly higher-ranked used of =>.

Ericson2314 commented Feb 2, 2018

Another question: would it make sense to split this proposal? Quantified constraints and implication constraints seem like separate features, although they certainly go well together.

Per the revised proposal, It looks like this is just implication constraints, and this + whatever adding explicit foralls is qualified constraints. Not to force silly bike-shedding, but this steers me more towards wanting to call it RankNConstraints, as it is exactly higher-ranked used of =>.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 3, 2018

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not

You are absolutely right. This should form part of the proposal.

Then (at risk of overburdening QuantifiedConstraints) is this the time to introduce per-instance UndecidableInstances?

Afterthought: QuantifiedConstraints are also to be available superclass (Monad Trans example in section 2.1 of the hs2017 paper). Do we have to worry about Undecidable superclass constraints? Or is the existing non-cyclicity test adequate?

AntC2 commented Feb 3, 2018

I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not

You are absolutely right. This should form part of the proposal.

Then (at risk of overburdening QuantifiedConstraints) is this the time to introduce per-instance UndecidableInstances?

Afterthought: QuantifiedConstraints are also to be available superclass (Monad Trans example in section 2.1 of the hs2017 paper). Do we have to worry about Undecidable superclass constraints? Or is the existing non-cyclicity test adequate?

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 4, 2018

Contributor

A few reactions to this proposal (which I'm reading for the first time today):

  • Quantified constraints also allow forall quantification. This should be explicit in the proposal. The current syntactic extension just mentions a context to the left of a class, but not fresh variables. Note that this is different than the forall allowed in an instance declaration, which just makes something explicit which was previously implicit. The forall in a quantified constraint is wholly new.

  • While summarizing the typing rules in the proposal may be hard to do, I agree with the TODO that it should explicitly address backtracking. In particular, what happens when quantified constraints lead to more than one way to solve a constraint? I believe that Simon has proposed (offline) to reject such situations as ambiguous, but this needs to be in the proposal (with an example).

  • As mentioned on GHC's #9123, the second issue could be solved by proactively expanding superclasses even in quantified constraints. I don't think this would be troublesome. If this expansion leads to an ambiguity that might lead to backtracking, then reject. Is that rejection becomes bothersome in real life, then we'll think more creatively with a concrete example.

I'm in strong support of this proposal, and favor QuantifiedConstraints over RankNConstraints. I find the former less jargony.

Contributor

goldfirere commented Feb 4, 2018

A few reactions to this proposal (which I'm reading for the first time today):

  • Quantified constraints also allow forall quantification. This should be explicit in the proposal. The current syntactic extension just mentions a context to the left of a class, but not fresh variables. Note that this is different than the forall allowed in an instance declaration, which just makes something explicit which was previously implicit. The forall in a quantified constraint is wholly new.

  • While summarizing the typing rules in the proposal may be hard to do, I agree with the TODO that it should explicitly address backtracking. In particular, what happens when quantified constraints lead to more than one way to solve a constraint? I believe that Simon has proposed (offline) to reject such situations as ambiguous, but this needs to be in the proposal (with an example).

  • As mentioned on GHC's #9123, the second issue could be solved by proactively expanding superclasses even in quantified constraints. I don't think this would be troublesome. If this expansion leads to an ambiguity that might lead to backtracking, then reject. Is that rejection becomes bothersome in real life, then we'll think more creatively with a concrete example.

I'm in strong support of this proposal, and favor QuantifiedConstraints over RankNConstraints. I find the former less jargony.

@treeowl

This comment has been minimized.

Show comment
Hide comment
@treeowl

treeowl Feb 4, 2018

Contributor

@simonpj, one example from the proposal:

class (forall m. Monad m => Monad (t m)) => Trans t where
  lift :: Monad m => m a -> (t m) a

Suppose we're given

instance Applicative m => Monad (T m)
instance Trans t
instance Functor M
instance Applicative M

Suppose we need Monad (T M). How do we resolve it? We might try using the Trans T instance. This leads us on a (fruitless) hunt for Monad M. The only way we can succeed is instead to use the Monad (T m) instance. This issue was discussed, but not entirely resolved, in the draft paper I skimmed. It smells as though constraint quantification without implication may not suffer from this problem, and if that's so it would argue for splitting into two extensions.

Contributor

treeowl commented Feb 4, 2018

@simonpj, one example from the proposal:

class (forall m. Monad m => Monad (t m)) => Trans t where
  lift :: Monad m => m a -> (t m) a

Suppose we're given

instance Applicative m => Monad (T m)
instance Trans t
instance Functor M
instance Applicative M

Suppose we need Monad (T M). How do we resolve it? We might try using the Trans T instance. This leads us on a (fruitless) hunt for Monad M. The only way we can succeed is instead to use the Monad (T m) instance. This issue was discussed, but not entirely resolved, in the draft paper I skimmed. It smells as though constraint quantification without implication may not suffer from this problem, and if that's so it would argue for splitting into two extensions.

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 5, 2018

Contributor

I don't understand @treeowl 's last comment. I assume you meant instance Trans T (with a capital T). But then, why would GHC ever consult the Trans T instance when solving for Monad (T M)? It could only use an instance for Monad, such as instance Applicative M => Monad (T M). This then works out.

I don't see how the implication constraint matters at all here, sorry.

Contributor

goldfirere commented Feb 5, 2018

I don't understand @treeowl 's last comment. I assume you meant instance Trans T (with a capital T). But then, why would GHC ever consult the Trans T instance when solving for Monad (T M)? It could only use an instance for Monad, such as instance Applicative M => Monad (T M). This then works out.

I don't see how the implication constraint matters at all here, sorry.

@treeowl

This comment has been minimized.

Show comment
Hide comment
@treeowl

treeowl Feb 5, 2018

Contributor

Yes, I meant Trans T. We do indeed need Monad (T M). But Trans T gives us a way to get that: the implication superclass constraint on T.

Contributor

treeowl commented Feb 5, 2018

Yes, I meant Trans T. We do indeed need Monad (T M). But Trans T gives us a way to get that: the implication superclass constraint on T.

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 5, 2018

Contributor

But we never use a global instance to access its superclass constraints. After all, if a global instance is accepted, then the superclass constraints are available elsewhere, anyway. Perhaps you're concerned if those instances are listed in the constraints of a function?

Contributor

goldfirere commented Feb 5, 2018

But we never use a global instance to access its superclass constraints. After all, if a global instance is accepted, then the superclass constraints are available elsewhere, anyway. Perhaps you're concerned if those instances are listed in the constraints of a function?

@treeowl

This comment has been minimized.

Show comment
Hide comment
@treeowl

treeowl Feb 5, 2018

Contributor

Yes, I was struggling to come up with a precise example, but that's the gist.

Contributor

treeowl commented Feb 5, 2018

Yes, I was struggling to come up with a precise example, but that's the gist.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 5, 2018

Contributor

Then (at risk of overburdening QuantifiedConstraints) is this the time to introduce per-instance UndecidableInstances?

I'm all for per-instance UndecidableInstances. Maybe someone would like to make a proposal and offer a patch? I think everyone would welcome it.

Contributor

simonpj commented Feb 5, 2018

Then (at risk of overburdening QuantifiedConstraints) is this the time to introduce per-instance UndecidableInstances?

I'm all for per-instance UndecidableInstances. Maybe someone would like to make a proposal and offer a patch? I think everyone would welcome it.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 5, 2018

I'm worried about this rather stark statement:

A quantified constraint is a bit like a local instance declaration.

As I understand it, QuantifiedConstraints is not introducing local instances, as occasionally requested for Haskell -- that is, choose a different instance in different modules/as you can somewhat achieve with orphan instances. The hs2017 paper contrasts its approach with COCHIS which does have local instances (following Scala). There's quite a discussion of the consequences for instance resolution.

The hs2017 paper does use "local" extensively in describing how its axioms work. But this means local evidence at the use sites.

I think it's unwise to use "local instance" in describing this extension to end users. Perhaps it's better put as:

  • A quantified constraint is in effect an instance declaration made available internally to the surrounding instance.

(I can see, as @goldfirere points out, it's going to be hard to explain the typing rules; especially in error messages when GHC has failed to solve a constraint even after backtracking. Thinking in terms of "local instances" won't help.)

AntC2 commented Feb 5, 2018

I'm worried about this rather stark statement:

A quantified constraint is a bit like a local instance declaration.

As I understand it, QuantifiedConstraints is not introducing local instances, as occasionally requested for Haskell -- that is, choose a different instance in different modules/as you can somewhat achieve with orphan instances. The hs2017 paper contrasts its approach with COCHIS which does have local instances (following Scala). There's quite a discussion of the consequences for instance resolution.

The hs2017 paper does use "local" extensively in describing how its axioms work. But this means local evidence at the use sites.

I think it's unwise to use "local instance" in describing this extension to end users. Perhaps it's better put as:

  • A quantified constraint is in effect an instance declaration made available internally to the surrounding instance.

(I can see, as @goldfirere points out, it's going to be hard to explain the typing rules; especially in error messages when GHC has failed to solve a constraint even after backtracking. Thinking in terms of "local instances" won't help.)

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 7, 2018

Thank you @Gertjan423 for the extra explanations of backtracking, that's an excellent example.

Sorry to be wordsmithing again, but do we want to use "Overlap" to describe the situation where different axioms have a common wanted conclusion? I know "overlapping axioms" is the wording that the hs2017 paper uses, but it's going to get easily confused with 'Overlapping Instances'. Again I'm thinking about error messages explaining why some constraint hasn't been resolved.

Can we steal some wording from the terminology of Horn clauses? What we have is multiple axioms with a common goal. The goal is a wanted arising from a superclass constraint (Ca => F a) in your example. To resolve, inference needs to find an axiom (or a chain of axioms) arriving at that goal from the givens. In your example that's directly available ((Ba => C a) => E a), but in general it's an NP-hard problem of connecting chains.

AntC2 commented Feb 7, 2018

Thank you @Gertjan423 for the extra explanations of backtracking, that's an excellent example.

Sorry to be wordsmithing again, but do we want to use "Overlap" to describe the situation where different axioms have a common wanted conclusion? I know "overlapping axioms" is the wording that the hs2017 paper uses, but it's going to get easily confused with 'Overlapping Instances'. Again I'm thinking about error messages explaining why some constraint hasn't been resolved.

Can we steal some wording from the terminology of Horn clauses? What we have is multiple axioms with a common goal. The goal is a wanted arising from a superclass constraint (Ca => F a) in your example. To resolve, inference needs to find an axiom (or a chain of axioms) arriving at that goal from the givens. In your example that's directly available ((Ba => C a) => E a), but in general it's an NP-hard problem of connecting chains.

Stuff from Simon
* Termination
* Instance selection
* Type variable in the head
@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 7, 2018

Contributor

QuantifiedConstraints is not introducing local instances, as occasionally requested for Haskell

But it is, really! Consider

f :: forall m.  (forall a. Eq a => Eq (m a)) => blah
f = ...rhs...

Then in f' right hand side it is really as if we had an instance declaration

instance Eq a => Eq m a

available locally, in that RHS only.

The difference is that these instances are always provided by GHC itself (by solving the wanted constraint at f's call site) rather than by user-written code. That alleviates the coherence worries.

Contributor

simonpj commented Feb 7, 2018

QuantifiedConstraints is not introducing local instances, as occasionally requested for Haskell

But it is, really! Consider

f :: forall m.  (forall a. Eq a => Eq (m a)) => blah
f = ...rhs...

Then in f' right hand side it is really as if we had an instance declaration

instance Eq a => Eq m a

available locally, in that RHS only.

The difference is that these instances are always provided by GHC itself (by solving the wanted constraint at f's call site) rather than by user-written code. That alleviates the coherence worries.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 7, 2018

Contributor

Thanks for all the feedback!

I have made some changes:

  • Notes on coherence
  • Notes on termination
  • Extension to allow a type variable at the head
  • Embrace Richard's superclass idea

I have not implemented all of this, but I'm confident it will not be hard.

Time for another look!

Contributor

simonpj commented Feb 7, 2018

Thanks for all the feedback!

I have made some changes:

  • Notes on coherence
  • Notes on termination
  • Extension to allow a type variable at the head
  • Embrace Richard's superclass idea

I have not implemented all of this, but I'm confident it will not be hard.

Time for another look!

@glaebhoerl

This comment has been minimized.

Show comment
Hide comment
@glaebhoerl

glaebhoerl commented Feb 7, 2018

(Is https://ghc.haskell.org/trac/ghc/ticket/9115 relevant here in any way?)

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 8, 2018

... local instances ...

But it is, really! Consider ...

... The difference is ... That alleviates the coherence worries.

Thanks @simonpj, but I have no worries about coherence. I can see the sense in which QuantifiedConstraints introduces a constraint limited "to that RHS only". The nested constraint applies globally wherever the outer instance applies.

Let me re-punctuate:
QuantifiedConstraints is not introducing local instances as occasionally requested for Haskell.

It's introducing constraints localised in a way different to how occasionally requested. I am worried that calling them "local instances" will confuse people who want per-module instances aka "scoped instances". Because QuantifiedConstraints doesn't provide "scoped instances".

AntC2 commented Feb 8, 2018

... local instances ...

But it is, really! Consider ...

... The difference is ... That alleviates the coherence worries.

Thanks @simonpj, but I have no worries about coherence. I can see the sense in which QuantifiedConstraints introduces a constraint limited "to that RHS only". The nested constraint applies globally wherever the outer instance applies.

Let me re-punctuate:
QuantifiedConstraints is not introducing local instances as occasionally requested for Haskell.

It's introducing constraints localised in a way different to how occasionally requested. I am worried that calling them "local instances" will confuse people who want per-module instances aka "scoped instances". Because QuantifiedConstraints doesn't provide "scoped instances".

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 8, 2018

@glaebhoerl I rather think not. #9115 wants

(=>) :: Constraint -> * -> *

But a nested => in a QuantifiedConstraint is (arguably) of kind

(=>) :: Constraint -> Constraint -> Constraint

Also by this proposal, we can introduce nested foralls. Trying to treat => as a type/kind-level operator might suggest it could be partially applied. Whereas this proposal needs it as special syntax.

See also ekmett's last comment on the ticket about the strength of implications.

AntC2 commented Feb 8, 2018

@glaebhoerl I rather think not. #9115 wants

(=>) :: Constraint -> * -> *

But a nested => in a QuantifiedConstraint is (arguably) of kind

(=>) :: Constraint -> Constraint -> Constraint

Also by this proposal, we can introduce nested foralls. Trying to treat => as a type/kind-level operator might suggest it could be partially applied. Whereas this proposal needs it as special syntax.

See also ekmett's last comment on the ticket about the strength of implications.

@glaebhoerl

This comment has been minimized.

Show comment
Hide comment
@glaebhoerl

glaebhoerl Feb 8, 2018

But a nested => in a QuantifiedConstraint is (arguably) of kind ...

Hmm yes. In that case it's relevant in the sense that they are in conflict. =)

Also by this proposal, we can introduce nested foralls.

Is this any different from the situation with RankNTypes and -> though?

(Note I'm not proposing anything nor suggesting any problem, just out of curiosity.)

glaebhoerl commented Feb 8, 2018

But a nested => in a QuantifiedConstraint is (arguably) of kind ...

Hmm yes. In that case it's relevant in the sense that they are in conflict. =)

Also by this proposal, we can introduce nested foralls.

Is this any different from the situation with RankNTypes and -> though?

(Note I'm not proposing anything nor suggesting any problem, just out of curiosity.)

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 8, 2018

Contributor

Yes, this is different than -> in RankNTypes. Both Int and forall a. Maybe a -> Maybe a have kind Type, so the -> has the same kind in a higher-rank situation as it normally does. If we were ever to make => a first-class construct, though, this proposal would cause trouble, as => would sometimes have kind Constraint -> Type -> Type and sometimes Constraint -> Constraint -> Constraint.

Contributor

goldfirere commented Feb 8, 2018

Yes, this is different than -> in RankNTypes. Both Int and forall a. Maybe a -> Maybe a have kind Type, so the -> has the same kind in a higher-rank situation as it normally does. If we were ever to make => a first-class construct, though, this proposal would cause trouble, as => would sometimes have kind Constraint -> Type -> Type and sometimes Constraint -> Constraint -> Constraint.

@RyanGlScott

This comment has been minimized.

Show comment
Hide comment
@RyanGlScott

RyanGlScott Feb 8, 2018

Contributor

Why is it just this proposal that would cause trouble? Can't (=>) already have kind Constraint -> Constraint -> Constraint in instance declarations? e.g., instance Foo a => Foo (Bar a). I don't see how quantified constraints would make things any worse in this regard.

Contributor

RyanGlScott commented Feb 8, 2018

Why is it just this proposal that would cause trouble? Can't (=>) already have kind Constraint -> Constraint -> Constraint in instance declarations? e.g., instance Foo a => Foo (Bar a). I don't see how quantified constraints would make things any worse in this regard.

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Feb 8, 2018

Contributor

The => in instance declarations could be considered part of the top-level instance concrete syntax and so could easily be special-cased. Ditto the => in class declarations. But this proposal includes a => that can be arbitrarily nested, and so poses more of a challenge.

Contributor

goldfirere commented Feb 8, 2018

The => in instance declarations could be considered part of the top-level instance concrete syntax and so could easily be special-cased. Ditto the => in class declarations. But this proposal includes a => that can be arbitrarily nested, and so poses more of a challenge.

@Ericson2314

This comment has been minimized.

Show comment
Hide comment
@Ericson2314

Ericson2314 Feb 8, 2018

I think we'll want a polymorphic return kind to => anyways, for e.g. unlifted kinds, so I'm not concerned.

Quantified constraints also allow forall quantification. This should be explicit in the proposal. The current syntactic extension just mentions a context to the left of a class, but not fresh variables. Note that this is different than the forall allowed in an instance declaration, which just makes something explicit which was previously implicit. The forall in a quantified constraint is wholly new.

Is this resolved? The proposal does specify the interaction of QualifiedConstraints and ExplicitForall, but still treats higher-ranked foralls in constraints as a sort of free feature anyways.

Ericson2314 commented Feb 8, 2018

I think we'll want a polymorphic return kind to => anyways, for e.g. unlifted kinds, so I'm not concerned.

Quantified constraints also allow forall quantification. This should be explicit in the proposal. The current syntactic extension just mentions a context to the left of a class, but not fresh variables. Note that this is different than the forall allowed in an instance declaration, which just makes something explicit which was previously implicit. The forall in a quantified constraint is wholly new.

Is this resolved? The proposal does specify the interaction of QualifiedConstraints and ExplicitForall, but still treats higher-ranked foralls in constraints as a sort of free feature anyways.

@simonpj

This comment has been minimized.

Show comment
Hide comment
@simonpj

simonpj Feb 23, 2018

Contributor

Rather to my surprise, there hasn't been much more discussion of this quantified-constraints proposal, despite the significant generalisations I added a couple of weeks ago.

Does this mean it's ready for the committee? Do take a look.

PS: The Haskell Weekly news had a nice blog post from Ryan Scott about using quantified constraints How to derive Generic for (some) GADTs using QuantifiedConstraints.

Contributor

simonpj commented Feb 23, 2018

Rather to my surprise, there hasn't been much more discussion of this quantified-constraints proposal, despite the significant generalisations I added a couple of weeks ago.

Does this mean it's ready for the committee? Do take a look.

PS: The Haskell Weekly news had a nice blog post from Ryan Scott about using quantified constraints How to derive Generic for (some) GADTs using QuantifiedConstraints.

@AntC2

This comment has been minimized.

Show comment
Hide comment
@AntC2

AntC2 Feb 26, 2018

@simonpj, I would take heart from the number of Hooray's voted at the first announcement.

It seems the idea was well-prefigured. I hadn't seen that myself, but the syntax and semantics seem 'obvious' (as soon as you point them out).

... there hasn't been much more discussion ...

I guess people are thinking it's a done deal/just get on with it. You've been very clear you don't want to introduce instance search or backtracking into ghc, so the Reject if in doubt tactic seems a prudent starting point.

..., despite the significant generalisations ...

And I would add motivations.

I can think of gazillions of motivations. But what I have in mind seem rather different in nature than your 2000 paper, or the hs2017 paper or @RyanGlScott's or @Iceland_jack's test cases/his reddit blog. Perhaps I'm not understanding; or I'm expecting too much?

So I didn't want to pollute this discussion, but rather posted in another place. So far not a sausage. The differences I see:

  • I'm relying on type equality constraints ~ in the arms of the implications. Will that fit with named TypeClass inference?
  • For the approach to FunDeps for Trac #10675, there's a cycle in the superclass constraints. Does that matter if the cycle is nested inside an implication? Does UndecidableSuperClasses allow it to work?

AntC2 commented Feb 26, 2018

@simonpj, I would take heart from the number of Hooray's voted at the first announcement.

It seems the idea was well-prefigured. I hadn't seen that myself, but the syntax and semantics seem 'obvious' (as soon as you point them out).

... there hasn't been much more discussion ...

I guess people are thinking it's a done deal/just get on with it. You've been very clear you don't want to introduce instance search or backtracking into ghc, so the Reject if in doubt tactic seems a prudent starting point.

..., despite the significant generalisations ...

And I would add motivations.

I can think of gazillions of motivations. But what I have in mind seem rather different in nature than your 2000 paper, or the hs2017 paper or @RyanGlScott's or @Iceland_jack's test cases/his reddit blog. Perhaps I'm not understanding; or I'm expecting too much?

So I didn't want to pollute this discussion, but rather posted in another place. So far not a sausage. The differences I see:

  • I'm relying on type equality constraints ~ in the arms of the implications. Will that fit with named TypeClass inference?
  • For the approach to FunDeps for Trac #10675, there's a cycle in the superclass constraints. Does that matter if the cycle is nested inside an implication? Does UndecidableSuperClasses allow it to work?

@AntC2 AntC2 referenced this pull request Feb 27, 2018

Closed

Instance apartness guards #56

@RyanGlScott RyanGlScott referenced this pull request Mar 1, 2018

Closed

Possibly add `ComposeT` #4

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Apr 6, 2018

Contributor

Simon submitted this for review (via the mailing list)

Contributor

nomeata commented Apr 6, 2018

Simon submitted this for review (via the mailing list)

@nomeata nomeata merged commit 14b5898 into ghc-proposals:master Apr 24, 2018

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Apr 24, 2018

Contributor

Yay, accepted!

Contributor

nomeata commented Apr 24, 2018

Yay, accepted!

@AntC2 AntC2 referenced this pull request Jul 4, 2018

Open

Decidable Instances #114

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