"some" library intended/compelling use-cases?

Learn
1

In a thread about working with bounded type-level naturals, it was suggested by @Leary that I take a look at the some library (Data.Some.Newtype, …).

I have read the Haddock page, and the Github tutorial, but I’m still not entirely clear on the use-cases for which the some library is most appropriate.

It does look like some can be put to good use to existentially wrap bounded SNat singletons as efficient newtypes:

Example code 
{-# LANGUAGE
    GHC2024
  , BlockArguments
  , PatternSynonyms
  , UnboxedTuples
  , ViewPatterns
  #-}

module Nat16
    ( type Nat16
    , SNat16(..)
    -- , pattern SNat16
    , natToWord16
    , wordToNat16
    ) where

import Data.Kind (Type, Constraint)
import Data.Typeable ((:~:)(..))
import Data.Word (Word16)
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeNats ( Natural, Nat, SNat, pattern SNat, CmpNat
                    , fromSNat, natVal, withSomeSNat)
import Data.Some.Newtype (Some(..), mkSome, withSome)

type Nat16 :: Nat -> Constraint
type Nat16 n = CmpNat n 65536 ~ LT

type role SNat16 nominal
type SNat16 :: Nat -> Type
newtype SNat16 n = UnsafeSNat16 { unSNat16 :: SNat n }

view16 :: forall (n :: Nat). SNat16 n
       -> (# CmpNat n 65536 :~: LT, SNat n #)
view16 !sn = (# unsafeCoerce (Refl @LT), unSNat16 sn #)

pattern SNat16 :: () => Nat16 (n :: Nat) => SNat n -> SNat16 n
pattern SNat16 x <- (view16 -> (# Refl, x #))
  where SNat16 x = UnsafeSNat16 x

natToWord16 :: forall (n :: Nat). SNat16 n -> Word16
natToWord16 (SNat16 x) = fromIntegral @Natural @Word16 $ fromSNat x

wordToNat16 :: Word16 -> Some(SNat16)
wordToNat16 w = withSomeSNat (fromIntegral w) \n -> case magic n of
  Refl -> Some (SNat16 n)
 where
  magic :: SNat n -> CmpNat n 65536 :~: LT
  magic _ = unsafeCoerce (Refl @LT)

With that code we can do things like:

λ> :set -XTypeApplications -XDataKinds
λ> import GHC.TypeNats (fromSNat, natSing)
λ> x = mkSome (SNat16 (natSing @12345))
λ> withSome x natToWord16
12345
λ> y = wordToNat16 12345
λ> withSome y natToWord16 
12345
λ> f :: Some (SNat16) -> Word16; f (Some (SNat16 y)) = fromIntegral $ fromSNat y
λ> f x
12345
λ> case x of { Some (SNat16 y) -> fromSNat y } :: Natural
12345

Though, FWIW, and for reasons I don’t understand the naïve variant below that omits the explicit :: Natural type in that last case expression fails to type check in ghci:

Error sans explicit type 
λ> case x of { Some (SNat16 y) -> fromSNat y } 
<interactive>:17:32: error: [GHC-25897]
    • Could not deduce ‘p ~ Natural’
      from the context: Nat16 a
        bound by a pattern with pattern synonym:
                   SNat16 :: forall (n :: Nat). () => Nat16 n => SNat n -> SNat16 n,
                 in a case alternative
        at <interactive>:17:19-26
      ‘p’ is a rigid type variable bound by
        the inferred type of it :: p
        at <interactive>:17:1-43
    • In the expression: fromSNat y
      In a case alternative: Some (SNat16 y) -> fromSNat y
      In the expression: case x of Some (SNat16 y) -> fromSNat y
    • Relevant bindings include it :: p (bound at <interactive>:17:1)
    Suggested fix: Consider giving ‘it’ a type signature

With all that out of the way, my question is what else is this machinery good for? I have a library in which a few type classes (say Foo, Bar, …) are associated with existential wrappers:

class (Show a, Eq a, Ord a, ..., Typeable a) => Foo a where ...
data SomeFoo where SomeFoo :: Foo a => a -> SomeFoo
fromSomeFoo :: Foo a => SomeFoo -> Maybe a
fromFoo (SomeFoo x) = cast x
instance Eq SomeFoo where ...
instance Ord SomeFoo where ...
instance Show SomeFoo where ...
...

along with various functions that work with SomeFoo wrapped values, including heterogenous comparison for equality and heterogenous order (first by a Word16 value associated with each type, then by content).

In these cases, it is not clear to me how some would be useful. I don’t see a way to employ newtypes here, because unlike the case with SNat16 where the Nat16 constraint is implied by construction, and can be synthesised when pattern matching, capturing the typeclass dictionary along with each value seems unavoidable when existentially wrapping a typeclass. So there’s no obvious gain in the efficiency of the representation.

If not for avoiding double-wrapping the existentially quantified values, what benefit would I get from some? I can write:

type Known :: (Type -> Constraint) -> Type
data Known cls where
    Known :: forall (cls :: Type -> Constraint) (a :: Type).
             (cls a, Typeable a) => a -> Known cls

fromKnown :: forall (cls :: Type -> Constraint) (a :: Type).
          (cls a, Typeable a)  => Known cls -> Maybe a
fromKnown (Known y) = cast y

withKnown :: forall (cls :: Type -> Constraint) r.
          Known cls -> (forall a. (cls a, Typeable a) => a -> r) -> r
withKnown (Known x) f =  f x

as an attempt to generalise the pattern, and I guess since all the cases of interest happen to be subclasses of Eq and Show, I can write somewhat more general instances of these. But already Ord presents a difficulty since I want to order by the Word16 index of the value types, which would require abstracting that property to a superclass (currently separately defined directly defined as a newtype around Word16 in each class).

And of course, that specific project aside, more generally, what are the use-cases in which some provides a clear benefit over custom per tag existential wrappers?

1 Like