Re: Pattern synonym 'Required' constraints === Datatype Contexts(?)

2021-03-11 Thread Lennart Augustsson
The required context on pattern synonyms isn't just useful, it's
necessary.  Since arbitrary computation can happen in both the pattern
matching and construction we need the context.
Take Richard's example, without the context on Positive we would infer the
wrong type for any use of the Positive synonym.


On Thu, Mar 11, 2021 at 7:09 AM Richard Eisenberg  wrote:

> You're right that these features sit in a similar space. The difference is
> that, with a pattern synonym, the required context might be useful. This is
> because pattern synonyms can perform computation (via view patterns), and
> this computation might plausibly require some class constraint. An easy
> example:
>
> pattern Positive :: (Ord a, Num a) => a
> pattern Positive <- ((>0) -> True)
>
>
> Here, the required context is helpful. On the other hand, because matching
> against a data constructor never does computation, the constraints are
> never useful in this way.
>
> Richard
>
> On Mar 9, 2021, at 7:02 PM, Anthony Clayden 
> wrote:
>
> I must be slow on the uptake. I've just grokked this equivalence -- or is
> it? Consider
>
> >data Eq a => Set a = NilSet | ConsSet a (Set a) -- from the
> Language report
> >
> >-- ConsSet :: forall a. Eq a => a -> Set a => Set a   -- inferred/per
> report
> >
> >--  equiv with Pattern syn 'Required' constraint
> >data Set' a = NilSet' | ConsSet' a (Set' a) -- no DT context
> >
> >pattern ConsSetP :: (Eq a) => () => a -> (Set' a) -> (Set' a)
> >pattern ConsSetP x xs = ConsSet' x xs
> >
> >ffP ((ConsSet x xs), (ConsSetP y ys)) = (x, y)
> >
> >-- ffP :: forall {a} {b}. (Eq a, Eq b) => (Set a, Set' b) -> (a, b)
>  -- inferred
>
> The signature decl for `ConsSetP` explicitly gives both the Required `(Eq
> a) =>` and Provided `() =>` constraints, but the Provided could be omitted,
> because it's empty. I get the same signature for both `ConsSetP` as
> `ConsSet` with the DT Context. Or is there some subtle difference?
>
> This typing effect is what got DT Contexts called 'stupid theta' and
> deprecated/removed from the language standard. ("widely considered a
> mis-feature", as GHC is keen to tell me.) If there's no difference, why
> re-introduce the feature for Patterns? That is, why go to the bother of the
> double-context business, which looks weird, and behaves counter to usual
> signatures:
>
> >foo :: (Eq a) => (Show a) => a -> a
> >--   foo :: forall {a}. (Eq a, Show a) => a -> a -- inferred
>
> There is a slight difference possible with Pattern synonyms, compare:
>
> >pattern NilSetP :: (Eq a) => () => (Set' a)
> >pattern NilSetP = NilSet'
> >
> >-- NilSetP :: forall {a}. Eq a => Set' a -- inferred
> >-- NilSet   :: forall {a}.  => Set a   --
> inferred/per report
>
> Using `NilSetP` somewhere needs giving an explicit signature/otherwise
> your types are ambiguous; but arguably that's a better discipline than
> using `NilSet` and allowing a Set with non-comparable element types.
>
> AntC
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Pattern synonym 'Required' constraints === Datatype Contexts(?)

2021-03-11 Thread Richard Eisenberg
You're right that these features sit in a similar space. The difference is 
that, with a pattern synonym, the required context might be useful. This is 
because pattern synonyms can perform computation (via view patterns), and this 
computation might plausibly require some class constraint. An easy example:

> pattern Positive :: (Ord a, Num a) => a
> pattern Positive <- ((>0) -> True)

Here, the required context is helpful. On the other hand, because matching 
against a data constructor never does computation, the constraints are never 
useful in this way.

Richard

> On Mar 9, 2021, at 7:02 PM, Anthony Clayden  
> wrote:
> 
> I must be slow on the uptake. I've just grokked this equivalence -- or is it? 
> Consider
> 
> >data Eq a => Set a = NilSet | ConsSet a (Set a) -- from the Language 
> > report
> >
> >-- ConsSet :: forall a. Eq a => a -> Set a => Set a   -- inferred/per 
> > report
> >
> >--  equiv with Pattern syn 'Required' constraint
> >data Set' a = NilSet' | ConsSet' a (Set' a) -- no DT context
> >
> >pattern ConsSetP :: (Eq a) => () => a -> (Set' a) -> (Set' a)
> >pattern ConsSetP x xs = ConsSet' x xs
> >
> >ffP ((ConsSet x xs), (ConsSetP y ys)) = (x, y)
> >
> >-- ffP :: forall {a} {b}. (Eq a, Eq b) => (Set a, Set' b) -> (a, b)   -- 
> > inferred
> 
> The signature decl for `ConsSetP` explicitly gives both the Required `(Eq a) 
> =>` and Provided `() =>` constraints, but the Provided could be omitted, 
> because it's empty. I get the same signature for both `ConsSetP` as `ConsSet` 
> with the DT Context. Or is there some subtle difference?
> 
> This typing effect is what got DT Contexts called 'stupid theta' and 
> deprecated/removed from the language standard. ("widely considered a 
> mis-feature", as GHC is keen to tell me.) If there's no difference, why 
> re-introduce the feature for Patterns? That is, why go to the bother of the 
> double-context business, which looks weird, and behaves counter to usual 
> signatures:
> 
> >foo :: (Eq a) => (Show a) => a -> a
> >--   foo :: forall {a}. (Eq a, Show a) => a -> a -- inferred
> 
> There is a slight difference possible with Pattern synonyms, compare:
> 
> >pattern NilSetP :: (Eq a) => () => (Set' a)
> >pattern NilSetP = NilSet'
> >
> >-- NilSetP :: forall {a}. Eq a => Set' a -- inferred
> >-- NilSet   :: forall {a}.  => Set a   -- 
> > inferred/per report
> 
> Using `NilSetP` somewhere needs giving an explicit signature/otherwise your 
> types are ambiguous; but arguably that's a better discipline than using 
> `NilSet` and allowing a Set with non-comparable element types.
> 
> AntC
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users