CODEWITHSUNDEEP
purescript
Code Whisperer
Code Whisperer

Reputation: 23652

PureScript - Inferred Type Causes Compiler Warning

Consider the following simple snippet of PureScript code

a :: Int
a = 5

b :: Int
b = 7

c = a + b

main ∷ Effect Unit
main = do
  logShow c

The program successfully infers the type of C to be Int, and outputs the expected result:

12

However, it also produces this warning:

 No type declaration was provided for the top-level declaration of c.
    It is good practice to provide type declarations as a form of documentation.
    The inferred type of c was:
         
      Int
         

  in value declaration c

I find this confusing, since I would expect the Int type for C to be safely inferred. Like it often says in the docs, "why derive types when the compiler can do it for you?" This seems like a textbook example of the simplest and most basic type inference.

  1. Is this warning expected? Is there a standard configuration that would suppress it?
  2. Does this warning indicate that every variable should in fact be explicitly typed?

Upvotes: 1

Views: 118

Answers (1)

Fyodor Soikin
Fyodor Soikin

Reputation: 80744

In most cases, and certainly in the simplest cases, the types can be inferred unambiguously, and indeed, in those cases type signatures are not necessary at all. This is why simpler languages, such as F#, Ocaml, or Elm, do not require type signatures.

But PureScript (and Haskell) has much more complicated cases too. Constrained types are one. Higher-rank types are another. It's a whole mess. Don't get me wrong, I love me some high-power type system, but the sad truth is, type inference works ambiguously with all of that stuff a lot of the time, and sometimes doesn't work at all.

In practice, even when type inference does work, it turns out that its results may be wildly different from what the developer intuitively expects, leading to very hard to debug issues. I mean, type errors in PureScript can be super vexing as it is, but imagine that happening across multiple top-level definitions, across multiple modules, even perhaps across multiple libraries. A nightmare!

So over the years a consensus has formed that overall it's better to have all the top-level definitions explicitly typed, even when it's super obvious. It makes the program much more understandable and puts constraints on the typechecker, providing it with "anchor points" of sorts, so it doesn't go wild.

But since it's not a hard requirement (most of the time), it's just a warning, not an error. You can ignore it if you wish, but do that at your own peril.

Now, another part of your question is whether every variable should be explicitly typed, - and the answer is "no".

As a rule, every top-level binding should be explicitly typed (and that's where you get a warning), but local bindings (i.e. let and where) don't have to, unless you need to clarify something that the compiler can't infer.

Moreover, in PureScript (and modern Haskell), local bindings are actually "monomorphised" - that's a fancy term basically meaning they can't be generic unless explicitly specified. This solves the problem of all the ambiguous type inference, while still working intuitively most of the time.

You can notice the difference with the following example:

f :: forall a b. Show a => Show b => a -> b -> String
f a b = s a <> s b
  where
    s x = show x

On the second line s a <> s b you get an error saying "Could not match type b with type a"

This happens because the where-bound function s has been monomorphised, - meaning it's not generic, - and its type has been inferred to be a -> String based on the s a usage. And this means that s b usage is ill-typed.

This can be fixed by giving s an explicit type signature:

f :: forall a b. Show a => Show b => a -> b -> String
f a b = s a <> s b
  where
    s :: forall x. Show x => x -> String
    s x = show x

Now it's explicitly specified as generic, so it can be used with both a and b parameters.

Upvotes: 1

Related Questions