haskellari/some

Existential type.

some

This library defines several versions of an existential type 'Some', which works like this datastructure:

data Some f where
    Some :: f a -> Some f

and operations to work with it.

However, due to GHC issue #1965, the direct implementation of this datastructure is less efficient than it could be. As a result, this library uses a more complex approach that implements it as a newtype, so there's no runtime overhead associated with wrapping and unwrapping Some values.

To use the recommended implementation, import Data.Some. If you need to ensure that you are definitely using the newtype implementation, import Data.Some.Newtype. By default, these are the same, but this can be changed via a Cabal flag.

some's Issues

Support for `exists a b. Either a b` and `exists a. Either a Int`

Some can only express exists a. Either Int a, but not the other two (at least not very easily).

I stumbled upon some old code of mine which supports all three and more, using two transformers I call SomeT and ThisT:

• exists a. Either Int a ~ Some Either
• exists a b. Either a b ~ SomeT Some Either
• exists a. Either a Int ~ SomeT (This Int) Either

I thought you might want to steal those ideas to make this package useful in more cases. I bet it would be easy to implement a third transformer which would support constraints too:

• exists a. Show a => Either a Int ~ ConstrainedT Show (This Int) Either

Documenting gread / GReadS

I think it would make things clearer to document gread as being in continuation-passing style. I literally only just realised this now, because it was similar to some other code I wrote today. And now I finally understand that type GReadS t [*] is something that consumes the continuation, which is vital to understanding how to implement an instance of GRead. (Previously I was just copy-pasting the existing instances and fiddling around until the type errors went away.)

[*] Actually this refers to the previous implementation of GReadResult, today's implementation avoids CPS and is a bit clearer, however the docstring still refers to the old CPS implementation which could still confuse users.

gread is still in CPS though and should be documented as such. Also, an alternative offering which may be more convenient for some users would be:

{-# LANGUAGE QuantifiedConstraints #-}

newtype SomeCxt c = SomeCxt { unCxt :: forall v. c v => v }

greadC
  :: (GRead t, forall a. c (t a))
  => Proxy t
  -> String
  -> SomeCxt c
greadC = ...

This relies on there existing an appropriate instance that applies to all a, which may not always exist, but if it does then it could be more convenient to use than passing in a continuation.

GEq (Product f g) instance requires more than needed.

Consider

data Tag a where
  TagInt :: Tag Int
  TagBool :: Tag Bool

then we can implement a function of type

geqEx :: Product Tag [] a -> Product Tag b -> Maybe (a :~: b)

working as geq. But that Product doesn't have GEq instance.

We can either document this, or remove the instance for the same reason as there isn't TestEquality (Product f g) as in "we don't want to chose which way to bias the instance.

Allow GHC-9.4?

GShow is the same as Show1 from base

Unlike the other classes, there are no proof obligations that matching on the indices can satisfy. It's therefore not a "GADT class" as I understand them.

edit I am wrong, GShow t is not the same as Show1 t it is the same as forall a. Show (t a). Do not, reader, that this holds in general: the Foo1 classes are not completely obviated by quantified constraints.

Data.Some.Church does not export withSome

Port "Implement GRead using an existential"

from obsidiansystems/dependent-sum#13

Port "Monoid newtypes"

from obsidiansystems/dependent-sum#37

Tag 1.0.0.3 missing

Please create it.

Port Data.Some.Lazy

from obsidiansystems/dependent-sum#35

Better docs to distinguish from TestEquality

See haskell/core-libraries-committee#21. The important thing about GEq is that it is doing term and type equality. Likewise GCompare is doing value ordering.

This will be easier after #21, as the quantified constraints bring the plain H98 classes "in scope", so we can less awkwardly write laws clarifying the situation.

(That PR is in turn blocked on haskell/core-libraries-committee#10, but the current plain H98 class instances for Sum and Product are too pointlessly restrictive for this to work.)

Make it compile with ghc-9.8

Only dependency bounds need to be changed:

diff --git a/some.cabal b/some.cabal
index ff723ed..2d047a3 100644
--- a/some.cabal
+++ b/some.cabal
@@ -61,8 +61,8 @@ library
 
   other-modules:    Data.GADT.Internal
   build-depends:
-      base     >=4.12    && <4.19
-    , deepseq  >=1.4.4.0 && <1.5
+      base     >=4.12    && <4.21
+    , deepseq  >=1.4.4.0 && <1.6
 
   if impl(ghc >=9.0)
     -- these flags may abort compilation with GHC-8.10

TestEquality

What is the/is there a difference between GEq and TestEquality? I see you use it internally, is it just to avoid orphans?