Functor variables for Flip data type
I have the following type definition:
newtype Flip f a b =
Flip (f b a) deriving (Eq, Show)
Does the data constructor create Flip
one or three arguments?
Sequence of execution:
data K a b = K a
newtype Flip f a b =
Flip (f b a) deriving (Eq, Show)
instance Functor (Flip K a) where
fmap f (Flip (K b)) = Flip (K (f b))
What is the type (Flip K a)
?
source to share
The data constructor Flip
takes one argument . This argument is of type f b a
.
This means that f
it is itself a higher-order type argument with a type f :: * -> * -> *
. Stricter operator newtype
:
newtype Flip (f :: * -> * -> *) a b = Flip (f b a)
This way you can instantiate Flip Either Int Bool
since Either
is a type that requires two additional type parameters, then construct a Flip (Right 1) :: Flip Either Int Bool
.
What is the type
(Flip K a)
?
Flip K a
is not a fully usable type. In pseudocode, it is of type b -> Flip K a b
. Once b
resolved ( Functor
works with higher order types), we know that the only argument Flip
will have a constructor K b
. So, for example, Flip (K 1)
is a type Flip K a Int
.
source to share
The future is now that you (use ghc 8 and) enable a flag or two
Prelude> :set -XPolyKinds -XFlexibleInstances
We declare
Prelude> newtype Flip f a b = MkFlip (f b a)
and then ask
Prelude> :kind Flip
Flip :: (k1 -> k -> *) -> k -> k1 -> *
Prelude> :type MkFlip
MkFlip
:: forall k k1 (b :: k) (f :: k -> k1 -> *) (a :: k1).
f b a -> Flip f a b
The type constructor Flip
takes two implicit arguments, k
and k1
, and three explicit arguments, which are a binary function that creates the type, and then two arguments in reverse order. The arguments to this function are of unrestricted type (old people can say "kind" if they want to), but it certainly returns a type (in the strict sense "thing in *
", not the uselessly vague feeling of "any old garbage right ::
"), because it is necessarily used as an ad type MkFlip
.
The data constructor MkFlip
takes five implicit arguments (namely arguments Flip
) and one explicit argument, which is some data in the f b a
.
What happens is a Hindley-Milner type inference up one level. Constraints are collected (for example, f b a
must settle *
because the constructor argument must live f b a
), but otherwise the most general type is supplied: a
and b
can be any, so their types are generic like k1
and k
.
Let's reproduce the same game with a constant type constructor:
Prelude> newtype K a b = MkK a
Prelude> :kind K
K :: * -> k -> *
Prelude> :type MkK
MkK :: forall k (b :: k) a. a -> K a b
We see that a :: *
, but b
could be any old rubbish (and, for that matter k :: *
, like these days * :: *
). It is clear that it is a
actually used as a type of thing, but b
not used at all, therefore, unlimited.
Then we can declare
Prelude> instance Functor (Flip K b) where fmap f (MkFlip (MkK a)) = MkFlip (MkK (f a))
and ask
Prelude> :info Flip
...
instance [safe] forall k (b :: k). Functor (Flip K b)
which tells us that unused b
can be any old junk. Since we had
K :: * -> k -> *
Flip :: (k1 -> k -> *) -> k -> k1 -> *
we can combine k1 = *
and get
Flip K :: k -> * -> *
and therefore
Flip K b :: * -> *
for any old one b
. So the instance is Functor
plausible and indeed implemented with a function acting on the boxed element a
corresponding to the argument Flip K b
that becomes the first argument k
, hence the type of the stored element.
Unification-based type inference is alive and well, to the right of ::
.
source to share