[ghc-steering-committee] Unlifted data types

[Eric Seidel]

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.