[Haskell-cafe] Kind product

[Richard Eisenberg]

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 <gautier.difolco at gmail.com> wrote:

> 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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141130/f2c2be33/attachment.html>