GHC: Ticket #8026: DatatypeContexts should be fixed, not deprecated
http://ghc.haskell.org/trac/ghc/ticket/8026
<p>
To borrow an example from the <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts"><span class="icon"></span>prime wiki page</a>, the following code fails to compile:
</p>
<pre class="wiki">data Eq a => Foo a = Foo a
isEq :: Foo a -> Foo a -> Bool
isEq (Foo x) (Foo y) = x == y
</pre><p>
We have to tell the compiler that <tt>Eq a => Foo a</tt> in <tt>isEq</tt>, even though this is part of the data type's definition. Furthermore,
</p>
<pre class="wiki">getVal :: Foo a -> a
getVal (Foo x) = x
</pre><p>
will also fail because of the missing constraint, even though it isn't used in the function's definition.
</p>
<p>
Rather than just deprecating the <tt>DatatypeContexts</tt> extension, it should be "fixed" to remember the context wherever the data type is used.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/8026
Trac 1.0.1simonpjTue, 02 Jul 2013 09:56:36 GMTstatus changed; difficulty, resolution set
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:1
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:1
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>resolution</strong>
set to <em>wontfix</em>
</li>
</ul>
<p>
We already have a notation for the "fixed" version:
</p>
<pre class="wiki">data Foo a where
Foo :: Eq a => a -> Foo a
</pre><p>
Moreover, this is arguably the "right" notation because you can vary the context per-constructor:
</p>
<pre class="wiki">data Bar a where
Bar1 :: Eq a => a -> Bar a
Bar2 :: (Ix a, Show a) => a -> a -> Bar a
</pre><p>
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.
</p>
<p>
Simon
</p>
TicketgidynTue, 02 Jul 2013 10:13:36 GMTstatus changed; resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:2
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:2
<ul>
<li><strong>status</strong>
changed from <em>closed</em> to <em>new</em>
</li>
<li><strong>resolution</strong>
<em>wontfix</em> deleted
</li>
</ul>
<p>
This only works when pattern matching on the constructor, and GADTs are no different to classical data types for this. Functions which uses a <tt>Foo</tt> without pattern matching will require a redundant type context in either case.
</p>
TicketgidynTue, 02 Jul 2013 10:28:23 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:3
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:3
<p>
This might be a better example:
</p>
<pre class="wiki">data Eq a => Pair a = Pair {x::a, y::a}
equal :: Pair a -> Bool
equal pair = (x pair) == (y pair)
</pre><p>
Is there any way you can avoid a redundant <tt>Eq a =></tt> in the definition of <tt>equal</tt>, without adding a redundant pattern match?
</p>
TicketgidynTue, 02 Jul 2013 10:30:12 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:4
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:4
<ul>
<li><strong>cc</strong>
<em>gideon@…</em> added
</li>
</ul>
TicketgidynTue, 02 Jul 2013 11:38:52 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:5
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:5
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8026#comment:1" title="Comment 1 for Ticket #8026">simonpj</a>:
</p>
<blockquote class="citation">
<p>
You may want to make suggesitons to the Haskell Prime group
</p>
</blockquote>
<p>
Haskell Prime expect extensions to be implemented in a compiler first, so that would have to come if/after it's been implemented here.
</p>
TicketisaacdupreeTue, 02 Jul 2013 17:23:59 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:6
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:6
<p>
In your example, do any of these three expressions typecheck? (note: functions are not in Eq)
</p>
<pre class="wiki">Pair id id
undefined :: Pair (()->())
equal undefined
</pre>
TicketmonoidalTue, 02 Jul 2013 21:47:26 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:7
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:7
<p>
@gidyn: What would the type of <tt>x</tt> be in your example?
</p>
<p>
You probably want <tt>x</tt> to <em>introduce</em> the validity of constraint <tt>Eq a</tt>. So the type would be somewhat dual to <tt>Eq a => Pair a -> a</tt>: using it would prove the constraint <tt>Eq a</tt>, rather than requiring evidence for the constraint. Something like <tt>Pair a -> (Eq a; a)</tt>.
</p>
<p>
It seems to me this change would complicate the type system a lot, while the benefits are rather doubtful.
</p>
TicketgidynWed, 03 Jul 2013 07:52:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:8
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:8
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8026#comment:7" title="Comment 7 for Ticket #8026">monoidal</a>:
</p>
<p>
The generated getter should have type <tt>Eq a => Pair a -> a</tt> - nothing complicated about it, unless I missed your point.
</p>
TicketmonoidalWed, 03 Jul 2013 09:05:07 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:9
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:9
<p>
@gidyn: You probably meant <tt>x :: Eq a => Pair a -> a</tt>.
</p>
<p>
Consider isaacdupree's <tt>equal (undefined :: Pair (() -> ()))</tt>. Surely this should be legal: <tt>undefined</tt> inhabits every type. Yet attempting to evaluate it leads to using <tt>==</tt> from <tt>Eq (() -> ())</tt> which does not exist.
</p>
TicketmonoidalWed, 17 Jul 2013 15:22:50 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:10
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:10
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>wontfix</em>
</li>
</ul>
<p>
As far as I understand, the proposal is not sound.
</p>
TicketgidynFri, 19 Jul 2013 09:11:40 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:11
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:11
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8026#comment:9" title="Comment 9 for Ticket #8026">monoidal</a>:
</p>
<blockquote class="citation">
<p>
Consider isaacdupree's <tt>equal (undefined :: Pair (() -> ()))</tt>. Surely this should be legal: <tt>undefined</tt> inhabits every type. Yet attempting to evaluate it leads to using <tt>==</tt> from <tt>Eq (() -> ())</tt> which does not exist.
</p>
</blockquote>
<p>
The use of DatatypeContexts would make this equivalent to <tt>equal (undefined :: Eq ? => Pair (() -> ()))</tt>, so the type he's asking about couldn't (and shouldn't) be constructed when using this extension.
</p>
<p>
Excluding some nefarious uses of undefined seems like a reasonable price to pay for turning on a useful extension.
</p>
TicketgidynFri, 19 Jul 2013 09:18:03 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:12
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:12
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8026#comment:10" title="Comment 10 for Ticket #8026">monoidal</a>:
</p>
<blockquote class="citation">
<p>
As far as I understand, the proposal is not sound.
</p>
</blockquote>
<p>
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 a more limited form of SPJ's <tt>(...) =></tt> proposal, but tied to the extension which most requires it, and without the syntactic noise.
</p>
TicketyoktoMon, 22 Sep 2014 13:04:13 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:13
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:13
<p>
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
</p>
<pre class="wiki">newtype (Num n) => Num' n = Num' n
type Int' = Num' Int
(+) :: Num' n -> Num' n -> Num' n
</pre><p>
This would mean you could actually make instances
</p>
<pre class="wiki">instance SomeClass (Num' n)
</pre><p>
that don't conflict with all other instances
</p>
<pre class="wiki">instance (Num n) => SomeClass n
instance SomeClass Char
</pre><p>
crash
</p>
<p>
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.
</p>
<p>
you can not make an instance
</p>
<pre class="wiki">class SomeClass a b | a -> b
instance (Num n) => SomeClass n b
</pre><p>
without immediately blocking all other possible Instances.
</p>
<p>
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.
</p>
<p>
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.
</p>
TicketgidynMon, 22 Sep 2014 14:08:34 GMTstatus changed; resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:14
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:14
<ul>
<li><strong>status</strong>
changed from <em>closed</em> to <em>new</em>
</li>
<li><strong>resolution</strong>
<em>wontfix</em> deleted
</li>
</ul>
<p>
See also <a class="ext-link" href="https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures#extra-constraints-wildcard"><span class="icon"></span>Partial Type Signatures</a>.
</p>
TicketgoldfireMon, 22 Sep 2014 14:19:32 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:15
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:15
<p>
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 <em>return</em> 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!
</p>
TicketgidynMon, 22 Sep 2014 14:38:25 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:16
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:16
<p>
Consider the first example
</p>
<pre class="wiki">data Eq a => Foo a = Foo a
isEq :: Foo a -> Foo a -> Bool
isEq (Foo x) (Foo y) = x == y
</pre><p>
This won't compile, because <tt>isEq</tt> is missing <tt>Eq a =></tt>. However, if we miss out the type signature altogether, GHC will correctly infer it. With <a class="ext-link" href="https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures#extra-constraints-wildcard"><span class="icon"></span>Partial Type Signatures</a>, we can also write
</p>
<pre class="wiki">isEq :: _ => Foo a -> Foo a -> Bool
</pre><p>
and GHC will infer the constraint.
</p>
<p>
This proposal is requesting that whenever <tt>DatatypeContexts</tt> 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.
</p>
<p>
It is different to extra-constraints wildcards in that:
</p>
<ul><li>no explicit syntax is needed, other than <tt>DatatypeContexts</tt>
</li><li>the only constraint which can be added by inference is one that was given in the data type declaration.
</li></ul><p>
Is that clearer?
</p>
TicketgidynMon, 22 Sep 2014 14:48:59 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:17
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:17
<p>
To emphasise: this proposal is <strong>not</strong> 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.
</p>
TicketgoldfireMon, 22 Sep 2014 16:09:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:18
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:18
<p>
This proposal <em>does</em> 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.
</p>
<p>
Your example is clear for that simple situation. But, Haskell's type system is not that simple! For example:
</p>
<pre class="wiki">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
</pre><p>
Your examples seem to address specific, easy cases. But, we need to consider all the wide range of compositions with other Haskell features!
</p>
TicketyoktoMon, 22 Sep 2014 21:42:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:19
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:19
<p>
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.
</p>
<p>
<tt>data Eq a => HasEq a = MkHasEq a</tt>
</p>
<h2 id="DerivingTypes">Deriving Types</h2>
<p>
How can you get a value of type <tt>HasEq a</tt>.
</p>
<ol><li>Using a Constructor (also in a pattern):
Use the same trick as with GADTs?
Just make the type signature of the constructor <tt>(Eq a) => a -> HasEq a</tt>
</li><li>Explicit type signature <tt>(undefined :: HasEq a)</tt>:
Add the constraint <tt>(Eq a)</tt> to all explicit type signatures containing <tt>HasEq a</tt>.
If you have more variables <tt>HasEq (Either a b)</tt> use the inner most forall in which one of the variables is bound
</li></ol><blockquote>
<p>
<tt> (forall a. HasEq (Either a b) -> c) -> c -> b </tt>
becomes
</p>
</blockquote>
<blockquote>
<p>
<tt> (forall a. (Eq (Either a b)) => HasEq (Either a b) -> c) -> c -> b </tt>
</p>
</blockquote>
<ol start="3"><li>Functions in modules without this extension.
Maybe it's possible to add the contexts when the functions are imported. I don't know.
</li></ol><h2 id="HidingTypes.">Hiding Types.</h2>
<p>
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.
</p>
<h2 id="Examples">Examples</h2>
<p>
Example1:
</p>
<pre class="wiki">a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool
a (Just x) (Just y) = x == y
a _ _ = Nothing
</pre><p>
according to rule 2. gets translated to.
<tt>a :: (Eq a) => Maybe (HasEq a) -> Maybe (HasEq a) -> Bool</tt>
</p>
<p>
Example2:
</p>
<pre class="wiki">b :: Either (HasEq a) (HasShow a) -> String -- what constraints are used here???
b (Left x) = show (x == x)
b (Right x) = show x
</pre><p>
according to rule 2. gets translated to.
<tt> b :: (Eq a, Show a) => Either (HasEq a) (HasShow a) -> String </tt>
</p>
<p>
Example3:
</p>
<pre class="wiki">c :: Proxy (HasEq a) -> () -- what constraints are used here???
c _ = ()
</pre><p>
according to rule 2. gets translated to. Though I don't really know what Proxy does.
<tt> c :: (Eq a) => Proxy (HasEq a) -> () </tt>
</p>
<pre class="wiki">d :: Dynamic -> Maybe Bool
d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z) -- where does the Eq constraint come from??
d _ = Nothing
</pre><p>
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.
</p>
TicketgidynTue, 23 Sep 2014 07:23:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:20
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:20
<p>
I think we actually have 2 implementation proposals here:
</p>
<ul><li>tokyo's rules add type constraints, whenever the data type appears in an explicit type signature or when the constructor is used
</li><li>use regular type inference
</li></ul><p>
The second implementation would give different results for <tt>c</tt> and <tt>d</tt>:
</p>
<pre class="wiki">c :: Proxy (HasEq a) -> () -- what constraints are used here???
c _ = ()
</pre><p>
No type constraint is added, because none is inferred by the definition of <tt>c</tt>.
</p>
<pre class="wiki">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
</pre><p>
<tt>DatatypeContexts</tt> wouldn't have any effect in this case.
</p>
TicketyoktoTue, 23 Sep 2014 23:29:27 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:21
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:21
<p>
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.
</p>
<p>
<tt>read :: PrimMonad m => MVector (PrimState m) a -> Int -> m a</tt>
</p>
<p>
Horrible to read, right. With this issue fixed you could put the context on MVector
</p>
<p>
<tt>data (PrimMonad m) => MVector m a = MVector !Int !Int !(MutableArray (PrimState m) a)</tt>
</p>
<p>
and the type signatures could look like this
</p>
<p>
<tt>read :: MVector m a -> Int -> m a</tt>
</p>
<p>
Actually I don't know if this would work but it looks good.
</p>
TicketsimonpjWed, 24 Sep 2014 08:53:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:22
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:22
<p>
I urge you to read the OutsideIn(X) paper.
</p>
<p>
I think that what you want in <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8026#comment:21" title="Comment 21 for Ticket #8026">comment:21</a> is already fully implemented. You would declare <tt>MVector</tt> like this:
</p>
<pre class="wiki">data MVector m a where
MVector :: PrimMonad m
=> !Int -> !Int -> !(MutableArray (PrimState m) a) -> MVector m a
</pre>
TicketgoldfireWed, 24 Sep 2014 12:07:33 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:23
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:23
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>wontfix</em>
</li>
</ul>
<p>
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 <tt>... HasEq a ...</tt> to <tt>Eq a => ... HasEq a ...</tt>. 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.
</p>
<p>
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.
</p>
TicketyoktoWed, 24 Sep 2014 12:29:14 GMT
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:24
http://ghc.haskell.org/trac/ghc/ticket/8026#comment:24
<p>
Ok @simonpj, that's right. I think I was mistaken and this is not as important as I thought.
</p>
<p>
Though it there are still some cases that are not covered.
</p>
<p>
Ok, so let my try to create a wiki page. <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/InferDatatypeContexts">InferDatatypeContexts</a>
</p>
Ticket