<div dir="ltr"><div><div><div>Other than being<br></div><br> A. displayed in the Haddocks<br></div><div><br>will this syntax also, now or at any later point, be<br></div><br> B. explicitly written by the programmer alongside the definition of the pattern, or<br>
</div><br> C. used as a type argument for other types?<br><br><div><div><div><div><div><br></div><div>If it's only A and B, perhaps abominations like these could be considered:<br></div><div><br></div><div> -- implicit foralls<br>
</div><div> pattern Show t => P t :: (Num t, Eq b) => b -> T t<br><br></div><div> -- explicit foralls<br></div><div> pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T t<br></div>
<div><br></div><div>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.<br>
</div></div></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Dec 22, 2013 at 3:09 PM, Dr. ERDI Gergo <span dir="ltr"><<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
As part of my work to add pattern synonyms to GHC (<a href="https://ghc.haskell.org/trac/ghc/ticket/5144" target="_blank">https://ghc.haskell.org/trac/<u></u>ghc/ticket/5144</a>) I initially planned to postpone implementing type signatures (<a href="https://ghc.haskell.org/trac/ghc/ticket/8584" target="_blank">https://ghc.haskell.org/trac/<u></u>ghc/ticket/8584</a>). 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.<br>
<br>
The basic problem with pattern synonyms in this regard is that their type is fully described by the following five pieces of information:<br>
<br>
1, Universially bound type variables<br>
2, Existentially bound type variables<br>
3, The (tau) type itself<br>
4, Typeclass context required by the pattern synonym<br>
5, Typeclass context provided by the pattern synonym<br>
<br>
To give you some parallels, functions are described by (1), (3) and (4), e.g. given the following definition:<br>
<br>
f = map fromIntegral<br>
<br>
(1) is {a, b}<br>
(3) is [a] -> [b]<br>
(4) is (Integral a, Num b)<br>
<br>
Data constructors are described by (1), (2), (3) and (5), e.g. given<br>
<br>
data T a where<br>
MkT :: (Num a, Eq b) => a -> (b, b) -> T a<br>
<br>
the type of `MkT` is described by<br>
<br>
(1) Universially bound type variables {a}<br>
(2) Existentially bound type variables {b}<br>
(3) Tau type a -> (b, b) -> T a<br>
(5) Typeclass context provided is (Num a, Eq b)<br>
<br>
Note that when using `MkT` in an expression, its type is simpler than that, since it simply becomes<br>
<br>
forall a b. (Num a, Eq b) => a -> (b, b) -> T a<br>
<br>
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`.<br>
<br>
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:<br>
<br>
{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-}<br>
data T a where<br>
MkT :: (Num a, Eq b) => a -> b -> T a<br>
<br>
f :: (Show a) => a -> Bool<br>
f = ...<br>
<br>
pattern P x <- MkT (f -> True) x<br>
<br>
to fully describe the type of pattern synonym P, we have:<br>
<br>
(1) Universially quantified type variables {a}<br>
(2) Existentially quantified type variables {b}<br>
(3) Tau type b -> T a<br>
(4) Required context (Show a)<br>
(5) Provided context (Num a, Eq b)<br>
<br>
So, what I'm looking for, is ideas on what syntax to use to represent these five pieces of information.<br>
<br>
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).<br>
<br>
The current implementation displays the following if you ask for `:info T`:<br>
<br>
> :info P<br>
pattern P ::<br>
b -> T t<br>
requires (Show t)<br>
provides (Num t, Eq b)<br>
<br>
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').<br>
<br>
The one idea I've had so far is to separate (4), (3) and (5) with two double arrows:<br>
<br>
pattern P :: (Show t) => b -> T t => (Num t, Eq b)<br>
<br>
<br>
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:<br>
<br>
pattern Single x = [x]<br>
pattern Second x <- (_:x:_)<br>
<br>
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.<br>
<br>
<br>
What do you think?<br>
<br>
Bye,<br>
Gergo<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
<br>
.--= ULLA! =-----------------.<br>
\ <a href="http://gergo.erdi.hu" target="_blank">http://gergo.erdi.hu</a> \<br>
`---= <a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a> =-------'<br>
Either the chocolate in my pocket has melted, or this is something altogether more sinister.<br>
______________________________<u></u>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.<u></u>org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/glasgow-<u></u>haskell-users</a><br>
</font></span></blockquote></div><br></div>