Proposal: Don't require users to use undefined

[Ian Lynagh]

On Wed, Oct 27, 2010 at 07:57:59PM +0000, Simon Peyton-Jones wrote:
> | Drifting off-topic, but wouldn't we want to be able to use similar
> | syntax to bind types too? e.g.
> | 
> |     f ((Just @ t) x) = (Right @ String @ t) x
> | 
> | but @ is unavailable in patterns.
> 
> Oh yes, good point.  It'd be particularly useful in existential patterns:
> 
>   data T where
>    MkT :: forall a. a -> (a -> Int) -> T
> 
>   f (MkT @ a x g) = g (x::a)
> 
> The idea is that the pattern (MkT @ a x g) brings the type variable 'a' into scope.  As you point out, though, '@' is already used in patterns, but perhaps this use is unambiguous.  Confusing though
>    f (MkS @ a x@(p,q) z) = ....
> 
> Maybe someone else can think of good syntax.

The difference in what "Just" means in (Just 'c') and ((Just @ Char) 'c')
feels a bit wrong to me.

Maybe it would be a better to have a syntax to get something with its
real type, and then use normal application, e.g. currently we have

    Just :: forall a . a -> Maybe a
    Just :: Char -> Maybe Char

And if #... is the new syntax then:

    #Just :: /\ a . a -> Maybe a
    #Just Char :: Char -> Maybe Char

    Just 'a' == #Just Char 'a'

and also

    map ord "foo" == #map Char Int ord "foo"


Thanks
Ian