[Haskell-cafe] What's the story of this weird type?
Chris Wong
lambda.fairy at gmail.com
Fri Mar 20 22:39:12 UTC 2015
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
More information about the Haskell-Cafe
mailing list