[ghc-steering-committee] Discussion about "Type Application in Patterns" (#126)

[Richard Eisenberg]

I hate to throw a wrinkle in, but much of this discussion assumes that type arguments come before other arguments after a constructor. This is true today, and there are no immediate plans to change it, but this assumption won't be valid if we have full dependent types. For example, we might want something like

> data T where
>   MkT :: forall k -> Int -> forall (a :: k). TypeRep a -> T

Now, we might get patterns like

> foo (MkT k n @a r) = ...

Without whitespace-sensitivity, I don't think we'll be able to disambiguate between type pattern and as-pattern. (I thought for a moment that we could use the constructor arity as a guide, but this fails if we have two @-signs, where only one is meant to be a type pattern. We won't be able to tell which one!)

Whitespace-sensitivity is bad, but it's not unprecedented in Haskell. Ignoring the layout rule (which is quite different), this is much more like the treatment of `.` and `$`. Specifically, `T . f` is T composed with f, while `T.f` is the name `f` from the module `T`. And `f $ (g x)` is f applied to (g x) while `f $(g x)` is f applied to a splice.

Considering this future of relaxed ordering requirements on data constructors isn't compulsory, but I do think it's better if we don't paint ourselves into a corner around this.

Thanks,
Richard

> On Aug 16, 2018, at 7:27 PM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> 
> Hi,
> 
> Am Donnerstag, den 16.08.2018, 23:22 +0000 schrieb Simon Peyton Jones:
>>>   pattern Ascii :: String
>>>   pattern Ascii <- (all isAscii -> True)
>>> 
>>> and now
>>> 
>>>   foo (Ascii @ ('X':rest)) =
>>> 
>>> is now longer as silly…
>> 
>> That’s a good example.  It's easy to work around:
>> 
>> 	pattern And p q = p at q
>> 
>> 	foo (Ascii `And` ('X' : rest)) = ..
> 
> nice. I included this in the proposal under “Costs and Drawbacks”, for
> future reference.
> 
> Cheers,
> Joachim
> 
> -- 
> Joachim Breitner
>  mail at joachim-breitner.de
>  http://www.joachim-breitner.de/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee