On Nov 8, 2014, at 11:23 AM, "Dr. ERDI Gergo" <[email protected]> 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 _______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
