#8026 closed feature request (wontfix)
DatatypeContexts should be fixed, not deprecated
Reported by: | gidyn | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.6.3 |
Keywords: | Cc: | gideon@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
Description
To borrow an example from the prime wiki page, the following code fails to compile:
data Eq a => Foo a = Foo a isEq :: Foo a -> Foo a -> Bool isEq (Foo x) (Foo y) = x == y
We have to tell the compiler that Eq a => Foo a in isEq, even though this is part of the data type's definition. Furthermore,
getVal :: Foo a -> a getVal (Foo x) = x
will also fail because of the missing constraint, even though it isn't used in the function's definition.
Rather than just deprecating the DatatypeContexts extension, it should be "fixed" to remember the context wherever the data type is used.
Change History (24)
comment:1 follow-up: ↓ 5 Changed 21 months ago by simonpj
- difficulty set to Unknown
- Resolution set to wontfix
- Status changed from new to closed
comment:2 Changed 21 months ago by gidyn
- Resolution wontfix deleted
- Status changed from closed to new
This only works when pattern matching on the constructor, and GADTs are no different to classical data types for this. Functions which uses a Foo without pattern matching will require a redundant type context in either case.
comment:3 Changed 21 months ago by gidyn
This might be a better example:
data Eq a => Pair a = Pair {x::a, y::a} equal :: Pair a -> Bool equal pair = (x pair) == (y pair)
Is there any way you can avoid a redundant Eq a => in the definition of equal, without adding a redundant pattern match?
comment:4 Changed 21 months ago by gidyn
- Cc gideon@… added
comment:5 in reply to: ↑ 1 Changed 21 months ago by gidyn
Replying to simonpj:
You may want to make suggesitons to the Haskell Prime group
Haskell Prime expect extensions to be implemented in a compiler first, so that would have to come if/after it's been implemented here.
comment:6 Changed 21 months ago by isaacdupree
In your example, do any of these three expressions typecheck? (note: functions are not in Eq)
Pair id id undefined :: Pair (()->()) equal undefined
comment:7 follow-up: ↓ 8 Changed 21 months ago by monoidal
@gidyn: What would the type of x be in your example?
You probably want x to introduce the validity of constraint Eq a. So the type would be somewhat dual to Eq a => Pair a -> a: using it would prove the constraint Eq a, rather than requiring evidence for the constraint. Something like Pair a -> (Eq a; a).
It seems to me this change would complicate the type system a lot, while the benefits are rather doubtful.
comment:8 in reply to: ↑ 7 Changed 21 months ago by gidyn
Replying to monoidal:
The generated getter should have type Eq a => Pair a -> a - nothing complicated about it, unless I missed your point.
comment:9 follow-up: ↓ 11 Changed 21 months ago by monoidal
@gidyn: You probably meant x :: Eq a => Pair a -> a.
Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.
comment:10 follow-up: ↓ 12 Changed 21 months ago by monoidal
- Resolution set to wontfix
- Status changed from new to closed
As far as I understand, the proposal is not sound.
comment:11 in reply to: ↑ 9 Changed 21 months ago by gidyn
Replying to monoidal:
Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.
The use of DatatypeContexts would make this equivalent to equal (undefined :: Eq ? => Pair (() -> ())), so the type he's asking about couldn't (and shouldn't) be constructed when using this extension.
Excluding some nefarious uses of undefined seems like a reasonable price to pay for turning on a useful extension.
comment:12 in reply to: ↑ 10 Changed 21 months ago by gidyn
Replying to monoidal:
As far as I understand, the proposal is not sound.
I think that there is some misunderstanding here. This is not proposing to change the actual type system, just that the DatatypeContexts extension should enable automatic context inference. This is similar to SPJ's (...) => proposal, but tied to the extension which makes requires it, and without the syntactic noise.
comment:13 Changed 6 months ago by yokto
I like the idea of fixing this too. The main Idea would be to hide Contexts from sight. As an example of how this could be useful consider Num were a newtype instead of a type class
newtype (Num n) => Num' n = Num' n type Int' = Num' Int (+) :: Num' n -> Num' n -> Num' n
This would mean you could actually make instances
instance SomeClass (Num' n)
that don't conflict with all other instances
instance (Num n) => SomeClass n instance SomeClass Char
crash
and even if you enable ugly extensions like UndecidableInstances this can not fix your problems if you want to use type families or functional dependencies.
you can not make an instance
class SomeClass a b | a -> b instance (Num n) => SomeClass n b
without immediately blocking all other possible Instances.
Maybe these DatatypeContexts based containers are a bit less flexible than common classes in that they don't mix, but if you know they don't have to mix it makes instances a lot easier and safer.
of course you can always add the context explicitly but it would be nice if ghc infer them. As gidyn said I don't think this would change the type system overly much. You would just get contexts that don't need not be explicitly stated. Every time you do context checks you can easily derive them from the type.
comment:14 Changed 6 months ago by gidyn
- Resolution wontfix deleted
- Status changed from closed to new
See also Partial Type Signatures.
comment:15 Changed 6 months ago by goldfire
It seems that those of us who have hacked on GHC in the past have a hard time understanding this proposal -- which, to me, looks either unsound (if implemented simply) or very complicated (adding the ability to return a constraint). If you want this to be considered, please write up a wiki page with detailed examples and types. Also, suggest how this feature should be implemented, in terms of a translation to GHC's core language. It currently all seems a little magical. Thanks!
comment:16 Changed 6 months ago by gidyn
Consider the first example
data Eq a => Foo a = Foo a isEq :: Foo a -> Foo a -> Bool isEq (Foo x) (Foo y) = x == y
This won't compile, because isEq is missing Eq a =>. However, if we miss out the type signature altogether, GHC will correctly infer it. With Partial Type Signatures, we can also write
isEq :: _ => Foo a -> Foo a -> Bool
and GHC will infer the constraint.
This proposal is requesting that whenever DatatypeContexts has been turned on, and a data type appears in a type signature, GHC will automatically infer the data type's context in the same way as it would for an extra-constraints wildcard.
It is different to extra-constraints wildcards in that:
- no explicit syntax is needed, other than DatatypeContexts
- the only constraint which can be added by inference is one that was given in the data type declaration.
Is that clearer?
comment:17 Changed 6 months ago by gidyn
To emphasise: this proposal is not proposing a change to the type system. It is, similar to Partial Type Signatures, proposing a new use for GHC's existing type inference capabilities.
comment:18 Changed 6 months ago by goldfire
This proposal does propose a change to the type system, as it proposes a change to the set of well-typed programs. The same is true of partial type signatures. Type inference is an algorithm that implements a way to enforce the constraints of a type system.
Your example is clear for that simple situation. But, Haskell's type system is not that simple! For example:
data Eq a => HasEq a = MkHasEq a deriving Typeable data Show a => HasShow a = MkHasShow a a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool a (Just x) (Just y) = x == y a _ _ = Nothing b :: Either (HasEq a) (HasShow a) -> String -- what constraints are used here??? b (Left x) = show (x == x) b (Right x) = show x c :: Proxy (HasEq a) -> () -- what constraints are used here??? c _ = () data Dynamic = forall a. Typeable a => MkDyn a d :: Dynamic -> Maybe Bool d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z) -- where does the Eq constraint come from?? d _ = Nothing
Your examples seem to address specific, easy cases. But, we need to consider all the wide range of compositions with other Haskell features!
comment:19 Changed 6 months ago by yokto
Ok I'm not an expert in type theory or anything but let me try to explain based on your example. I don't know how this relates to type theory or if it is sound but it covers all the cases I could think of.
data Eq a => HasEq a = MkHasEq a
Deriving Types
How can you get a value of type HasEq a.
- Using a Constructor (also in a pattern): Use the same trick as with GADTs? Just make the type signature of the constructor (Eq a) => a -> HasEq a
- Explicit type signature (undefined :: HasEq a): Add the constraint (Eq a) to all explicit type signatures containing HasEq a. If you have more variables HasEq (Either a b) use the inner most forall in which one of the variables is bound
(forall a. HasEq (Either a b) -> c) -> c -> b
becomes
(forall a. (Eq (Either a b)) => HasEq (Either a b) -> c) -> c -> b
- Functions in modules without this extension. Maybe it's possible to add the contexts when the functions are imported. I don't know.
Hiding Types.
This doesn't even really concern haskell anymore. It's just a question of how you can tell ghci or haddock that it doesn't need to show the contexts that were derived.
Examples
Example1:
a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool a (Just x) (Just y) = x == y a _ _ = Nothing
according to rule 2. gets translated to.
a :: (Eq a) => Maybe (HasEq a) -> Maybe (HasEq a) -> Bool
Example2:
b :: Either (HasEq a) (HasShow a) -> String -- what constraints are used here??? b (Left x) = show (x == x) b (Right x) = show x
according to rule 2. gets translated to.
b :: (Eq a, Show a) => Either (HasEq a) (HasShow a) -> String
Example3:
c :: Proxy (HasEq a) -> () -- what constraints are used here??? c _ = ()
according to rule 2. gets translated to. Though I don't really know what Proxy does.
c :: (Eq a) => Proxy (HasEq a) -> ()
d :: Dynamic -> Maybe Bool d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z) -- where does the Eq constraint come from?? d _ = Nothing
according to rule 1. The Eq quality constraint gets set because of the use of the constructor. I'm not sure how to write this in terms of types but it works for GADTs.
comment:20 Changed 6 months ago by gidyn
I think we actually have 2 implementation proposals here:
- tokyo's rules add type constraints, whenever the data type appears in an explicit type signature or when the constructor is used
- use regular type inference
The second implementation would give different results for c and d:
c :: Proxy (HasEq a) -> () -- what constraints are used here??? c _ = ()
No type constraint is added, because none is inferred by the definition of c.
data Dynamic = forall a. Typeable a => MkDyn a d :: Dynamic -> Maybe Bool d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z) -- where does the Eq constraint come from?? d _ = Nothing
DatatypeContexts wouldn't have any effect in this case.
comment:21 Changed 6 months ago by yokto
I just found an other interesting realworld example that could profit from this extension. Consider the vector package. All type signature look something like this.
read :: PrimMonad m => MVector (PrimState m) a -> Int -> m a
Horrible to read, right. With this issue fixed you could put the context on MVector
data (PrimMonad m) => MVector m a = MVector !Int !Int !(MutableArray (PrimState m) a)
and the type signatures could look like this
read :: MVector m a -> Int -> m a
Actually I don't know if this would work but it looks good.
comment:22 Changed 6 months ago by simonpj
I urge you to read the OutsideIn(X) paper.
I think that what you want in comment:21 is already fully implemented. You would declare MVector like this:
data MVector m a where MVector :: PrimMonad m => !Int -> !Int -> !(MutableArray (PrimState m) a) -> MVector m a
comment:23 Changed 6 months ago by goldfire
- Resolution set to wontfix
- Status changed from new to closed
I'm afraid the recent salvo of examples has done little to convince me of what this extension really means. The only I can glean from this is you want a very syntactic translation of a type ... HasEq a ... to Eq a => ... HasEq a .... The problem is that this translation doesn't always make sense, given the other features of Haskell's type system, and would either work or not work in various scenarios unpredictably.
At the risk of repeating myself: those of us with experience working inside GHC and who do know type theory think this proposal doesn't fly. We love contributions and ideas from folks without this experience. But, in this case, where we disagree with the proposal, the burden rests on the proposers to convince us that the proposal holds water. The way to do this starts with a wiki page and typing rules, not just examples.
comment:24 Changed 6 months ago by yokto
Ok @simonpj, that's right. I think I was mistaken and this is not as important as I thought.
Though it there are still some cases that are not covered.
Ok, so let my try to create a wiki page. InferDatatypeContexts
We already have a notation for the "fixed" version:
Moreover, this is arguably the "right" notation because you can vary the context per-constructor:
You may want to make suggesitons to the Haskell Prime group, but I'm disinclined to add yet new behaviour to GHC when an existing solution does the job.
Simon