Excellent bikeshedding opportunity! Frontend syntax for pattern synonym types

[Dr. ERDI Gergo]

Hi,

On Tue, 24 Dec 2013, Tsuyoshi Ito wrote:

>> pattern (Num a, Eq b) => P a b :: (Show a) => T a
>
> Is “P a b” a typo for “P b”?  Otherwise I cannot see how we can read
> from this signature that pattern synonym P should be used with one
> argument, which is a pattern of type b.

I must have mixed up my examples, sorry. You are right in that it should 
be "P b".

> Is there a reason why the leftmost context is the provided one and the
> context after :: is the required one, rather than the other way
> around?  I am asking this not because I think the other way is better,
> but because to me both look equally good (or equally confusing) and I
> can imagine that I will have trouble remembering which context means
> which, no matter which way is chosen.

There's only one reason I went with that ordering instead of the other. 
Let's go back to the previous example (with the typo fixed):

(1) pattern (Num a, Eq b) => P a b :: (Show a) => T a

vs.

(2) pattern (Show a) => P b :: (Num a, Eq b) => T a

it just weirds me out that in (2), (Num a, Eq b) mentions the type 
variable b, which doesn't occur in 'T a' (since it is existentially 
bound). 
Note that this is true in general: only the provided typeclass constraints 
can mention existentially bound tyvars.

> One thing I like about the above notation better than
>
>>    pattern P ::
>>      b -> T t
>>      requires (Show t)
>>      provides (Num t, Eq b)
>
> or
>
>> pattern P :: (Show t) => b -> T t => (Num t, Eq b)
>
> is that it avoids the use of type constructor (->) because P is
> neither an expression nor a pattern of type “b -> T t”.  At best, P is
> a “pattern function” from a pattern of type b to a pattern of type T
> t, and it has little to do with the function type “b -> T t” if I am
> not mistaken.

Yes, I agree 100%, in fact now I really don't want to go back and whatever 
syntax is eventually agreed upon, it shouldn't use the function type 
notation.

> By the way, do you allow higher-order pattern functions such as
>
>  pattern Q p <- p "Hello"
>
> with which Q P evaluates to
>
>  MkT (f -> True) "Hello"
>
> ?  I guess they are not allowed, but if they are allowed, I do not
> know how their types can be expressed in the syntax you proposed.

This is definitely *not* something we're adding.

Thanks,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Make it possible for programmers to write programs in English, and you will find that programmers can not write in English.