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.

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