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

2

Another very natural use case

elems :: forall {k1} (k2 :: k1 -> Type) (v :: k1 -> Type). DEnumMap k2 v -> [Some v]

from

3

Looks interesting, but once again the docs could/should be much better. There’s not a single example of a useful Enum1instance. And especially the more complex cases like differenceWithKey' are much too abstract.

4

The main purpose of data Some f is not strictly to hide types, but to minimise the hiding of types. Usually you want to be using the f that you would apply Some to, while the Some itself should be wrapped on only when needed and peeled off when it isn’t.

The reasons are simple enough:

  • Existentials are not first class in Haskell; we only support the operations on existential data types that can be typed with universals. Luckily this does include construction and pattern matching with case, but record accessors and updates are a no-go, as is pattern matching with let or where.

  • Hiding types grossly limits what can be done with data, and forces you to take up dynamic typing if you want to break those limits. Often the problems that are solved with existentials and dynamic typing can be better solved statically with heterogeneous data types. E.g. the common question of “how do I put different types in the same list” can be answered with [Some f], or you can use

    data Product f xs where
  Nil  :: Product f '[]
  (:~) :: f x -> Product f xs -> Product f (x:xs)

    instead with no loss of information.

The some library didn’t invent data Some f, they just captured the pattern, made sure it was a zero-cost abstraction, and provided some useful instances that the typical hand-rolled data Some f wouldn’t have.

5

Thanks, that’s helpful and clear enough. What’s missing in my view is a small set of canonical examples in which Some(Foo) is a compelling improvement over the well trodden:

{-# LANGUAGE GADTs, StandalongKindSignatures #-}

import Data.Kind (Type, Constraint)
import Data.Typeable (Typeable)

type Constrained :: Type -> Constraint
type Constrained a = (Typeable a) -- ... more constraints ...

data SomeFoo where
    SomeFoo :: (Constrained a) => a -> SomeFoo

with SomeException as a canonical example.

It is now clear that SNat n and similar indexed singleton types are fairly “natural” use-cases for Some(). What are some other patterns/use-cases where it is also beneficial? I’d hope to see the documentation address the topic of when the offered abstraction is applicable. With just the function signatures and short intro blurb it remains unclear when one should think about employing this machinery.