Hi,
FWIW, I'm neither a proponent of adding an unlifted keyword or modifier,
nor a strong opponent.
I just want to make aware of the point I raise in
https://github.com/ghc-proposals/ghc-proposals/pull/265#issuecomment-9019041...,
namely that
No keyword is sufficient to describe the full spectrum of
levity-polymorphic data typesOur 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.
Cheers,
Sebastian
------ Originalnachricht ------
Von: "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.