Proposal: Don't require users to use undefined

[David Menendez]

On Fri, Oct 29, 2010 at 4:09 PM, Ian Lynagh <igloo at earth.li> wrote:
> 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'

This is similar to how Coq does it. If you have a form with implicit
arguments (in our case type arguments), you can add a '@' prefix to
make them explicit. So you'd write @Just Char 'a'.

If we are doing explicit type variables, we might also want to allow _
to mean "infer this argument anyway". That way, when using something
like map:

    map :: forall a b. (a -> b) -> [a] -> [b]

you could write: @map Int _ show to let Haskell infer the second type parameter.

> and also
>
>    map ord "foo" == #map Char Int ord "foo"

I guess this would only work with explicit foralls, otherwise how do
you know which type is the Int and which is the Char?

That is, "forall a b. ..." is different from "forall b a. ...".

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>