[ghc-steering-committee] Unlifted data types

[Simon Peyton Jones]

|  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?

We use them to *communicate* behaviour, but not to *specify* behaviour.  That is done by the definition of the function itself.

I'm keen to hear from other members of the committee.

Maybe I should make a proposal, to seek broader input.

Simon

|  -----Original Message-----
|  From: Eric Seidel <eric at seidel.io>
|  Sent: 18 August 2021 14:33
|  To: Simon Peyton Jones <simonpj at microsoft.com>; ghc-steering-
|  committee at haskell.org; Sebastian Graf <sgraf1337 at gmail.com>
|  Subject: Re: [ghc-steering-committee] Unlifted data types
|  
|  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.