Why no exposed `NullAddr#` literal?

Learn
1

Suppose that, switching on -XDataKinds -XGADTSyntax -XKindSignatures -XMagicHash -XUnliftedNewtypes and importing the relevant definitions from GHC.Exts, one creates the newtype

newtype MyAddr# :: TYPE AddrRep where
    WrapAddr# :: Addr# -> MyAddr#

(perhaps because they wish to signal interaction with a particular, trusted subset of foreign code—I think this is not a wholly unreasonable thing to do). Then they might like to declare something along the lines of

myNullAddr# :: MyAddr#
myNullAddr# = WrapAddr# nullAddr#

but this is of course disallowed, being an unlifted top-level binding. Fair enough!

The next best thing (actually, the ostensibly better thing, seeing as GHC already internally seems to treat nullAddr# as a literal—cf. LitNullAddr defined in compiler/GHC/Types/Literal.hs, but I am admittedly not very familiar with the GHC codebase) would be to be turn on -XPatternSynonyms and write

pattern MyNullAddr# :: MyAddr#
pattern MyNullAddr# = WrapAddr# _

where the hole is filled by some literal coinciding in value with nullAddr#. Indeed, were such a literal available, I don’t see why it wouldn’t make sense to deprecate the current nullAddr# in its favor, much like the old void# was deprecated in favor of (# #).

Unfortunately, such a literal does not seem to be available, neither via -XExtendedLiterals nor by using -XTemplateHaskell to splice some constructor of Lit from Language.Haskell.TH. (Per error GHC-65904, the interaction between the two extensions does not yet seem fully fleshed out.)

Is there any fundamental obstruction to GHC exposing such a literal? I tried searching for prior discussion about this matter but came up empty-handed.

Edit: I should add that the best workaround of which I’m currently aware is to use the standard top-level-unlifted-value binding trick

myNullAddr# :: (# #) -> MyAddr#
myNullAddr# = \ _ -> WrapAddr# nullAddr#

It might not be abominable, but it sure doesn’t spark any joy…

2

TIL pattern synonyms can be unlifted. But then a bidirectional pattern should work:

pattern MyNullAddr# :: MyAddr#
pattern MyNullAddr# <- ((\(WrapAddr# x) -> isTrue# (eqAddr# nullAddr# x)) -> True) where
  MyNullAddr# = WrapAddr# nullAddr#

I expected this:

myNullAddr# :: (() :: Constraint) => MyAddr#
myNullAddr# = WrapAddr# nullAddr#

(of course credit goes to @ekmett: unboxed/internal/Unboxed/Internal/Levitation.hs at main · ekmett/unboxed · GitHub)

Which makes is basically as easy to use as the pattern synonym.

The downside of this approach in general is that the value is not shared, but in this case it does not do any work so that shouldn’t be an issue. And the pattern synonym has the same downside.

3

I’m not sure it is fair, or at least there could in principle be an exception for values, and a newtype constructor applied to a value would be value. Maybe that adds too much extra complexity to be worth it.

Yeah, that’s what I’ve been using.

That’s a nice alternative!

4

I worked on this during my internship at Well-Typed. It is quite complicated. I managed to implement a basic form for unlifted top-level binding in Core (for optimizations), but that is stuck on supporting this in GHCi: !10841.

5

Awesome, thanks! This does spark joy.

My impression is that on the frontend (so more superficially than @jaror’s work above, but also more programmer-visibly) and with the exception of the nullAddr# issue, a statically-known fully evaluated unlifted value should be able to be built up from literals and constructors, hence should be bindable as an implicitly bidirectional unlifted pattern synonym. Language.Haskell.TH.Lit already represents literals of types Int#, Word#, Char#, Float#, and Double# (and hopefully once -XExtendedLiterals is fully supported by TemplateHaskell, also Int8#, Int16#, Int32#, Int64#, Word8#, Word16#, Word32#, and Word64#—maybe even eventually SIMD literals, although those aren’t currently supported by -XExtendedLiterals either), so in cases where the literal value is the result of a nontrivial computation one can do something like

{-# LANGUAGE Haskell2010 #-}

module MyInt.TH where

{- | Here because of the stage restriction -}
complicated :: Integer -> Integer
complicated = \ n -> product [ 1 .. n ]

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

{-# LANGUAGE Haskell2010
  , GADTSyntax
  , MagicHash
  , PatternSynonyms
  , UnliftedNewtypes
  , TemplateHaskell
#-}

module MyInt where

import GHC.Exts
import Language.Haskell.TH
import MyInt.TH

newtype MyInt# where
    WrapInt# :: Int# -> MyInt#

data MyInt where
    MyI# :: Int# -> MyInt

{- |  Binds 'WrapInt# 2432902008176640000#' as a pattern -}
$(pure $
    let nm = mkName "Fac20Int#"
        n = complicated 20
    in  [ PatSynD
            ( nm )
            ( PrefixPatSyn [ ] )
            ( ImplBidir )
            ( ConP
                ( 'WrapInt# )
                [ ]
                [ LitP ( IntPrimL n ) ] )
        , PatSynSigD
            ( nm )
            ( ConT ''MyInt# ) ]
  )

{- |  Binds 'MyI# 2432902008176640000#' as a value -}
fac20Int :: MyInt
fac20Int = $(pure $
    let n = complicated 20
    in  AppE
          ( ConE 'MyI# )
          ( LitE ( IntPrimL n ) )
  )