If Andres's solution isn't what you want, you probably really do need kind families. They're on the way, as part of my ongoing work in making GHC more dependently typed. Definitely not expected for 7.10, but perhaps for the following release. Out of curiosity, what are you trying to do here? Thanks, Richard On Nov 30, 2014, at 7:28 AM, Gautier DI FOLCO wrote:

2014-11-30 10:57 GMT+01:00 Andres Löh : Hi.

[...]

...

My goal is to have a thing like that: type family Product (v :: Branch) (a :: k1) (b :: k2) :: (Either k1 k2) where

I'm not sure what exactly it is that you want, but this code checks:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-} module PairEitherKinds where

data Branch = L | R

type family Product (s :: Branch) (a :: k1) (b :: k2) :: Either k1 k2 where Product L a b = Left a Product R a b = Right b

Cheers, Andres

Hello,

I know but obtained types are wrapped in the Either kind and I try to have it directly. If I have a kind family I'll do something like this:

type family SumI (s :: Branch) (a :: k1) (b :: k2) :: Max k1 k2 where SumI Left l r = Maximise a b l SumI Right l r = Maximise a b r

type Sum a b = DropFlippedConst (SumI a b)

type FlippedConst a b = Const b a

kind Max a b c = FromJust (LeftMax a b c <|> LeftMax b a c) kind family LeftMax a b where Max * k2 = Nothing Max k k = Just k Max (k1 -> k2) k3 = (k1 ->) <$> Max k2 k3

kind Maximize a b c = FromJust (LeftMaximize a b c <|> LeftMaximize b a c) kind family LeftMaximize a b c where LeftMaximize * k1 k2 = Nothing LeftMaximize k k k = Just k LeftMaximize (k1 -> k2) k3 k4 = FlippedConst k1 <$> LeftMaximize k2 k3 k4

kind family FromJust a where Just x =x

type family DropFlippedConst x where DropFlippedConst (FlippedConst a b) = DropFlippedConst b DropFlippedConst a = a

I don't know if it's clearer now, let me know.

Thanks, Regards. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Nov 30, 2014, at 5:38 PM, Gautier DI FOLCO wrote:

Thanks for your answer. I don't see why it's closer to dependent typing, can you give me some hints?

One of the steps to dependent typing in Haskell (as my research partners and I see it) is making the type level and the kind level uniform -- that is, to stop distinguishing types from kinds. Thus, since we have type families, we must have kind families as well. The uniformity between the levels makes it easier to promote more data constructors to type constructors. I agree with the implied opinion that kind families have little to do with types depending on values. Richard