[Haskell-cafe] Kind signatures and closed type families syntax

[Karl Voelker]

On Sat, Nov 29, 2014, at 04:35 PM, Gautier DI FOLCO wrote:
> Hello all,
>
> I have the following code: {-# LANGUAGE NoImplicitPrelude #-} {-#
> LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE
> DataKinds #-} {-# LANGUAGE PolyKinds #-}
>
> data Branch = Left | Right
>
> type family Product (v :: Branch) (a :: k) (b :: k) :: k where Product
> Left l r = l Product Right l r = r
>
> He is doing what I expect it to do and Product has the right Kind:
> *Main> :kind Product Product :: Branch -> k -> k -> k
>
> But when I change the Kind signature syntax, its Kind changes: type
> family Product v a b :: Branch -> k -> k -> k where Its Kind become:
> *Main> :kind Product Product :: Branch -> (Branch -> k -> k -> k) ->
> (Branch -> k1 -> k1 -> k1) -> Branch -> k2 -> k2 -> k2

In a type family declaration, the signature to the right of the
top-level "::" is always the kind of the result. When you drop the kind
signatures from the parameter declarations, the kinds of those
parameters become inferred rather than explicit, but that doesn't change
the interpretation of the top-level signature - it is still just the
kind of the result.

-Karl


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