This is probably a silly question but I cannot figure out the underlying rules for the following behavior:
foo :: t (f a) -> f a b -- accepted
foo = undefined
bar :: t [f a] -> f a b -- rejected
bar = undefined
It makes perfect sense that f
applied to a
and a b
respectively in bar
leads to a kind error and is thus rejected. But why is foo
accepted?
It's the kind of f
.
Since the return type is f a b
- i.e. f
applied to two parameters, - it means that f :: Type -> Type -> Type
.
But then f a
is used as a list element - [f a]
- and list elements must be Type
, which means that f a :: Type
, which means that f :: Type -> Type
.
Mismatch.
foo
works because types can be partially applied. That is, if f :: Type -> Type -> Type
, then f a :: Type -> Type
. And then, type t
is allowed to have a parameter of kind Type -> Type
, so everything matches.
To reiterate the above:
foo
works because type t
may have a parameter of kind Type -> Type
.bar
doesn't work, because type []
(aka "list") must have a parameter of kind Type
.If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With