Here is one principle: for GADTs, the pattern type signature should look like
the GADT data constructor. So if we have
data S a where
S1 :: p -> q -> S (p,q)
S2 :: ...blah...
pattern P x y = S1 x y
then surely the signature for P should be
P :: p -> q -> S
One note on the syntax front, 'pattern type' was mentioned as annoyingly
trying to shoehorn the word 'type' in to lean on an existing keyword, even
though its about a term level construction rather than a type level one.
We do have some perfectly serviceable keywords available to us that
indicate
On Wed, 5 Nov 2014, Edward Kmett wrote:
One note on the syntax front, 'pattern type' was mentioned as annoyingly trying
to
shoehorn the word 'type' in to lean on an existing keyword, even though its
about a
term level construction rather than a type level one.
We do have some perfectly service
Just a small note about parsing:
On Tue, 4 Nov 2014, Simon Peyton Jones wrote:
The more I think about this, the more I think we'll just have to bite
the bullet and adapt the syntax for constraints in pattern types, to
distinguish the match-required and match-provided parts. Suppose we let
pat
On Nov 8, 2014, at 11:23 AM, "Dr. ERDI Gergo" wrote:
> So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ..., Um)
> into a type, which would then require rejecting everywhere else where we
> really do mean a type... Sounds painful. Also painful: rewriting the whole
> context p
On Sat, 8 Nov 2014, Richard Eisenberg wrote:
On Nov 8, 2014, at 11:23 AM, "Dr. ERDI Gergo" wrote:
So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ...,
Um) into a type, which would then require rejecting everywhere else
where we really do mean a type... Sounds painful. Also
On Nov 8, 2014, at 10:42 PM, "Dr. ERDI Gergo" wrote:
> Right, but the issue in this case is if we add this artifical constructor to
> HsType just so we can fix it up into a pair of contexts, this constructor
> would permeate everything else that has to do with HsTypes; if nothing else,
> it'd
On Sat, 8 Nov 2014, Richard Eisenberg wrote:
I should also note that I intended the `forall`s to be optional.
Of course, the forall binders are optional in all proposals.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/l
On 11/04/2014 05:32 AM, Simon Peyton Jones wrote:
> The "; match-required" part is optional, and the "match-provided" part might
> be empty. So P1 and P2 would look like this:
>
> pattern P1 :: forall a. (; Num a) => b -> (a,b)
> pattern P2 :: forall a. (; Num a, Ord a) => a -> a
How about
On Tue, 4 Nov 2014, Simon Peyton Jones wrote:
pattern P :: forall tvs. (match-provided ; match-required) => tau
The "; match-required" part is optional, and the "match-provided" part might be
empty. So P1 and P2 would look like this:
pattern P1 :: forall a. (; Num a) => b -> (a,b)
pattern
n effect a modified HsForAll,
just for pattern type signatures, and probably flattened out into
the pattern-signature constructor form itself.
Does that help?
Simon
| -Original Message-
| From: Dr. ERDI Gergo [mailto:ge...@erdi.hu]
| Sent: 09 November 2014 07:56
| To: Simon Peyton Jon
erly interpreting it, but users
already interpret (Foo a, Bar b) => .. differently in different contexts,
e.g. in class and instance declarations. They can adapt.
-Edward
>
> | -Original Message-
> | From: Dr. ERDI Gergo [mailto:ge...@erdi.hu]
> | Sent: 09 November 2014 07:56
On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones wrote:
>
> * One other possibility would be two => thus
> pattern P :: (Eq b) => (Num a, Eq a) => ...blha...
>
I should note that I can say this in 7.8.3:
foo :: Show a => Eq a => a -> String
foo x = show x ++ show (x == x)
Note that I've
on Jones
| Cc: Dr. ERDI Gergo; GHC Devs
| Subject: Re: Concrete syntax for pattern synonym type signatures
|
|
| On Nov 9, 2014, at 2:11 PM, Simon Peyton Jones
| wrote:
| >
| > * One other possibility would be two => thus
| >pattern P :: (Eq b) => (Num a, Eq a) => .
Good news, I've made the necessary parser breakthrough and I've now got
pattern P :: pretty much anything after this point
to parse as a pattern synonym type signature on a local sub-branch of my
branch. So no more annoying 'pattern type' nonsense.
As for the 'pretty much anything' part,
Note though, it doesn't mean the same thing to say (Foo a, Bar a b) => ...
as it does to say
Foo a => Bar a b => ...
The latter can use Foo a when working on Bar a b, but not Bar a b to
discharge Foo a, which makes a difference when you have functional
dependencies.
So in some sense the 'pattern
While I'll admit I still like my bikeshed color choice over Simon's, I'm happy
to go with the fact that there seems to be more momentum behind Simon's.
Instead, let me propose a slight change of shade: put the "required"
constraints *first* and the "provided" ones *second*. Of course, we could l
On Mon, 10 Nov 2014, Richard Eisenberg wrote:
pattern P :: forall a. Num a => forall c. (Eq a, Ord Bool, Show c) => c -> Bool
-> T a Bool
pattern C :: (Eq b, Num b) => () => b -> c -> X Maybe (Maybe b)
Of course, you can drop the `forall`s in `P`'s type.
This has, I believe, several advantag
| Instead, let me propose a slight change of shade: put the "required"
| constraints *first* and the "provided" ones *second*. Of course, we could
| leave out the required constraints.
I'm agnostic about this choice at the moment, but I don't understand your
points.
| So, continuing the examples
an you offer a concrete example, and show that one typechecks
when the other does not?
Simon
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 10 November 2014 15:46
To: Richard Eisenberg
Cc: Simon Peyton Jones; GHC Devs
Subject: Re: Concrete syntax for pattern synonym type signatures
Note thou
Well done! Thanks Gergo.
| -Original Message-
| From: Dr. ERDI Gergo [mailto:ge...@erdi.hu]
| Sent: 10 November 2014 14:09
| To: Simon Peyton Jones
| Cc: Richard Eisenberg; GHC Devs
| Subject: RE: Concrete syntax for pattern synonym type signatures
|
| Good news, I've made the nece
Let me restate the proposals more concretely. Correct me if I'm wrong!
Suppose we have the following declarations:
data T a b where
MkT :: (Eq a, Ord b, Show c) => a -> (b, b) -> c -> T a b
pattern P x y = MkT 5 (y, True) x
What is the type of P?
Simon's proposal:
> pattern P :: (E
dencies.
>
>
>
> I disagree. Can you offer a concrete example, and show that one
> typechecks when the other does not?
>
>
>
> Simon
>
>
>
> *From:* Edward Kmett [mailto:ekm...@gmail.com]
> *Sent:* 10 November 2014 15:46
> *To:* Richard Eisenberg
> *
| My proposal:
|
| > pattern P :: (Num a) => (Eq a, Ord Bool, Show c) => c -> Bool -> T a
| > Bool
|
| My previous comment about bizarre scoping is that the universal
| variables -- which (in my opinion) go with the required constraints --
| scope over both sets of constraints. The existe
24 matches
Mail list logo
