[ghc-steering-committee] Unlifted data types

[Eric Seidel]

On Thu, Aug 19, 2021, at 06:14, Simon Peyton Jones wrote:
> |  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 disagree, types are a great specification language. The whole point of advanced
type system features is to enhance the specification language so we can
specify more interesting properties. 

Often, we do this so that the type checker can *verify* our code, but there are plenty
of cases where we use types to *drive code generation*. Consider GHC.Generics.
We can write a highly-polymorphic JSON serialization function

  gToJSON :: Generic a => a -> JSON

which we can then instantiate at different types, e.g.

  data Foo
  fooToJSON :: Foo -> JSON
  fooToJSON = gToJSON

  data Bar
  barToJSON :: Bar -> JSON
  barToJSON = gToJSON

fooToJSON and barToJSON have the exact same definition, but very different
semantics. Their complete semantics depends on *both* their definition *and*
their type signatures.

I think the deeper point here is that Haskell's dynamic semantics depends on
its static semantics. We can't evaluate a Haskell program without knowing the
types involved.