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.