Opened 9 years ago
Last modified 7 weeks ago
#1965 new feature request
Allow unconstrained existential contexts in newtypes
Reported by: | guest | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 6.8.1 |
Keywords: | Cc: | pumpkingod@…, ireney.knapp@…, mokus@…, jake.mcarthur@…, sweirich@…, oerjan, dfeuer, RyanGlScott, osa1 | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by simonpj)
Declarations like
newtype Bar = forall a. Bar (Foo a)
ought to be allowed so long as no typeclass constraints are added. Right now, this requires data rather than newtype.
The wiki page NewtypeOptimizationForGADTS summarises the proposal
Change History (35)
comment:1 Changed 9 years ago by simonpj
comment:2 Changed 9 years ago by igloo
- Resolution set to wontfix
- Status changed from new to closed
Please reopen this ticket if you have a useful application for it.
comment:3 Changed 8 years ago by simonmar
- Architecture changed from Unknown to Unknown/Multiple
comment:4 Changed 8 years ago by simonmar
- Operating System changed from Unknown to Unknown/Multiple
comment:5 Changed 5 years ago by pumpkin
- Cc pumpkingod@… added
- Resolution wontfix deleted
- Status changed from closed to new
- Type of failure set to None/Unknown
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?
comment:6 Changed 5 years ago by Irene
- Cc ireney.knapp@… added
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. :)
comment:7 Changed 5 years ago by mokus
- Cc mokus@… added
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.
comment:8 Changed 5 years ago by igloo
- Milestone set to 7.6.1
comment:9 follow-ups: ↓ 19 ↓ 28 Changed 5 years ago by simonpj
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
comment:10 Changed 4 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:11 Changed 2 years ago by pumpkin
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.
comment:12 Changed 2 years ago by jmcarthur
- Cc jake.mcarthur@… added
comment:13 follow-up: ↓ 14 Changed 2 years ago by pumpkin
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 :(
comment:14 in reply to: ↑ 13 Changed 2 years ago by heisenbug
Replying to 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.
comment:15 Changed 2 years ago by thoughtpolice
- Milestone changed from 7.6.2 to 7.10.1
Moving to 7.10.1.
comment:16 Changed 2 years ago by pumpkin
Dan Doel pointed out that as useful as this could be, it would allow this fairly odd use case:
data Nat = Z | S Nat data Fin n where Zero :: Fin (S n) Suc :: Fin n -> Fin (S n) newtype SomeFin where SomeFin :: Fin n -> SomeFin suc :: SomeFin -> SomeFin suc (SomeFin n) = SomeFin (Suc n) inf :: SomeFin inf = suc inf
Which leads to inf containing a Fin whose existential index can't actually be any valid (finite) type. Fin thus becomes a bit of a misnomer in this context, since it's not finite. Making SomeFin into data rather than newtype fixes the problem by making inf into a bottom.
comment:17 Changed 2 years ago by sweirich
- Cc sweirich@… added
comment:18 Changed 22 months ago by thoughtpolice
- Milestone changed from 7.10.1 to 7.12.1
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
comment:19 in reply to: ↑ 9 Changed 20 months ago by oerjan
Replying to simonpj:
- Only one field with nonzero width in that constructor (counting constraints as fields)
I'd like to point out (as may already have been indented), that read literally, this should include things like
data Dict :: Constraint -> * where Dict :: a => Dict a
from the constraints package.
comment:20 Changed 20 months ago by oerjan
- Cc oerjan added
comment:21 Changed 14 months ago by thoughtpolice
- Milestone changed from 7.12.1 to 8.0.1
Milestone renamed
comment:22 Changed 9 months ago by thomie
- Milestone 8.0.1 deleted
comment:23 Changed 7 months ago by ryantrinkle
Use cases like pumpkin's Some have been cropping up more and more frequently for me; I think this would be pretty useful.
Edit: here's a link to an actual Some in the wild: https://hackage.haskell.org/package/dependent-map-0.2.1.0/docs/Data-Dependent-Map.html#t:Some
comment:24 Changed 7 months ago by simonpj
But the Some at the link is this:
data Some tag :: (k -> *) -> * where This :: !(tag t) -> Some k tag
There's no reason why this can't be a newtype today, is there?
So it doesn't look relevant to this ticket. (Except I suppose that if comment:9 was implemented, it'd be efficient already.)
comment:25 Changed 7 months ago by ryantrinkle
Hmm, when I try to convert it to a newtype, like this:
newtype Some tag = forall t. This (tag t)
I get this error:
src/Data/Some.hs:17:20: A newtype constructor cannot have existential type variables This :: forall (k :: BOX) (tag :: k -> *) (t :: k). tag t -> Some tag In the definition of data constructor ‘This’ In the newtype declaration for ‘Some’
Is there a different way of converting it to a newtype that I'm overlooking?
Here's a link to the original source of that Some: https://hackage.haskell.org/package/dependent-sum-0.3.2.1/docs/src/Data-Some.html#Some . The Hoogle output is more confusing to me than the original.
comment:26 Changed 7 months ago by simonpj
Oh sorry, my fault. I stupidly missed the fact that t was existential. Just ignore comment:24. So this is an example of the ticket.
Back to comment:9 then, I think.
comment:27 Changed 5 months ago by dfeuer
- Cc dfeuer added
comment:28 in reply to: ↑ 9 Changed 5 months ago by dfeuer
Replying to simonpj:
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.
I would like to have something like this very much! Among other things, it's one possible way to make IntMap nicer. One potential extension: I think constraints only need to count as fields if any of them are classes that have methods, or whose superclasses have methods. In particular, it could be very useful to have equality constraints involving type families.
comment:29 Changed 5 months ago by dfeuer
I've started a wiki page to give examples of why we want this.
comment:30 Changed 5 months ago by simonpj
- Description modified (diff)
comment:31 follow-up: ↓ 33 Changed 4 months ago by Iceland_jack
Possible example from A Foundation for GADTs and Inductive Families, encoding GADTs as left Kan extensions can be reworked to:
data N = O | S N data LanO j where LanO :: LanO (S i) data LanS j where LanS :: Fin i -> LanS (S i)
Fin defined as
data Fin a where FinO :: LanO i -> Fin i FinS :: LanS i -> Fin i pattern FinO' = FinO LanO pattern FinS' n = FinS (LanS n)
Do LanO, LanS satisfy the conditions to be newtypes?
Original code
data Fin :: * -> * where NZero :: Lan S One j -> Fin j NSucc :: Lan S Fin j -> Fin j data One j = One data Lan h _X j = forall i. Lan (Eql j (h i), _X i) data Eql i j where Refl :: Eql i i
comment:32 Changed 2 months ago by RyanGlScott
- Cc RyanGlScott added
comment:33 in reply to: ↑ 31 Changed 2 months ago by dfeuer
Replying to Iceland_jack:
data LanO j where LanO :: LanO (S i) data LanS j where LanS :: Fin i -> LanS (S i)Fin defined as
Do LanO, LanS satisfy the conditions to be newtypes?
LanO does not, because its constructor takes no arguments. But that's perfectly fine; there's only one LanO value anyway. LanS does not either, because its constructor is lazy. If you wrote LanS :: !(Fin i) -> LanS (S i) then it would satisfy the conditions.
comment:34 Changed 2 months ago by oerjan
LanO might, however, be a candidate for being zero width when in a strict field, which could help other types satisfy the newtype condition.
comment:35 Changed 7 weeks ago by osa1
- Cc osa1 added
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