Re: [Haskell-cafe] Kind product

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