[Haskell-cafe] Kind product

[Gautier DI FOLCO]

2014-11-30 10:57 GMT+01:00 Andres Löh <andres.loeh at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141130/4c528253/attachment.html>