[ghc-steering-committee] Unlifted data types

Wed Aug 18 09:00:39 UTC 2021

Hello,

I am retired but still on the list so I read it sometimes :). (feel free to
unsubscribe me)

But since I was not sure where else to comment, I thought I'd chime in here
to say that I also find this pretty confusing.

My assumption/intuition is that 'data' should always introduce a lifted
type, and 'newtype' should have the same liftedness as its definition.   I
would much prefer that if we wanted to have some sort of unified 'data' we
should have a separate construct for it (e.g., like the proposed 'data
unlifted')

Iavor

On Wed, Aug 18, 2021, 11:33 Simon Peyton Jones via ghc-steering-committee <
ghc-steering-committee at haskell.org> wrote:

> I'm bothered both by distance, and the hidden-ness of Wombat, and (most
> fundamentally) by the fact that the data type declaration itself is not
> self-describing.  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.
>
> 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.
>
> I wish I had realised this at the time.  Apologies for that.
>
> Simon
>
> |  -----Original Message-----
> |  From: Eric Seidel <eric at seidel.io>
> |  Sent: 18 August 2021 03:57
> |  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
> |
> |  I think the distance between the `type IntU` and `data IntU` is the
> crux of
> |  the issue. If we were forced to keep the signature and declaration
> together,
> |  i.e.
> |
> |  ```
> |  type IntU :: Bool -> Wombat
> |  data IntU a b = IntU Int
> |  ```
> |
> |  I wouldn't be bothered by the distance from the definition of `Wombat`.
> |
> |  If I'm reading this code, and I already know what Wombat is, there's no
> |  problem. If I *don't* know what Wombat is, then I need to look up its
> |  definition anyway to make sense of IntU.
> |
> |  I've never been particularly fond of Haskell's tolerance for separating
> |  signatures and definitions. It has some practical uses -- notably in
> |  combination with -XCPP it makes it easy to ensure signatures are
> consistent
> |  across CPP branches -- but in general I think distance between
> signature and
> |  definition is a smell.
> |
> |  On Wed, Aug 11, 2021, at 03:48, Simon Peyton Jones via ghc-steering-
> |  committee wrote:
> |  >
> |  > I have just posted
> |  >
> |  <
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.co
> |  m%2Fghc-proposals%2Fghc-proposals%2Fpull%2F265%23issuecomment-
> |  896626642&data=04%7C01%7Csimonpj%40microsoft.com
> %7C9bd05c205b5d4757d4cd0
> |
> 8d961f3ea95%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637648524474023194%
> |
> 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi
> |
> LCJXVCI6Mn0%3D%7C3000&sdata=sr6XzIgF5CSnLyol8jSfjHToJpD86Q7bPHnKkaMjMgI%
> |  3D&reserved=0> this, about unlifted data types.  Yikes!
> |  > Simon
> |  >
> |  > *In accepted proposal #265 on Unlifted Datatypes
> |  > <
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgit
> |  > hub.com
> %2Fghc-proposals%2Fghc-proposals%2Fpull%2F265&data=04%7C01%
> |  > 7Csimonpj%40microsoft.com
> %7C9bd05c205b5d4757d4cd08d961f3ea95%7C72f988b
> |  > f86f141af91ab2d7cd011db47%7C1%7C0%7C637648524474033189%7CUnknown%7CTWF
> |  > pbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6M
> |  > n0%3D%7C3000&sdata=OWlj9RxqQfTBZcjp1QE5AUSSvnG%2By3wbuXL2VbqEGpw%3
> |  > D&reserved=0>* I have just realised that in this accepted, and
> |  > implemented proposal we have done something entirely new. Consider
> |  > this (from
> |  >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitl
> |  > ab.haskell.org
> %2Fghc%2Fghc%2F-%2Fissues%2F20204&data=04%7C01%7Csim
> |  > onpj%40microsoft.com
> %7C9bd05c205b5d4757d4cd08d961f3ea95%7C72f988bf86f1
> |  > 41af91ab2d7cd011db47%7C1%7C0%7C637648524474033189%7CUnknown%7CTWFpbGZs
> |  > b3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D
> |  > %7C3000&sdata=9SNn4GSIs%2Bd40SBQCEpYfYh7hO73XLoXY%2BWE2uuTg0k%3D&a
> |  > mp;reserved=0)
> |  >
> |  > `type IntU ::  Bool -> Wombat` ` ` `...LOTS OF CODE...` ` ` `data IntU
> |  > a b = IntU Int` ` ` `...MORE CODE...` ` ` `type Wombat =Type -> TYPE
> |  > UnliftedRep` The kind signature for `IntU` *completely changes the
> |  > semantics of the *`*data IntU*`* declaration*, and yet can be separate
> |  > from it. That is
> |  > new: generally, signatures can restrict the applicability of
> |  > something, but *don't change its semantics*. (Yes, with overlapping
> |  > instances, certainly incoherent instances, you could change semantics,
> |  > but the general principal holds.)
> |  >
> |  > Even if it is adjacent, the fact that it's unlifted is quite subtle...
> |  > you have to look to the right of the arrows, and then through the
> |  > distant (and perhaps imported) type synonym `Wombat`.
> |  >
> |  > I'm not very happy with a distant kind signature having such a
> |  > profound effect on the semantics of the data type. Indeed in my
> |  > comment above
> |  > <
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgit
> |  > hub.com
> %2Fghc-proposals%2Fghc-proposals%2Fpull%2F265%23issuecomment-52
> |  > 5705557&data=04%7C01%7Csimonpj%40microsoft.com
> %7C9bd05c205b5d4757d
> |  > 4cd08d961f3ea95%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637648524
> |  > 474033189%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIi
> |  > LCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=fB257%2Flsx8ucSnW%2Fgc
> |  > %2FPP50rVz4e2MJJCZgmc%2FB08jo%3D&reserved=0> I suggested a keyword
> |  >
> |  > `data unlifted IntU a b = IntU Int`
> |  > to signal that it's an *unlifted* data type. But then I went AWOL and
> |  > didn't pursue the matter. I don't know why I was so negligent.
> |  >
> |  > So this post is to ask: does anyone else think this is bizarre? I'm
> |  > inclined to make a proposal to add the keyword, but I thought I'd test
> |  > the waters first.
> |  >
> |  >
> |  > _______________________________________________
> |  > ghc-steering-committee mailing list
> |  > ghc-steering-committee at haskell.org
> |  >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail
> |  > .haskell.org
> %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&a
> |  > mp;data=04%7C01%7Csimonpj%40microsoft.com
> %7C9bd05c205b5d4757d4cd08d961
> |  > f3ea95%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637648524474033189
> |  > %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I
> |  > k1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=rwunJpephHqcWKNE%2F0IpMPS21mWSL
> |  > uyYr3V%2FVs6hfCo%3D&reserved=0
> |  >
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210818/2f56be77/attachment-0001.html>