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@erdi.hu =-------' Make it possible for programmers to write programs in English, and you will find that programmers can not write in English.