On Wed, Aug 18, 2021, at 03:32, Simon Peyton Jones wrote:
Usually if I look at a type signature for a function and don't really understand it, I can rely on the type checker to ensure that it's only called in well-typed ways. I can also just look at the code for the function, and infer a type that is either the same or more general.
Note that we can still rely on the type checker to ensure that IntU is only used in well-typed ways. This is strictly about communicating semantics to other programmers (not suggesting that's less important).
Not so here. I boggled that we can write data IntU a b = IntU Int and not know whether it is lifted or not. That's about *semantics* and runtime behaviour, not mere static acceptance/rejection!
I suppose my base principle is: * If GHC can infer a type for a declaration * Then it's ok to omit or ignore the type/kind signature
That is, signatures (a) are needed when inference is Too Hard (b) restrict polymorphism. But they should not (c) change semantics.
Now I know that because of dark corners of the language, defaulting etc, the signature of a function *can* affect its semantics, but it is rare and very much a dark corner -- it's a wart. But this is right at the heart of what every data declaration means. I don't want to use one small wart to justify a much larger wartier wart.
Type classes (and in particular the monomorphism restriction) are a very prominent example of signatures affecting runtime semantics in fundamental ways. The monomorphism restriction itself is a wart, but the underlying difference between foo :: Num a => a and foo :: Int in terms of runtime representation and sharing are core to the language. And in my opinion, the type signature is *exactly* the right place to capture these semantic differences. We use types to communicate the externally-visible behavior of our programs: the number of arguments to a function and their types, effects incurred in the form of monads, etc. Why should liftedness and the implications for evaluation strategies be different? (In fact, as I've suggested before, I think we should go further and expose the strictness of function arguments in the type system, but that's a separate discussion.) --- On a semi-related note, this prompted me to go back and reread the proposal, and I'm not entirely clear on one point. In ``` data Foo :: TYPE (BoxedRep Unlifted) where MkFoo :: Int -> Foo ``` Foo is unlifted and arguments of type Foo will be evaluated strictly, but is MkFoo itself strict in its Int argument? The proposal doesn't seem to say, and I could see arguments in either direction.