[ghc-steering-committee] Unlifted data types

Wed Aug 18 08:32:40 UTC 2021

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
|  >