[Haskell-cafe] What's the story of this weird type?

[Chris Wong]

Hi David,

On Sat, Mar 21, 2015 at 10:21 AM, David Feuer <david.feuer at gmail.com> wrote:
> I was reading an answer by Luis Casillas on Stack Overflow
>
> http://stackoverflow.com/a/23418746/1477667
>
> and he used a somewhat peculiar type, with apparently not-so-useful constraints:
>
> newtype f :-> g =
>     Natural { eta :: forall x. (Functor f, Functor g) => f x -> g x }
>
> There are a couple things about it that I don't understand.
>
> 1. I can construct a :-> from a function that doesn't satisfy the
> constraints, and I can pattern match to get access to it, but I can't
> use it. Why am I allowed to construct it at all?
>
> data Mb a = N | J a -- Not a Functor instance
>
> -- This is accepted (why?)
> pot = Natural (\case
>   [] -> N
>   (a:_) -> J a)
>
> -- And I can even do this:
> mb :: Functor Mb => Mb Int
> mb = case pot of
>        Natural f -> f [3]
>
> But then of course I can't satisfy the constraint to use it.

I think it would help to use the dictionary-passing interpretation of
type classes:

    newtype f :-> g =
        Natural { eta :: forall x. FunctorInstance f ->
FunctorInstance g -> f x -> g x }

In this form we can see why your code works that way. This inner
function only needs the Functor instances when it is *called*, not
when it's constructed. So GHC defers resolving the constraints until
the function is used.

Alternatively, we can write :-> as a GADT:

    newtype f :-> g where
        Natural :: (forall x. (Functor f, Functor g) => f x -> g x) -> (f :-> g)
        -- a.k.a. Natural :: (forall x. FunctorInstance f ->
FunctorInstance g -> f x -> g x) -> (f :-> g)

Notice again how it's the inner function that wants the instances, not
the Natural constructor itself.

This form suggests a method to check the constraints earlier. If we
move the (Functor f, Functor g) out of the inner forall:

    data f :-> g where
        Natural :: (Functor f, Functor g) => (forall x. f x -> g x) -> (f :-> g)
        -- a.k.a. Natural :: FunctorInstance f -> FunctorInstance g ->
(forall x. f x -> g x) -> (f :-> g)

then GHC will check the constraints on construction, not use. This is
very close to *existential types* which you may have come across
before.

Note that we have to use "data" here, not "newtype". This is because
to enforce its constraints, GHC must store a copy of the Functor
instances in the data type itself. So the data type ends up with two
extra fields, so it can't be a newtype any more.

> 2. I would have thought that such a weird/broken thing as this would
> only be allowed with -XDatatypeContexts, but in fact it is allowed
> without it. Why?

There are in fact *three* places where you can place a context in a data type:

    -- Datatype contexts (discouraged)
    data Class a => Type a = Constructor a

    -- Existential types
    data Type = forall a. Class a => Constructor a

    -- Higher-rank polymorphism
    newtype Type = Constructor (forall a. Class a => a)

Only the first is discouraged: the others are quite useful.

> David
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- 
https://lambda.xyz