Reputation: 1094
I want to do something like: (In pseudocode; this does not compile)
type Num a => Vector2d = (a,a)
or possibly
type Num a => Vector2d a = (a,a)
But I cannot do this.
After reading up I have a feeling that to achieve this I need the RankNTypes
extension or the forall
keyword, but I just can't wrap my mind around this...
Can anyone help?
EDIT:
I managed, but rather by "guessing around syntax":
The solution is, indeed with RankNTypes
:
type Vec = forall a. Num a => (a,a)
This works, but with the RankNTypes
extension
type Vec = Num a => (a,a)
works equally. What's the difference, and how does a Num a =>
constraint, which seems quite natural, relate to rank n types?
So the question is still open, but I'm looking for an explanation, rather than a solution.
Upvotes: 3
Views: 203
Reputation: 30103
type Vec = forall a. Num a => (a, a)
is the same thing as
type Vec = Num a => (a, a)
.
The reason is that every type variable without a corresponding forall
is implicitly introduced by GHC at the topmost type variable scope, for example:
const :: a -> b -> a
const :: forall a b. a -> b -> a -- the same thing
For the most part type synonyms are just syntactic convenience, so whenever you see Vec
in a type signature, you can just put parentheses around its definition and substitute:
Vec -> Vec -> Integer
-- equals:
(forall a. Num a => (a, a)) -> (forall a. Num a => (a, a)) -> Integer
There is one weird exception, where you can't just blindly substitute in the types. If you have a type synonym like this:
type Vec a = Num a => (a, a)
then the Num
constraint floats out to the outermost scope after substitution:
vec = (100, 100) :: Vec Integer
-- vec has now type "(Integer, Integer)"
and multiple constraints on the same type variable merge:
addVec :: Vec a -> Vec a -> Vec a
addVec (a, b) (c, d) = (a + c, b + d)
-- addVec has now effectively type "Num a => (a, a) -> (a, a) -> (a, a)
In the above cases the class constraint didn't introduce higher-rankedness, because the constraints were bound to variables in the outer scope. However, when we use the synonym inside data constructors, the constraint turns into an implicit (existential) dictionary:
type Foo a = Num a => a
data Bar a = Bar (Foo a) -- equals "data Bar a = Bar (Num a => a)"
-- requires ExistentialQuantifiaction or GADTs to compile
-- and of course, any data constructor blocks the outwards floating of the constraint:
type Baz = a -> (Foo a, ()) -- requires ImpredicativeTypes.
So, to summarize, the behaviour of these kinds of constraints in type synonyms is rather wobbly. We need RankNTypes
or Rank2Types
to write them out, but this seems to be more of an implementation artifact than anything else. We could argue that the syntax can be used to introduce quantifiers to types, and this sort of justifies the RankNType
requirement, but we could equally say that it's reasonable that the compiler should detect whether there are fresh quantifiers or not, and proceed accordingly (like it's already being done with the introduced existentials...).
Upvotes: 6