I've come to think the culprit here is the fallacy that Any should inhabit every kind.
I realize this is useful from an implementation perspective, but it has a number of far reaching consequences: This means that a product kind isn't truly a product of two kinds. x * y, it winds up as a *distinguishable* 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. A coproduct of two kinds x + y, isn't x + y, its x + y + 1. 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. 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? -Edward On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg <e...@cis.upenn.edu>wrote: > I retract my statement. > > 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. > > 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. > > In light of this, it would seem that allowing eta coercions while > retaining consistency would require some more work. > > Thanks for pointing out my mistake. > Richard > > [1] S. Weirich et al. "Generative Type Abstraction and Type-level > Computation." > (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf) > > On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote: > > > On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <e...@cis.upenn.edu> > wrote: > >> [...] > >> 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. > >> > > > > A recent snapshot of ghc HEAD doesn't seem to agree: > > > > {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds, > > TypeFamilies, ScopedTypeVariables, TypeOperators #-} > > > > import GHC.Exts > > import Unsafe.Coerce > > > > data (:=:) :: k -> k -> * where > > Refl :: a :=: a > > > > trans :: a :=: b -> b :=: c -> a :=: c > > trans Refl Refl = Refl > > > > type family Fst (x :: (a,b)) :: a > > type family Snd (x :: (a,b)) :: b > > > > type instance Fst '(a,b) = a > > type instance Snd '(a,b) = b > > > > eta :: x :=: '(Fst x, Snd x) > > eta = unsafeCoerce Refl > > -- ^^^ this is an acceptable way to simulate new coercions, i hope > > > > type family Bad s t (x :: (a,b)) :: * > > type instance Bad s t '(a,b) = s > > type instance Bad s t Any = t > > > > refl_Any :: Any :=: Any > > refl_Any = Refl > > > > cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y > > cong_Bad Refl = Refl > > > > s_eq_t :: forall (s :: *) (t :: *). s :=: t > > s_eq_t = cong_Bad (trans refl_Any eta) > > > > subst :: x :=: y -> x -> y > > subst Refl x = x > > > > coerce :: s -> t > > coerce = subst s_eq_t > > > > {- > > GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help > > *Main> coerce (4.0 :: Double) :: (Int,Int) > > (Segmentation fault > > -} > > > > -- Andrea Vezzosi > > > > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
