Extension request: "where" clauses in type signatures

[danso]

Some type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow for type signatures like the following:

fold :: f -> [a] -> a 
        where f = a -> a -> a

-- expresses intention more clearly than:
fold :: (a -> a -> a) -> [a] -> a

union :: a -> a -> a
         where a = Map.Map k v

-- much shorter/more readable than:
union :: Map.Map k v -> Map.Map k v -> Map.Map k v

Or maybe even:

fmap :: (a -> b) -> f a -> f b
        where (Functor f)

-- arguably prettier than: 
fmap :: (Functor f) => (a -> b) -> f a -> f b

This minor syntactic sugar is essentially equivalent to local "type" definitions, which provides an advantage of making the type's purpose more clear. This seems like a natural development on what the type checker can do.

[nomeata]

fold :: f -> [a] -> a 
        where f :: a -> a -> a

is certainly confusing, because in the first line f is used like a type, but in the second, f is used like a value (or a -> a -> a is used like a kind

Maybe you meant

fold :: f -> [a] -> a 
        where f = a -> a -> a

which could be extended to allow

fold :: f -> [a] -> a 
        where f :: *
              f = a -> a -> a

I’m sure the type level programming wizards and dependently typed programmers will have the greatest need for such an extension, and have a good opinion here.

[danso]

Replying to nomeata:

fold :: f -> [a] -> a 
        where f :: a -> a -> a

is certainly confusing, because in the first line f is used like a type, but in the second, f is used like a value (or a -> a -> a is used like a kind

Maybe you meant

fold :: f -> [a] -> a 
        where f = a -> a -> a

Good catch. I agree that your suggestion makes more sense and have changed the ticket accordingly.

[simonpj]

You can today say

fold :: (f ~ a -> a -> a)
     => f -> [a] -> [a]

which does the job reasonably. I doubt it's worth doing more.

[goldfire]

Replying to simonpj:

fold :: (f ~ a -> a -> a)
     => f -> [a] -> [a]

But doing this changes type inference characteristics, by introducing an equality and making some type variables untouchable. This was pointed out in an earlier bug (sadly, I can't remember any search terms) that highlighted a case where the static semantics of using this sort of trick was different than the expanded form.

The place I've wanted a feature like this most is when writing intricate type families. But there, it would be necessary to allow local type family definitions in the where clause.

All that said, I'm ambivalent about this proposal as stated. It would be useful. But does Simon's trick work often enough? Is it worth specifying, developing, and maintaining this? I'm not sure.

[simonpj]

I don't think it changes the type inference characteristics. Can you give an example?

[goldfire]

No, I don't have one. But I'm sure that there was a ticket complaining about the weirdness of using your trick. However, several minutes of looking through a bunch of tickets has yielded nothing. Maybe I'm imagining things. Until we have evidence of the failure, I agree that we should consider your trick to be a suitable encoding of the proposed idea.