GHC: Ticket #2157: Equality Constraints with Type Families
http://ghc.haskell.org/trac/ghc/ticket/2157
<p>
For the implementation of fixpoint recursive definitions for a datatype I have defined the family:
</p>
<pre class="wiki">type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One
</pre><p>
for which we can define functor instances
</p>
<pre class="wiki">instance (Functor (F [a])) where
fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x)
...
</pre><p>
However, in the definition of recursive patterns over these representation, I need some coercions to hold such as
</p>
<pre class="wiki">F d c ~ F a (c,a)
</pre><p>
but in the current implementation they are evaluated as
</p>
<pre class="wiki">F d ~ F a /\ c ~(c,a)
</pre><p>
what does not express the semantics of "fully parameterized equality" that I was expecting
</p>
<p>
You can find a pratical example in (<a class="ext-link" href="http://groups.google.com/group/fa.haskell/browse_thread/thread/6ea21dcade9e632f/01148521c33ac29a"><span class="icon"></span>my conversions at the haskell-cafe mailing list</a>)
</p>
<p>
In order to avoid this, the family could be redefined as
</p>
<pre class="wiki">type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x
</pre><p>
but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.
</p>
<p>
PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2157
Trac 1.2hpachecoFri, 14 Mar 2008 19:10:24 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:1
<p>
I meant conversations, not conversions :P
</p>
TicketchakMon, 17 Mar 2008 01:38:00 GMTos, component, architecture, type changed; owner set
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:2
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Multiple</em>
</li>
<li><strong>component</strong>
changed from <em>Compiler</em> to <em>Compiler (Type checker)</em>
</li>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Multiple</em>
</li>
<li><strong>type</strong>
changed from <em>bug</em> to <em>feature request</em>
</li>
</ul>
<p>
I'd like to find a solution here, but as far as I can see, there is no bug in GHC's type checker. In fact, if GHC would admit any of your code, it would also allow programs that are not type safe.
</p>
<p>
In particular, given your second definition,
</p>
<pre class="wiki">type family F a x :: *
</pre><p>
if we would allow partial applications, as in <code>Functor (F a)</code>, we would get an inconsistent system; see Section 3.6 in <a class="ext-link" href="http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html"><span class="icon"></span>http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html</a>.
</p>
<p>
On the other hand, given
</p>
<pre class="wiki">type family F a :: * -> *
</pre><p>
an equality of the form <code>F a1 b1 ~ F a2 b2</code> implies <code>F a1 ~ F a2</code> and <code>b1 ~ b2</code> as always in Haskell (this is what Mark Jones called higher-kinded unification in his paper about constructor classes).
</p>
<p>
In other words, given a type (f :: * -> * -> *), the partial application <code>f t</code> is well-formed exactly if the decomposition rule holds (i.e., <code>f a1 b1 ~ f a2 b2</code> implies <code>f a1 ~ f a2</code> and <code>b1 ~ b2</code>). These two properties are causally linked, you cannot get one without the other.
</p>
TicketclausMon, 17 Mar 2008 13:14:09 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:3
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:2" title="Comment 2">chak</a>:
</p>
<blockquote class="citation">
<p>
On the other hand, given
</p>
<pre class="wiki">type family F a :: * -> *
</pre><p>
an equality of the form <code>F a1 b1 ~ F a2 b2</code> implies <code>F a1 ~ F a2</code> and <code>b1 ~ b2</code> as always in Haskell
</p>
</blockquote>
<p>
i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - <code>Const</code> and <code>f</code> seem fishy here (wrt your implication, at least):
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
type family Const a :: * -> *
type instance Const a = C a
type C a t = a
f :: Const Bool Int -> Const Bool Char -> Const Bool Bool
f i c = False
-- f i c = i
-- f i c = i && True
-- f i c = (i || c)
type family Const2 a :: * -> *
type instance Const2 a = Ct a
newtype Ct a t = Ct a
g :: Const2 Bool Int -> Const2 Bool Char -> Const2 Bool Bool
g i c = Ct False
-- g i c = Ct i
-- g i c = Ct (i && True)
-- g i c = Ct (i || c)
</pre><p>
for <code>Const</code> and <code>f</code>, <code>GHCi, version 6.9.20080217</code> happily accepts <code>i && True</code> and <code>i || c</code>, converting between <code>Const Bool *</code> and <code>Bool</code>, but does not accept <code>i</code>.
</p>
TickethpachecoMon, 17 Mar 2008 15:08:31 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:4
<p>
I understood your points and they do make sense, but do you think that this is a feasible feature request or it should never be supported?
</p>
<p>
I have just remembered that, still for the family
</p>
<pre class="wiki">type family F a x :: *
type instance F [a] x = Either () (a,x)
type instance F Int x = Either () x
</pre><p>
we can write "partial-evaluated classes for F" whenever not all type parameters are in use.
For the Functor class this would mean:
</p>
<pre class="wiki">class FunctorF x where
fmapF :: (a -> b) -> F x a -> F x b
instance FunctorF [a] where
fmapF _ (Left _) = Left ()
fmapF f (Right (a,x)) = Right (a,f x)
instance FunctorF Int where
fmapF _ (Left ()) = Left ()
fmapF f (Right n) = Right (f n)
</pre><p>
At first glance it is less generic but seems to work.
However, a previous function (for the family F a :: * -> *)
</p>
<pre class="wiki">hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmap (hylo d g h) . h
</pre><p>
if translated to
</p>
<pre class="wiki">hylo :: (FunctorF d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmapF (hylo d g h) . h
</pre><p>
does not compile with the explicit type signature.
Without a type signature it compiles and infers the signature (does not make sense to me)
</p>
<pre class="wiki">hylo :: forall t d c a. (FunctorF d) => t -> (F d c -> c) -> (a -> F d a) -> a -> c
</pre><p>
However, if this signature is passed explicitly, it does not compile again.
There must be a bug somewhere in this scheme, or am I missing something huge?
</p>
<p>
Regards,
hugo
</p>
TickethpachecoMon, 17 Mar 2008 18:21:24 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:5
<p>
Well, it seems to work if the add a "magic" dummy argument to fmapF.
</p>
<pre class="wiki">class FunctorF x where
fmapF :: d -> (a -> b) -> F x a -> F x b
hylo :: (FunctorF d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmapF d (hylo d g h) . h
</pre>
TickethpachecoMon, 17 Mar 2008 22:45:41 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:6
<p>
Curiously if I have
</p>
<pre class="wiki">fff a = fmapF a id
</pre><p>
it compiles correctly.
But if I infer the type signature of fff I get
</p>
<pre class="wiki">fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
</pre><p>
On the other side, a similar problem as before arises when
</p>
<pre class="wiki">fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
fff a = fmapF a id
</pre><p>
fails to compile.
This must be a bug. Sorry for all this posts.
</p>
TicketchakThu, 20 Mar 2008 00:24:31 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:7
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:7
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:3" title="Comment 3">claus</a>:
</p>
<blockquote class="citation">
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:2" title="Comment 2">chak</a>:
</p>
<blockquote class="citation">
<p>
On the other hand, given
</p>
<pre class="wiki">type family F a :: * -> *
</pre><p>
an equality of the form <code>F a1 b1 ~ F a2 b2</code> implies <code>F a1 ~ F a2</code> and <code>b1 ~ b2</code> as always in Haskell
</p>
</blockquote>
<p>
i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - <code>Const</code> and <code>f</code> seem fishy here (wrt your implication, at least):
</p>
</blockquote>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
type family Const a :: * -> *
type instance Const a = C a
type C a t = a
</pre><p>
Why do you think <code>Const</code> is fishy? Maybe I should make more precise what I regard as <em>partial application</em> in the context of type families. If you look at <a class="ext-link" href="http://haskell.org/haskellwiki/GHC/Type_families"><span class="icon"></span>the type family specification</a> in Section 7.1, it says that the arity of a type family is the number of parameters given in the type family declaration. In the case of <code>Const</code>, this is 1 (namely <code>a</code>), <strong>not</strong> 2 (as you might think if you only consider the kind of <code>Const</code>). Whenever a type family is used, you must supply <strong>at least</strong> as many type arguments as the arity of the type family suggests. So, in the case of <code>Const</code>, a single argument suffices. Do you think Section 7 of <a class="ext-link" href="http://haskell.org/haskellwiki/GHC/Type_families"><span class="icon"></span>the type family specification</a> is unclear on that matter. If so, I'd be grateful for any suggestions that make the specification clearer.
</p>
<p>
NB: The rules for what constitutes a valid partial application of a vanilla type synonym are different, see <a href="http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms">http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms</a> This may be somewhat confusing, but I don't think there is much we can do about this, as the present definitions are crucial to get a sound type system. (Well, we could restrict what you can do with vanilla synonyms, but we'd like to stay backwards compatible to H98 and, I guess, people would also not be happy to sacrifice any of the currently offered expressiveness.)
</p>
TicketchakThu, 20 Mar 2008 00:39:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:8
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:8
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:6" title="Comment 6">hpacheco</a>:
</p>
<blockquote class="citation">
<p>
Curiously if I have
</p>
<pre class="wiki">fff a = fmapF a id
</pre><p>
it compiles correctly.
But if I infer the type signature of fff I get
</p>
<pre class="wiki">fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
</pre><p>
On the other side, a similar problem as before arises when
</p>
<pre class="wiki">fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
fff a = fmapF a id
</pre><p>
fails to compile.
This must be a bug. Sorry for all this posts.
</p>
</blockquote>
<p>
No, it's not as bug. The problem is that the variable <code>x</code> occurs <strong>only</strong> as a type-index to the type family in the signature. Remember from above, as the arity of <code>F</code> is 2, given <code>F a1 b1 ~ F a2 b2</code> we <strong>can not</strong> deduce that <code>a1 ~ a2</code> and <code>b1 ~ b2</code>. (We need to explain that better in the type family documentation...)
</p>
TicketclausThu, 20 Mar 2008 12:44:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:9
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:9
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:7" title="Comment 7">chak</a>:
</p>
<blockquote class="citation">
<blockquote class="citation">
<blockquote class="citation">
<pre class="wiki">type family F a :: * -> *
</pre><p>
an equality of the form <code>F a1 b1 ~ F a2 b2</code> implies <code>F a1 ~ F a2</code> and <code>b1 ~ b2</code> as always in Haskell
</p>
</blockquote>
<p>
i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - <code>Const</code> and <code>f</code> seem fishy here (wrt your implication, at least):
</p>
</blockquote>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
type family Const a :: * -> *
type instance Const a = C a
type C a t = a
</pre><p>
Why do you think <code>Const</code> is fishy?
</p>
</blockquote>
<p>
because:
</p>
<ul><li>type synonym <code>C</code> appears partially applied in what amounts to a type class instance parameter position (the rhs of the Const instance)
</li></ul><ul><li>the implementation definitely does not behave as if your decomposition played any role (parameters of both <code>Const Bool Int</code> and <code>Const Bool Char</code> are used as/converted to <code>Bool</code>, hence equal types even though <code>Int</code> does not equal <code>Char</code>). nor do the permitted and not-permitted conversions in <code>f</code> seem consistent - compare also:
</li></ul><p>
<a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-March/040788.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-March/040788.html</a>
</p>
<p>
<a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-March/040790.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-March/040790.html</a>
</p>
<blockquote class="citation">
<p>
Maybe I should make more precise what I regard as <em>partial application</em> in the context of type families.
</p>
</blockquote>
<p>
it isn't about partial applications of type families (even though the different sorts of parameters there take some getting used to), but about good old-fashioned partial applications of type synonyms in new contexts. i guess they are permitted here because the rhs of a type instance uses the same grammar non-terminal as the rhs of a type synonym, but i suspect that the rhs of a type instance might have to be treated like a type parameter of a type class instance.
</p>
<p>
but that is just a guess - the main issues here are the decomposition rule, which i don't quite understand, and which doesn't quite seem to be used in the implementation, and the equalities/conversions permitted in the implementation, which do not seem to be consistent.
</p>
TicketchakTue, 25 Mar 2008 06:25:50 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:1
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:9" title="Comment 9">claus</a>:
</p>
<blockquote class="citation">
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157#comment:7" title="Comment 7">chak</a>:
</p>
<blockquote class="citation">
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
type family Const a :: * -> *
type instance Const a = C a
type C a t = a
</pre><p>
Why do you think <code>Const</code> is fishy?
</p>
</blockquote>
<p>
because:
</p>
<ul><li>type synonym <code>C</code> appears partially applied in what amounts to a type class instance parameter position (the rhs of the Const instance)
</li></ul></blockquote>
<p>
I don't agree that the lhs of a type instance amounts to a type class instance parameter position; type instance have nothing to do with type classes.
</p>
<p>
However, I think I now understand what you are worried about. It is the interaction of type families and GHC's generalised type synonyms (i.e., type synonyms that may be partially applied). I agree that it does lead to an odd interaction, because the outcome may depend on the order in which the type checker performs various operations. In particular, whether it first applies a type instance declaration to reduce a type family application or whether it first performs decomposition.
</p>
<p>
The most clean solution may indeed be to outlaw partial applications of vanilla type synonyms in the rhes of type instances. (Which is what I will implement unless anybody has a better idea.)
</p>
TicketchakWed, 26 Mar 2008 01:05:47 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:11
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:11
<p>
See also the clarification in <a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-March/040983.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-March/040983.html</a>
</p>
TicketchakWed, 26 Mar 2008 09:24:41 GMT
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:12
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:12
<p>
Also <a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-March/040989.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-March/040989.html</a>
</p>
TicketiglooSun, 30 Mar 2008 14:41:52 GMTdifficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:13
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:13
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
TickethpachecoTue, 08 Apr 2008 04:12:40 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:14
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:14
<ul>
<li><strong>cc</strong>
<em>hpacheco@…</em> added
</li>
</ul>
TicketchakMon, 14 Jul 2008 14:48:38 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:15
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:15
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
I fixed the checking of rhss of type family instances. Otherwise, I don't think there is anything that we can do about this; hence, I close the ticket.
</p>
TicketchakTue, 15 Jul 2008 05:28:54 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:16
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:16
<ul>
<li><strong>testcase</strong>
set to <em>T2157</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:45:17 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:17
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:17
<ul>
<li><strong>architecture</strong>
changed from <em>Multiple</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:54:54 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:18
http://ghc.haskell.org/trac/ghc/ticket/2157#comment:18
<ul>
<li><strong>os</strong>
changed from <em>Multiple</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket