Hi David,
On Sat, Mar 21, 2015 at 10:21 AM, David Feuer
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe