I've come to think the culprit here is the fallacy that Any should inhabit every kind. <div><br></div><div>I realize this is useful from an implementation perspective, but it has a number of far reaching consequences:<div>
<br></div><div>This means that a product kind isn't truly a product of two kinds. x * y, it winds up as a <i>distinguishable</i> x * y + 1, as Andrea has shown us happens because you can write a type family or MPTC with fundep that can match on Any.</div>
<div><br></div><div>A coproduct of two kinds x + y, isn't x + y, its x + y + 1. </div><div><br></div><div>Kind level naturals aren't kind nats, they are nats + 1, and not even the one point compactification we get with lazy nats where you have an indistinguishable infinity added to the domain, but rather there is a distinguished atom to each kind under consideration.</div>
<div><br></div><div>I noticed that the polykindedness of Any is abused in the GHC.TypeLits to make fundeps determining a kind, but where else is it exploited?</div><div><br></div><div>-Edward</div><div><br><div class="gmail_quote">
On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I retract my statement.<br>
<br>
My mistake was that I looked at the definition for consistency in FC -- which correctly is agnostic to non-base-kind coercions -- and applied it only to the set of coercion assumptions, not to any coercion derivable from the assumptions. As Andrea's example shows, by assuming an eta coercion, it is possible to derive an inconsistent coercion.<br>
<br>
Examining the definition for FC consistency more closely, an eta coercion does not match to the form allowed for coercion assumptions used to prove consistency. The proof, in [1], requires all assumptions to have a type family application on the left-hand side. An eta coercion does not have a type family application on either side, and so the consistency proof in [1] does not apply.<br>
<br>
In light of this, it would seem that allowing eta coercions while retaining consistency would require some more work.<br>
<br>
Thanks for pointing out my mistake.<br>
Richard<br>
<br>
[1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation."<br>
(<a href="http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf" target="_blank">http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf</a>)<br>
<div class="HOEnZb"><div class="h5"><br>
On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:<br>
<br>
> On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br>
>> [...]<br>
>> So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.<br>
>><br>
><br>
> A recent snapshot of ghc HEAD doesn't seem to agree:<br>
><br>
> {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,<br>
> TypeFamilies, ScopedTypeVariables, TypeOperators #-}<br>
><br>
> import GHC.Exts<br>
> import Unsafe.Coerce<br>
><br>
> data (:=:) :: k -> k -> * where<br>
> Refl :: a :=: a<br>
><br>
> trans :: a :=: b -> b :=: c -> a :=: c<br>
> trans Refl Refl = Refl<br>
><br>
> type family Fst (x :: (a,b)) :: a<br>
> type family Snd (x :: (a,b)) :: b<br>
><br>
> type instance Fst '(a,b) = a<br>
> type instance Snd '(a,b) = b<br>
><br>
> eta :: x :=: '(Fst x, Snd x)<br>
> eta = unsafeCoerce Refl<br>
> -- ^^^ this is an acceptable way to simulate new coercions, i hope<br>
><br>
> type family Bad s t (x :: (a,b)) :: *<br>
> type instance Bad s t '(a,b) = s<br>
> type instance Bad s t Any = t<br>
><br>
> refl_Any :: Any :=: Any<br>
> refl_Any = Refl<br>
><br>
> cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y<br>
> cong_Bad Refl = Refl<br>
><br>
> s_eq_t :: forall (s :: *) (t :: *). s :=: t<br>
> s_eq_t = cong_Bad (trans refl_Any eta)<br>
><br>
> subst :: x :=: y -> x -> y<br>
> subst Refl x = x<br>
><br>
> coerce :: s -> t<br>
> coerce = subst s_eq_t<br>
><br>
> {-<br>
> GHCi, version 7.7.20120830: <a href="http://www.haskell.org/ghc/" target="_blank">http://www.haskell.org/ghc/</a> :? for help<br>
> *Main> coerce (4.0 :: Double) :: (Int,Int)<br>
> (Segmentation fault<br>
> -}<br>
><br>
> -- Andrea Vezzosi<br>
><br>
<br>
<br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</div></div></blockquote></div><br></div></div>