diff --git a/src/Nattish.hs b/src/Nattish.hs index 925f8b3..d6988de 100644 --- a/src/Nattish.hs +++ b/src/Nattish.hs @@ -18,6 +18,7 @@ module Nattish ( Nattish (Zeroy, Succy) ) where +import Foreign.Ptr (WordPtr) import Unsafe.Coerce (unsafeCoerce) #if __GLASGOW_HASKELL__ >= 800 import Data.Kind (Type) @@ -42,20 +43,20 @@ data Nattish :: k -> (k -> k) -> k -> * where Zeroy :: Nattish zero succ zero Succy :: !(Nattish zero succ n) -> Nattish zero succ (succ n) -toWord :: Nattish zero succ n -> Word -toWord = go 0 +toWordPtr :: Nattish zero succ n -> WordPtr +toWordPtr = go 0 where - go :: Word -> Nattish zero succ n -> Word + go :: WordPtr -> Nattish zero succ n -> WordPtr go !acc Zeroy = acc go !acc (Succy n) = go (acc + 1) n instance Show (Nattish zero succ n) where showsPrec p n = showParen (p > 10) $ - showString "Nattish " . showsPrec 11 (toWord n) + showString "Nattish " . showsPrec 11 (toWordPtr n) #else type Nattish :: forall k. k -> (k -> k) -> k -> Type -newtype Nattish zero succ n = Nattish Word +newtype Nattish zero succ n = Nattish WordPtr -- See [Note: WordPtr] deriving (Show) type role Nattish nominal nominal nominal @@ -81,4 +82,30 @@ pattern Succy n <- (check -> ResSucc n) {-# COMPLETE Zeroy, Succy #-} +-- [Note: WordPtr] +-- +-- Why WordPtr and not Word? We want to be extremely certain that it does not +-- overflow, because that would lead to a type safety problem (accessing a Succ +-- object as a value). At first, I thought we couldn't possibly have to worry +-- about that—after all, the Nattish never exceeds the *logarithm* of the queue +-- size. But then I remembered that it's possible to make quite absurdly large +-- queues by repeated concatenation. Imagine if a Word is 32 bits, but a +-- pointer is 64 bits. Then something like +-- +-- stimes (2^(2^33)) (singleton () ()) +-- +-- might actually be possible to construct in a relatively reasonable amount of +-- time and an achievable (if somewhat ridiculous) amount of memory. If this +-- were then traversed with traverseWithKeyU or foldMapWithKeyU from right to +-- left (using a lazy left fold, for example), we could overflow. Disaster! +-- Fortunately, we have WordPtr, which is equivalent to uintptr_t, and +-- therefore big enough to hold the logarithm of the size of any queue +-- represented in memory, even with maximal sharing. +-- +-- Now, according to a comment on +-- https://hackage.haskell.org/package/base-4.18.0.0/docs/src/Foreign.Ptr.html#WordPtr +-- GHC actually guarantees that a Word is the same size as a pointer, so we +-- actually *could* just use Word, but I think WordPtr makes it *utterly clear* +-- that we're safe here. + #endif