Concrete syntax for pattern synonym type signatures

[Richard Eisenberg]

On Nov 8, 2014, at 11:23 AM, "Dr. ERDI Gergo" <gergo at erdi.hu> wrote:

> So we would need to add a way of parsing (T1, T2, ..., Tn; U1, U2, ..., Um)
> into a type, which would then require rejecting everywhere else where we really do mean a type... Sounds painful. Also painful: rewriting the whole context parsing code :/

I actually think this wouldn't be all that hard. The same parse-as-wrong-AST-node-and-then-fix-it-up-later trick happens in plenty of places, patterns (parsed as expressions) being one of the biggest. Harder than my proposal, probably, but I don't think it's terrible.

> 
> Richard's suggestion:
> 
>> pattern type forall a. Num a => P :: forall c. (Eq a, Ord Bool, Show c) =>
>>  c -> Bool -> T a Bool
> 
> has the nice property (unlike the current horrible syntax) that the foralls close left-to-right; also, it is very easy to parse :)

One slight infelicity of my syntax is that the `P` is buried.

I should also note that I intended the `forall`s to be optional. The universally-quantified variables would be those that appear in the result type. (I conjecture without proof that the free variables of the required constraints must be a subset of the free variables of the result type. I further conjecture that said proof is easy, but the neurons capable of producing said proof have the night off.) The existentially-quantified variables are the other ones.

Given that the `forall`s are optional and that required constraints are likely rare (I agree there), then the P does not get buried often.

My syntax has the felicity that, like Simon's, if we make a pattern synonym for a GADT constructor, without any funny business, the pattern type is the same as the GADT type. It also supports a reading that says, for the example P, "As long as we have Num a, then P has the type (...)", which is a correct reading of the type.

Richard