More Haskell Blue Sky: Partial Type Annotations

[Ashley Yakeley]

I sometimes come across a situation when I only want to provide a 
_partial_ type annotation, perhaps because the full type has some 
variable unified with some variable in some other type annotation, or 
something. For instance:

  f :: forall a. [a] -> [a] -> [a]
  f x y = g x where
    g [] = y
    g (_:_) = x

...there doesn't seem to be a way of giving a type annotation for 'g'. 
Theoretically it's '[a] -> [a]', but where 'a' is the same as the 'a' in 
the type signature for 'f'.

Under this proposal, unqualified type variables would be considered to be 
'free' rather than implicitly forall-qualified. So for instance, any 
function could be given the partial type annotation 'a -> b'. For 
instance, all these annotations would be the same given this function:

  k :: a
  k :: a -> ba
  k :: a -> b -> a
  k :: forall b. a -> b -> a
  k :: forall a b. a -> b -> a

  k x y = x

...and these would both be the same, but different from the previous:

  k' :: Int -> ba
  k' :: forall b. Int -> b -> Int

  k' x y = x

And so we could write this:

  f :: forall a. [a] -> [a] -> [a]
  f x y = g x where
    g :: [a] -> [a] -- partial annotation may be sufficient
    g [] = y
    g (_:_) = x

I admit that's a bit of a change, and might break programs... In 
addition, it doesn't address the occasional need to tie type annotations 
together, something that has often made me add ugly dummy arguments used 
just for their type.

-- 
Ashley Yakeley, Seattle WA