Excellent bikeshedding opportunity! Frontend syntax for pattern synonym types
Hi, As part of my work to add pattern synonyms to GHC (https://ghc.haskell.org/trac/ghc/ticket/5144) I initially planned to postpone implementing type signatures (https://ghc.haskell.org/trac/ghc/ticket/8584). However, since adding the feature in the first place requires Haddock support, some syntax will be needed for pattern synonym type signatures so that at least there's something to generate into the docs. The basic problem with pattern synonyms in this regard is that their type is fully described by the following five pieces of information: 1, Universially bound type variables 2, Existentially bound type variables 3, The (tau) type itself 4, Typeclass context required by the pattern synonym 5, Typeclass context provided by the pattern synonym To give you some parallels, functions are described by (1), (3) and (4), e.g. given the following definition: f = map fromIntegral (1) is {a, b} (3) is [a] -> [b] (4) is (Integral a, Num b) Data constructors are described by (1), (2), (3) and (5), e.g. given data T a where MkT :: (Num a, Eq b) => a -> (b, b) -> T a the type of `MkT` is described by (1) Universially bound type variables {a} (2) Existentially bound type variables {b} (3) Tau type a -> (b, b) -> T a (5) Typeclass context provided is (Num a, Eq b) Note that when using `MkT` in an expression, its type is simpler than that, since it simply becomes forall a b. (Num a, Eq b) => a -> (b, b) -> T a which has exactly the same shape as the previous example which had (1), (3) and (4) specified. However, the context has different semantics (and the distinction between (1) and (2) becomes important) when pattern matching on `MkT`. For pattern synonyms, all five axes are present and orthogonal, and all five is something that a user should care about. For example, given the following code: {-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-} data T a where MkT :: (Num a, Eq b) => a -> b -> T a f :: (Show a) => a -> Bool f = ... pattern P x <- MkT (f -> True) x to fully describe the type of pattern synonym P, we have: (1) Universially quantified type variables {a} (2) Existentially quantified type variables {b} (3) Tau type b -> T a (4) Required context (Show a) (5) Provided context (Num a, Eq b) So, what I'm looking for, is ideas on what syntax to use to represent these five pieces of information. Note that (1) and (2) can be made implicit, just like for constructor types, simply by noting that type variables that don't occur in the result type are existentially bound. So the tricky part is maintaining the distinction between (4) and (5). The current implementation displays the following if you ask for `:info T`: > :info P pattern P :: b -> T t requires (Show t) provides (Num t, Eq b) but I don't think we would want to use that for syntax that is actually enterred by the user into type signatures (if nothing else, then simply because why would we want to use two extra keywords 'requires' and 'provides'). The one idea I've had so far is to separate (4), (3) and (5) with two double arrows: pattern P :: (Show t) => b -> T t => (Num t, Eq b) As an added extra problem, there are also unidirectional and bidirectional pattern synonyms: unidirectional ones are usable only as patterns, whereas bidirectional ones can also be used as expressions. For example: pattern Single x = [x] pattern Second x <- (_:x:_) in this example, `Single` is bidirectional and `Second` is unidirectional. As you can see, this is indicated by syntax in the definition (`=` vs `<-`). However, I'd like to show this in the type as well, since you'd need to be able to see if you can use a given pattern synonym as a "constructor", not just a "destructor", by just looking at its Haddock-generated docs. What do you think? Bye, Gergo -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' Either the chocolate in my pocket has melted, or this is something altogether more sinister.
[Superb summary of pattern synonyms omitted] On 2013-12-22 9:09 AM, Dr. ERDI Gergo wrote:
The one idea I've had so far is to separate (4), (3) and (5) with two double arrows:
pattern P :: (Show t) => b -> T t => (Num t, Eq b)
pattern P :: (Show t) => ( (Num t, Eq b) => b -> T t ) perhaps? Given 'Show t', you get what's on the rhs of the first => ? Another idea is pattern P :: (Show t) ~> (Num t, Eq b) => b -> T t which has the drawback of introducing a new 'keyword'.
As an added extra problem, there are also unidirectional and bidirectional pattern synonyms: unidirectional ones are usable only as patterns, whereas bidirectional ones can also be used as expressions. For example:
pattern Single x = [x] pattern Second x <- (_:x:_)
in this example, `Single` is bidirectional and `Second` is unidirectional. As you can see, this is indicated by syntax in the definition (`=` vs `<-`). However, I'd like to show this in the type as well, since you'd need to be able to see if you can use a given pattern synonym as a "constructor", not just a "destructor", by just looking at its Haddock-generated docs.
Since the first is an iso, why not pattern Single :: t a ~ [ a ] or pattern Single :: t a <-> [ a ] ? [I definitely prefer the first] Or is your 'type' for Single somehow different than my guess? Jacques
On Sun, 22 Dec 2013, Jacques Carette wrote:
Since the first is an iso, why not pattern Single :: t a ~ [ a ] or pattern Single :: t a <-> [ a ] ? [I definitely prefer the first] Or is your 'type' for Single somehow different than my guess?
the type of Single would be 'a -> [a]', as in: in an expression context, if x :: a, then Single x :: [a] in a pattern context, if Single x :: [a], then it binds x :: a -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' The masses are asses.
On Sun, 22 Dec 2013, Jacques Carette wrote:
pattern P :: (Show t) => ( (Num t, Eq b) => b -> T t ) perhaps? Given 'Show t', you get what's on the rhs of the first => ?
I like this one; in fact, I originally wanted to go with something like that. But unfortunately, this type is already valid and is parsed simply as (Show t, Num t, Eq b) => b -> T t by GHC: Prelude> :t undefined :: (Show t) => ((Num t, Eq b) => b -> Maybe t) undefined :: (Show t) => ((Num t, Eq b) => b -> Maybe t) :: (Eq b, Num t, Show t) => b -> Maybe t -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' A pessimist sees the glass half empty, the optimist sees it half full and the blind can't see shit
Other than being
A. displayed in the Haddocks
will this syntax also, now or at any later point, be
B. explicitly written by the programmer alongside the definition of the
pattern, or
C. used as a type argument for other types?
If it's only A and B, perhaps abominations like these could be considered:
-- implicit foralls
pattern Show t => P t :: (Num t, Eq b) => b -> T t
-- explicit foralls
pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T t
where I'm grafting together syntax originally from `DatatypeContexts` and
`GADTs`. The foralls could each be either illegal, optional, or necessary.
I think the `DatatypeContexts` syntax gives a good intuition: you're
required to put something in, but don't get to take it back out.
On Sun, Dec 22, 2013 at 3:09 PM, Dr. ERDI Gergo
Hi,
As part of my work to add pattern synonyms to GHC ( https://ghc.haskell.org/trac/ghc/ticket/5144) I initially planned to postpone implementing type signatures (https://ghc.haskell.org/trac/ ghc/ticket/8584). However, since adding the feature in the first place requires Haddock support, some syntax will be needed for pattern synonym type signatures so that at least there's something to generate into the docs.
The basic problem with pattern synonyms in this regard is that their type is fully described by the following five pieces of information:
1, Universially bound type variables 2, Existentially bound type variables 3, The (tau) type itself 4, Typeclass context required by the pattern synonym 5, Typeclass context provided by the pattern synonym
To give you some parallels, functions are described by (1), (3) and (4), e.g. given the following definition:
f = map fromIntegral
(1) is {a, b} (3) is [a] -> [b] (4) is (Integral a, Num b)
Data constructors are described by (1), (2), (3) and (5), e.g. given
data T a where MkT :: (Num a, Eq b) => a -> (b, b) -> T a
the type of `MkT` is described by
(1) Universially bound type variables {a} (2) Existentially bound type variables {b} (3) Tau type a -> (b, b) -> T a (5) Typeclass context provided is (Num a, Eq b)
Note that when using `MkT` in an expression, its type is simpler than that, since it simply becomes
forall a b. (Num a, Eq b) => a -> (b, b) -> T a
which has exactly the same shape as the previous example which had (1), (3) and (4) specified. However, the context has different semantics (and the distinction between (1) and (2) becomes important) when pattern matching on `MkT`.
For pattern synonyms, all five axes are present and orthogonal, and all five is something that a user should care about. For example, given the following code:
{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-} data T a where MkT :: (Num a, Eq b) => a -> b -> T a
f :: (Show a) => a -> Bool f = ...
pattern P x <- MkT (f -> True) x
to fully describe the type of pattern synonym P, we have:
(1) Universially quantified type variables {a} (2) Existentially quantified type variables {b} (3) Tau type b -> T a (4) Required context (Show a) (5) Provided context (Num a, Eq b)
So, what I'm looking for, is ideas on what syntax to use to represent these five pieces of information.
Note that (1) and (2) can be made implicit, just like for constructor types, simply by noting that type variables that don't occur in the result type are existentially bound. So the tricky part is maintaining the distinction between (4) and (5).
The current implementation displays the following if you ask for `:info T`:
> :info P pattern P :: b -> T t requires (Show t) provides (Num t, Eq b)
but I don't think we would want to use that for syntax that is actually enterred by the user into type signatures (if nothing else, then simply because why would we want to use two extra keywords 'requires' and 'provides').
The one idea I've had so far is to separate (4), (3) and (5) with two double arrows:
pattern P :: (Show t) => b -> T t => (Num t, Eq b)
As an added extra problem, there are also unidirectional and bidirectional pattern synonyms: unidirectional ones are usable only as patterns, whereas bidirectional ones can also be used as expressions. For example:
pattern Single x = [x] pattern Second x <- (_:x:_)
in this example, `Single` is bidirectional and `Second` is unidirectional. As you can see, this is indicated by syntax in the definition (`=` vs `<-`). However, I'd like to show this in the type as well, since you'd need to be able to see if you can use a given pattern synonym as a "constructor", not just a "destructor", by just looking at its Haddock-generated docs.
What do you think?
Bye, Gergo
--
.--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' Either the chocolate in my pocket has melted, or this is something altogether more sinister. _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Sun, 22 Dec 2013, Gábor Lehel wrote:
Other than being
A. displayed in the Haddocks
will this syntax also, now or at any later point, be
B. explicitly written by the programmer alongside the definition of the pattern, or
C. used as a type argument for other types?
A and B.
If it's only A and B, perhaps abominations like these could be considered:
-- implicit foralls pattern Show t => P t :: (Num t, Eq b) => b -> T t
-- explicit foralls pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T t
I'm not 100% sure what that 't' in 'P t' is supposed to be in your example. 'P' is not like a type constructor at all; it's a lot more like a data constructor. -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' I know KUNG FU, KARATE and 47 other dangerous words.
On Sun, 22 Dec 2013, Dr. ERDI Gergo wrote:
If it's only A and B, perhaps abominations like these could be considered:
-- implicit foralls pattern Show t => P t :: (Num t, Eq b) => b -> T t
-- explicit foralls pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T t
I'm not 100% sure what that 't' in 'P t' is supposed to be in your example. 'P' is not like a type constructor at all; it's a lot more like a data constructor.
Thinking further about it, I think this could work, using a syntax similar to data constructor definitions instead of sticking to the function type syntax: pattern (Num a, Eq b) => P a b :: (Show a) => T a or with explicit foralls (using the fact that we can deduce which tyvars are universial vs existential simply by seeing if they occur in 'T a'): pattern forall a b. (Num a, Eq b) => P a b :: (Show a) => T a my only concern with this one is that the direction of the first double arrow doesn't "feel right". Other examples with this syntax: -- Number literal patterns pattern Z :: (Num a, Eq a) => a pattern Z = 0 -- Monomorphic patterns pattern TrueAnd Bool :: [Bool] pattern TrueAnd b = [True, b] -- Infix notation pattern a :< Seq a :: Seq a pattern x :< xs <- (Seq.viewl -> x Seq.:< xs) I'm liking this so far. Bye, Gergo -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' RICE: Race Inspired Cosmetic Enhancement
i'm confused, are these types ever human writeable?
If not, are they meant to be an operational way of communicating how a
pattern works? In which case, wouldn't having the pattern definition
visible in the haddocks be a simpler way to communicate it? There have
been several projects in the past to have type system for describing lambda
calculi with pretty right higher order pattern matching facilities, perhaps
that vocabulary could be used here?
cheers (i hope my questions make sense, I could merely be confused)
-Carter
On Sun, Dec 22, 2013 at 10:56 PM, Dr. ERDI Gergo
On Sun, 22 Dec 2013, Dr. ERDI Gergo wrote:
If it's only A and B, perhaps abominations like these could be considered:
-- implicit foralls pattern Show t => P t :: (Num t, Eq b) => b -> T t
-- explicit foralls pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T t
I'm not 100% sure what that 't' in 'P t' is supposed to be in your example. 'P' is not like a type constructor at all; it's a lot more like a data constructor.
Thinking further about it, I think this could work, using a syntax similar to data constructor definitions instead of sticking to the function type syntax:
pattern (Num a, Eq b) => P a b :: (Show a) => T a
or with explicit foralls (using the fact that we can deduce which tyvars are universial vs existential simply by seeing if they occur in 'T a'):
pattern forall a b. (Num a, Eq b) => P a b :: (Show a) => T a
my only concern with this one is that the direction of the first double arrow doesn't "feel right".
Other examples with this syntax:
-- Number literal patterns pattern Z :: (Num a, Eq a) => a pattern Z = 0
-- Monomorphic patterns pattern TrueAnd Bool :: [Bool] pattern TrueAnd b = [True, b]
-- Infix notation pattern a :< Seq a :: Seq a pattern x :< xs <- (Seq.viewl -> x Seq.:< xs)
I'm liking this so far.
Bye, Gergo
--
.--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' RICE: Race Inspired Cosmetic Enhancement _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Mon, 23 Dec 2013, Carter Schonwald wrote:
i'm confused, are these types ever human writeable?
Yes, this syntax is meant to be also used for giving human-written type signatures for pattern synonym definitions.
If not, are they meant to be an operational way of communicating how a pattern works? In which case, wouldn't having the pattern definition visible in the haddocks be a simpler way to communicate it?
The pattern definition itself should be abstract for the same reason function definitions are abstract. Imagine if the Haddock docs contained the definition of all functions instead of their types... Bye, Gergo -- .--= ULLA! =-----------------. \ http://gergo.erdi.hu \ `---= gergo@erdi.hu =-------' Post tenebras lux, post fenestras Tux.
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. 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. 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. 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. Best regards, Tsuyoshi
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.
Dear Gergo, Thank you for your prompt reply. Now the ordering makes sense. To be honest, I still find it a little confusing even after knowing that the order is logical, but maybe it is just a matter of getting used to it. Also thank you for the clarification that higher-order pattern functions are outside the scope of the current work. Now I am curious about if/how higher-order pattern functions are useful, how their types can be described, and so on. If they have any applications, they may be a candidate for future work. Best regards, Tsuyoshi
Hi, On Tue, 24 Dec 2013, Tsuyoshi Ito wrote:
Thank you for your prompt reply. Now the ordering makes sense. To be honest, I still find it a little confusing even after knowing that the order is logical, but maybe it is just a matter of getting used to it.
So just to make my position clear: I don't think that syntax is good, it's just the best we've come up with so far:) And the problem is exactly this, that it's not intuitive at all. One source of solace might be that 'provided' contexts will only pop up when you use GADTs with typeclass-constrained constructors, so for less 'power-user' cases, the signature simplifies to something like this: pattern P Bool t :: (Show t) => [t]
Also thank you for the clarification that higher-order pattern functions are outside the scope of the current work. Now I am curious about if/how higher-order pattern functions are useful, how their types can be described, and so on. If they have any applications, they may be a candidate for future work.
I don't have an insight to offer on this at this point. However, I feel there's a huge qualitative difference between higher-order and non-higher-order pattern synonyms in the amount of new concepts that they introduce. I would even go so far as to recommend waiting until a stable GHC release with pattern synonyms (i.e. GHC 7.10 or 8.0 or whatever the next one will be called), and looking at real world usage of them, before jumping into higher-order patsyns. Thanks, Gergo
participants (5)
-
Carter Schonwald -
Dr. ERDI Gergo -
Gábor Lehel -
Jacques Carette -
Tsuyoshi Ito