[ghc-steering-committee] Unlifted data types

[Sebastian Graf]

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-901904173, 
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" <eric at seidel.io>
An: "Simon Peyton Jones" <simonpj at microsoft.com>; 
"ghc-steering-committee at haskell.org" 
<ghc-steering-committee at haskell.org>; "Sebastian Graf" 
<sgraf1337 at gmail.com>
Gesendet: 19.08.2021 21:16:39
Betreff: Re: [ghc-steering-committee] Unlifted data types

>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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210819/48c74fe7/attachment.html>