Allow unconstrained existential contexts in newtypes

changed weight to 5

added Tfeature request Trac import labels

Why is this useful?

In GHC it's disallowed because an existential is modeled as a data constructor with a field that captures the type in the same way that it captures the value fields. But since the representation of a newtype is supposed to be the same as the representation of the (single) field, you can't do that.

So, it'd be quite difficult to make GHC do this (i.e. it'd affect GHC's typed intermediate language); and I can't see any useful applications.

Simon

closed

Please reopen this ticket if you have a useful application for it.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

Trac metadata

Trac field	Value
Architecture	Unknown → Unknown/Multiple

Trac metadata

Trac field	Value
Operating system	Unknown → Unknown/Multiple

reopened

This would actually be a useful feature with GADTs, since matching on one can tell us what the existential field was, even without storing a context for it in our newtype.

It's definitely not essential to anything I'm doing, but perhaps the recent changes to GHC since the last time people looked at this ticket make this feature easier to implement?

Trac metadata

Trac field	Value
TypeOfFailure	- → OtherFailure
Resolution	ResolvedWon'tFix → Unresolved

Okay, so this ticket-revival stemmed from a question I asked on IRC, so here's what I wanted to use this for.

class (Monad (m context)) => MonadContext m context where
  getContext
    :: m context context
  withContext
    :: MonadContext m context'
    => context'
    -> m context' a
    -> m context a


data FallibleContextualOperation failure context a =
  FallibleContextualOperation {
      fallibleContextualOperationAction :: context -> IO (Either failure a)
    }


instance Monad (FallibleContextualOperation failure context) where
  return a = FallibleContextualOperation {
                 fallibleContextualOperationAction = \_ -> return $ Right a
               }
  x >>= f =
    FallibleContextualOperation {
        fallibleContextualOperationAction = \context -> do
          v <- fallibleContextualOperationAction x context
          case v of
            failure@(Left _) -> return failure
            Right y -> fallibleContextualOperationAction (f y) context
      }


instance MonadContext (FallibleContextualOperation failure) context where
  getContext =
    FallibleContextualOperation {
        fallibleContextualOperationAction =
          \context -> return $ Right context
      }
  withContext context' x =
    FallibleContextualOperation {
        fallibleContextualOperationAction =
          \context -> fallibleContextualOperationAction x context'
      }

I can provide more details of what this is motivated by upon request, but basically, I want to have my "master implementation" of this class based on FallibleContextualOperation, and then I want to make two types that get that behavior for free:

newtype Serialization context a =
  forall backend
  . Serialization {
        serializationOperation :: FallibleContextualOperation
                                    (SerializationFailure backend)
                                    context
                                    a
      }
deriving instance Monad (Serialization context)
deriving instance MonadContext Serialization context


newtype Deserialization context a =
  forall backend
  . Deserialization {
        deserializationOperation :: FallibleContextualOperation
                                    (DeserializationFailure backend)
                                    context
                                    a
      }
deriving instance Monad (Deserialization context)
deriving instance MonadContext Deserialization context

The point is so that I can then do:

class Serializable context a where
  serialize :: Serialization context a
  deserialize :: Deserialization context a

.. and write many instances of this, elsewhere in my program, which don't need to know or care about the fact that there are two backend types (ByteStrings and open files), or any of this other nasty plumbing detail.

I don't know if this is sufficient motivation to justify the work the ticket is requesting, since I don't know just how much work it is. But it's presented here for everyone's edification. :)

I also have run into cases where I'd like to make a "trivial" GADT into a newtype. In particular, when programming in a "dependent"-like style using GADTs to encode the tags of dependent sums, it's often nice to have a wrapper that does nothing but alter the type index - a very general example would be "data Map f t a where Map :: t a -> Map f t (f a)" - which allows transforming the last type parameter by an arbitrary type-level function. Most of the time this usage could be avoided by including 'f' in the dependent sum type itself, but that complicates other things and even then I've found you occasionally want to modify the types of tags.

Another situation where I've wanted something like this to forget a phantom type - and I've seen the same pattern in other people's code I've read on hackage.

There is a different possible resolution to this request, which would probably be more work but not break portability - guarantee that any "data" declaration satisfying certain criteria will be compiled to a newtype-like representation. Here's my stab at that set of criteria:

Only one constructor
Only one field with nonzero width in that constructor (counting constraints as fields)
That field is marked strict

It seems like those requirements should be sufficient to justify special-case handling to compile them to something effectively the same as a newtype. Or if some mechanism already causes this to effectively by the case, then I'd be happy with that being documented and test-cases added to ensure it continues to be a stated goal to cover situations like these.

changed milestone to %7.6.1

Anything involving existentials is going to be hard to implement using newtype directly. But as 'mokus' says, it might be possible to make a guarantee, right in the code generator, that certain sorts of data types do not allocate a box. The conditions are, I think, very nearly as 'mokus' says:

Only one constructor
Only one field with nonzero width in that constructor (counting constraints as fields)
That field is marked strict
That field has a boxed (or polymorphic) type

I think this'd be do-able. The question is how important it is in practice; it's one more thing to maintain.

Simon

changed milestone to %7.6.2

Just a minor bump on this. The more fancy GADT and Poly/DataKind programming I do, the more this bothers me. It seems like a real pity to be penalized (with an extra box) for choosing to encode invariants in indices, especially with all the new delicious features GHC has been getting recently.

To be clear about what I'm looking for:

data IntList where
  Nil :: IntList
  Cons :: Int -> IntList -> IntList

data Nat = Z | S Nat

data IntVec :: Nat -> * where
   NilV :: IntVec Z
   ConsV :: Int -> IntVec n -> IntVec (S n)

-- N.B: not data
newtype Exists (f :: k -> *) = forall x. Exists (f x)

type IntVecList = Exists IntVec

-- IntList and IntVecList should be isomorphic! If Exists can't be a newtype, I have to pay a penalty for adding indices to my type :(

Replying to [ticket:1965#comment:84463 pumpkin]:

To be clear about what I'm looking for:

Yes, I always wondered how existentially quantifying over a type constructor with non-* domain kinds can ever necessitate extra information at runtime. I fully support the reopen proposal because of data Hidden :: k -> * where Hide :: t a -> Hidden t wants to be a newtype.

changed milestone to %7.10.1

Moving to 7.10.1.

Allow unconstrained existential contexts in newtypes

Child items ...

Activity

Allow unconstrained existential contexts in newtypes

Relates to

Activity