Function return type signatures

[ghost]

This is a proposal to augment the existing ScopedTypeVariables extension to permit in-line function return type signatures, which are already recognised by the Happy grammar, but currently rejected. Such signatures can easily be given meaning and do permit very concise in-line type signature definitions.

Rendered

[AntC2]

Ooh yes!

Presumably this allows binding tyvars; where do constraints go?:

f (x :: a) :: Num a => Maybe a = Just x

Hmm. That's not pretty. But then neither is:

f (x :: a) = Just x :: Num a => Maybe a 

The main motivation I see (I'm not coming from Scala/etc) is to avoid using ScopedTypeVariables with that daft rule about needing explicit forall. That applies particularly inside where decls attached to a function/method.

[ghost]

Yes this would allow tyvars bound via pattern signatures as in your example, the only issue is that these are bound rigid (as discussed in the proposal). Thus we may want to permit an inline explicit forall somewhere as part of this proposal, or perhaps change the default binding behaviour for such pattern signatures under certain circumstances. Interestingly OCaml also requires explicit forall bindings for such inline signatures, if universal quantification is required.

[Ericson2314]

I believe there is already a proposal to relax the rigidity requirement.

[goldfirere]

"Where do constraints go?" is a good question. I propose: nowhere. That is, if you want explicit constraints, write a top-level type signature.

The ability to bind type variables in patterns is not new with this proposal, and the rigidity requirement seems orthogonal.

If a user writes an inline signature such as this, is it considered a full signature? For example:

f (x :: a) :: a = x + 1

Is that accepted? It needs a Num a constraint. If the signature is considered incomplete, then GHC would accept by inferring the missing bits. If the signature is considered complete, then GHC would reject. If this is considered a complete signature, what about

g (x :: a) _ :: a = x + 1

No one has given the type of _. So this looks incomplete to me.

Upshot to all this: if we consider any of these complete, then we're looking down the barrel of CUSKs, which have proven to be very confusing in type declarations. (Whether or not a type declaration is considered to have a complete type is defined by a somewhat-arbitrary set of syntactic hints.) I thus propose: no inline signature is considered complete. This means both that GHC would infer any constraints as necessary, and that polymorphic recursion would not be allowed with these signatures.

By the way, I do think this would be a nice syntactic convenience. Thanks for writing it up.

[AntC2]

@goldfirere I propose: nowhere. [for constraints]

?So this proposal is not as conceptually simple as shunting the signature from the end of the rhs to the end of the lhs?

Some personage is already complaining about the "veritable zoo of special cases". Is this going to be a different species of duck-billed platypus?

if you want explicit constraints, write a top-level type signature.

... or put the return signature on rhs.

[howtonotwin]

No, it is as simple as shunting the signature from the RHS to the LHS. You cannot add constraints to the type annotation of a RHS today, and you will not be able to add those same constraints on the LHS tomorrow. Using the above example,

f (x :: a) = x + 1 :: a

is not a complete type signature today, and GHC will infer the Num a constraint into f's type. More than that, there is no place to actually write the Num a in the first place. It is also illegal to try polymorphic recursion like:

f (x :: a) = (if x == 0 then x else fromInteger (f (5 :: Integer)) + x) :: a

because that is only possible if there is a complete type signature. Instead, you must write

f :: (Num a, Eq a) => a -> a
f (x :: a) = (if x == 0 then x else fromInteger (f (5 :: Integer)) + x) :: a

Similarly,

f (x :: a) :: a = x + 1

has no complete type signature, and the constraint must be inferred, as there is no place to write it, and, again

f (x :: a) :: a = if x == 0 then x else fromInteger (f (5 :: Integer)) + x

is rejected, as polymorphic recursion is a no-no.

[simonpj]

I can see that this proposal would sometimes be convenient; but I'm not sure that it fully pays its way.

If adopted, I strongly urge that

• This result-signature stuff should NOT have any influence on the notion of a definition having a "complete type signature". Today f has a complete type signature if it has a separate type signature, and that type signature is no partial (i.e. no underscores). Let's stick with that. We are about to add type-level kind signatures precisely because separate type signatures have proved so valuable for terms.

• Treat the result signature EXACTLY like a pattern signature. That is, it is not implicitly quantified, and may bring new type variables into scope. For eaxmple

f xs y  :: a = let  g :: [a] -> a
                    g (p:ps) = p
                    g []     = y
               in g xs

Here the result signature brings a into scope, and it is used in the signature for g.

• Write out the typing rules formally, using the framework of our Haskell Symposium paper: "Type variables in patterns", Haskell Symposium 2018

[Ericson2314]

@AntC2 @goldfirere wrote the top-level signatures proposal, so I think that trac comment is just agreeing with @simonpj's point that we should have no more CUSKs.

I'd like to emphasize that doing this proposal while not adding CUSKs not only avoids problems, but also makes the language more consistent in accordance with the top-level sigs proposal. Together the two would create near-complete "inline signatures" for all declaration types which I believe is a good thing to be consistent about: the user should need true top-level sigs for precisely signature completeness and not anything more (not being able to specify the return type otherwise) or less (there is some CUSK thing that also suffices).

[AntC2]

@howtonotwin You cannot add constraints to the type annotation of a RHS today, ... Using the above example,

   f (x :: a) = x + 1 :: a

I'm confused. Yes for that signature, GHC infers the Num a. So I should be able to explicitly give a constraint that GHC infers anyway(?) Today GHC 8.6.1 with ScopedTypeVariables just accepted

f (x :: a) = x + 1 :: Num a => a

(I have no other signature for f; so a is indeed a new type variable coming into scope.)

there is no place to actually write the Num a in the first place.

Em, I seem to have put Num a into a place. It's true I can't attach the Num a to the pattern sig for x. Indeed I can do this

g (x :: a) = show $ x + 1 :: Num a => String

(That annotation looks weird. GHC infers g :: (Num a, Show a) => a -> String.)

I defer to the experts on whether such sigs should be considered complete/banning polymorphic recursion/CUSKs/etc.

[goldfirere]

My "no place for constraints" comment is saying that there is no special place for constraints. This was confusing -- yes, you can put a constraint on the result type, and that works. But, placing this constraint does not turn off type inference, so it's unsurprising that GHC can infer a Show a constraint even when you didn't write one.

[AntC2]

so it's unsurprising that GHC can infer a Show a constraint even when you didn't write one.

Good. Yes. Quite. Thank you for your "yes". I was getting too many "no"es -- I suspect in answer to questions I did not ask and did not intend and would not understand anyway.

So please could the proposal include the following examples and say they're to be valid, so people can assess whether they're too weird/whether the extra syntax "pays its way":

f (x :: a) :: Num a => Maybe a = Just x

g (x :: a) :: Num a => String = show $ x + 1

And point out that GHC is to infer g :: (Num a, Show a) => a -> String, as currently for the annotation appearing on rhs.

With @nomeata's recent proposal to revive PatternSignatures as a separate extension, I was at first sceptical. But I was won round: the full-bore ScopedTypeVariables is just too hard. That Users Guide section 10.17.4 I understood at the time on the 4th or 5th reading; but looking at it again just now, I had to start over. It just seems easier if the pattern signature "brings the type variables into scope", and the return type signature then uses those variables, rather than all that dicking about with explicit forall in a separate/stand-alone signature.

Then I suggest this proposal is enabled by PatternSignatures alone. (And the full ScopedTypeVariables implies PatternSignatures, so also enables this proposal.)

[simonpj]

Assuming my three suggestions above, there is a very big difference between

f1 x :: a -> a = blah
f2 x = blah :: a -> a

The latter means

f2 x = blah :: forall a. a->a

That is, the a is brought into scope by a forall, and blah must have that polymorphic type. Thus

f2 x = (\y -> x) :: a -> a

is ill-typed.

But I propose that

f1 x :: a -> a = \y -> x

is perfectly well typed. There is no automatic quantification (just as there isn't for patterns. Instead, the result type is constrained to be "something -> something" and a is brought into scope as a name for "something".

These days, pattern-bound type variables can stand for types, not just type variables, so this is also ok

f1a (x :: a) = \y -> (x :: Char)

Here a stands for Char. So this should also be fine

f1b x :: a -> a = \y -> 'v'

with inferred type f1b :: forall t. t -> Char -> Char.

Putting any foralls or constraints on these pattern-bound types gets you into higher-rank types. Tricky territory.

[AntC2]

there is a very big difference between

   f1 x :: a -> a = blah
   f2 x = blah :: a -> a

The former is not currently valid, so how can you claim what it means or what it's different from? What rule are you using? The proposal says that a return type sig on lhs is to mean the same as if it appeared on rhs. Treat that as purely syntactic sugar (to avoid the programmer repeating the sig on multiple rhs equations, and to show it more 'in your face').

But I propose that ...

Stop proposing. If a lhs sig is going to mean something different to a rhs, I see no merit here.

Putting any ... constraints on these pattern-bound types gets you into higher-rank types.

Does it? @goldfirere just said it doesn't. Or by "pattern-bound types" do you mean something different to this (with a constraint, but not taken as a "complete type signature"):

g (x :: a) :: Num a => String = show $ x + 1

You perhaps mean where a var is bound purely by a return type sig, not also bound to an argument? Then does it need a rule: return type signatures must not introduce variables? Please be clear.

The proposal section 4 says

Pattern signatures currently can only introduce rigid, fully-known type variables; and we are somewhat further encouraging their use with this extension ...

It's not clear from the text if this is only a description, or is intended as a prescription/restriction.

[int-index]

Stop proposing. If a lhs sig is going to mean something different to a rhs, I see no merit here.

Why should the meaning be the same? Type signatures in patterns bind type variables, type signatures in expressions introduce type variables. @simonpj argues that we should use the same principle for return type signatures, and it actually seems to have more merit: instead of a syntactic convenience, we get a way to bind variables in the result type.

[int-index]

Now that we have https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst, doing anything else would be neither consistent nor terribly useful.

[AntC2]

Why should the meaning be the same?

Because this proposal says that's what it wants, following the lead from other languages (section 2 to 3):

We propose that this change ... is just a syntactic change.

Because the extension is a simple syntactic addition which can be easily expressed using existing features, I do not expect any unintended effects or interactions.

@int-index doing anything else would be neither consistent nor terribly useful.

(You seem to be using a different sense of "consistent". I guess: what is consistent with which? I.e. not consistent in this sense:)

@howtonotwin it is as simple as shunting the signature from the RHS to the LHS.

Then section 3's (and @howtonotwin's ) claims are false. Then this proposal is terrible and non-useful: kill it.

[int-index]

You seem to be using a different sense of "consistent". I guess: what is consistent with which?

It is consistent with the way ScopedTypeVariables work. Type annotations in patterns and in expressions behave differently when it comes to type variables, and the question is:

• Do we want pattern-like behavior in function return type signatures?
• Do we want expression-like behavior in function return type signatures?

Since it's on the LHS of =, we probably want pattern-like behavior.

[int-index]

Then this proposal is terrible and non-useful: kill it.

I don't get where the "terrible" claim comes from, but the "non-useful" is easy to counter: it becomes useful for everything that the proposal currently claims and for binding parts of the return type to type variables.

[shayan-najd]

cc: @goldfirere @simonpj

This is just a side note related to this proposal to point out some related decisions in the design space. In dependently-typed programming, where GHC Haskell is moving towards to, it is often desired (although languages like Agda lack this) to let named arguments in types (to indicated term dependencies of types) to also be accessible in terms to avoid duplication. For example, in a dependent language, say Agda, we may have

f : (size : Nat) (vec : Vec size Char) ->  Vec size Char
f size vec = M 

Notice the duplication in naming the arguments (the first naming is mandatory for stating the term dependency of types).
Instead, one may want to write in the following "inductive definition" style:

f  (size : Nat) (vec : Vec size Char) 
   : Vec size Char
   = M

How the above style interacts with induction / pattern matching is an important point to consider.

[Icelandjack]

So when do we allow

data Ty :: Type
  = TFree Name
  | Ty :-> Ty

[nomeata]

Little activity recently, marking this as dormant.

[int-index]

@timw-da Do you plan to submit this to the committee?

[ghost]

Given the discussion so far, Digital Asset will reluctantly withdraw the proposal in its current form but would welcome any other contributors that might wish to take it forward.

[nomeata]

Ok, will close this, but encourage anyone who wants to pick it up again to reopen.

[int-index]

Thanks for the information. I will write and submit my version of the proposal.

[int-index]

The new proposal is at #228