• No keyword is sufficient to describe the full spectrum of levity-polymorphic data types
• Our language server is already smart enough to give the necessary info on hover, without even needing to navigate to the definition (where we would hope to see `unlifted` or a lack thereof). It also works with levity-polymorphism.

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.