2014-11-30 10:57 GMT+01:00 Andres Löh <andres.loeh@gmail.com>:

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.