Kind signatures and closed type families syntax
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 It's even worse with this syntax: type family Product :: Branch -> k -> k -> k where Produces: *Main> :r [1 of 1] Compiling Main ( product-highkind.hs, interpreted ) product-highkind.hs:13:3: Number of parameters must match family declaration; expected 0 In the equations for closed type family ‘Product’ In the type family declaration for ‘Product’ Failed, modules loaded: none. I don't know if I'm tired or not but in the documentation [1] these syntaxes should be equivalent. If not, I'll take any explanations. Thanks in advance for your help. [1] https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/kind-polymorp...
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
2014-11-30 4:42 GMT+01:00 Karl Voelker
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.
Hello, Thanks for your answer, it's perturbing me but that's a nice explanation. Thanks.
participants (2)
-
Gautier DI FOLCO -
Karl Voelker