[Haskell-cafe] More Nested =>s (was: On finding the right exposition...)

[Richard Eisenberg]

Because things on the internet live forever, I want to correct a few small misunderstandings here:

> On Oct 5, 2021, at 1:28 AM, Anthony Clayden <anthony.d.clayden at gmail.com> wrote:
> `-XRankNTypes` enables something called Rank 1 types, which accepts this:
The -XRankNTypes extension is a bit of an unfortunate name.

My best understanding is:

Ranks are cumulative: all rank-0 types are rank-1 types, all rank-0 and rank-1 types are rank-2 types, etc.

A rank-0 type has no quantification (that is, no "forall", implicit or explicit). Examples:
> ex1 :: Int -> Int
> ex2 :: Bool -> String -> [Int]
Non-examples:
> ex3 :: [a] -> Int
> ex4 :: String -> a
> ex5 :: forall a. a -> a
> ex6 :: a -> Bool
> ex7 :: (forall a. a -> a -> a) -> Int -> Int

A rank-1 type includes the above and can quantify type variables only at the top level or to the right of arrows. (That is, the `forall` can be the right child of an arrow node in the abstract syntax tree.) Examples:
> ex8 :: a -> a
> ex9 :: forall a. a -> a
> ex10 :: a -> b -> a
> ex11 :: forall a. forall b. a -> b -> a
> ex12 :: forall a. a -> forall b. b -> a
> ex13 :: Int -> forall a. a -> a -> a
> ex14 :: forall a. Int
Non-examples:
> ex15 :: (forall a. a -> a -> a) -> Int -> Int
> ex16 :: (forall a b. a -> b -> a) -> Int

A rank-2 type includes the above and can quantify type variables to the left of one arrow. (That is, the `forall` can be within the left child of an arrow node in the abstract syntax tree, as long as that arrow node is not within the left child of any other arrow node.) Examples:
> ex17 :: (forall a. a -> a -> a) -> Int -> Int
> ex18 :: (forall a b. a -> b -> a) -> ()
> ex19 :: forall r. (forall a. a -> a -> r) -> r
> ex20 :: Int -> (forall a. a -> a -> a) -> Int
> ex21 :: (Int -> forall a. a -> a) -> Bool
Non-example:
> ex21 :: ((forall a. a -> a) -> Int) -> Bool

A rank-3 type includes the above and can quantify type variables to the left of two arrows. (That is, the `forall` can be within the left child of an arrow node that is within the left child of an arrow node, as long as that last arrow node is not within the left child of any other arrow node.) Example:
> ex22 :: ((forall a. a -> a) -> Int) -> Bool
Non-example:
> ex23 :: Int -> (((forall a. a -> a) -> Bool) -> Double) -> Char

And so on.

GHC considers constraint quantification (that is, =>) to be similar to variable quantification. So, in GHC parlance, we lump any constraints in with variable quantification when considering the rank of a type. We would thus consider
> ex24 :: forall a. (Show a => a -> a) -> a -> String
to be a rank-2 type, even though a type theorist would call it a rank-1 type.

Haskell98 allows a subset of rank-1 types; this subset uses what is called prenex quantification. A prenex-quantified type has all of its variable (and, in GHC, constraint) quantification all the way at the top, not under any arrows at all. Examples of prenex quantification:
> ex25 :: a -> a
> ex26 :: forall a b. a -> b -> a
> ex27 :: Show a => a -> String
Non-examples:
> ex28 :: Int -> forall a. a -> a
> ex29 :: Show a => Ord a => a -> Int

GHC's -XRankNTypes extension allows types of arbitrary rank, and those which are non-prenex.

So,
> ex30 :: Show a => Num a => Eq a => a -> a -> Bool
is rank-1, but it is non-prenex. It thus requires the -XRankNTypes extension. This is why RankNTypes is perhaps a poor name: it does more than allow higher-rank types. It allows non-prenex types, too. (All types higher that are not rank-1 are also non-prenex.)
> 
> >    foo :: Ord a => Num b => a -> Show b => b
As AntC says, this type is rank-1, and yet it needs -XRankNTypes. However, all prenex rank-1 types are accepted without any extension.
> >    bar :: forall a. forall {- empty -}. forall b. blah
> >    -- bar :: forall a b. blah   -- equivalent
These are mostly equivalent. The only difference is how -XScopedTypeVariables treats them: the first one will bring `a` into scope in the body of `bar`, while the second has both `a` and `b` in scope in the body of `bar`.

> 
> But `PatternSynonyms` drives a cart and horses through that:
Yes! Pattern synonym type signatures are not types. They are Something Else, which I'll call a patsyn-type. A patsyn-type has 6 components:
 - Universally quantified variables are inputs to the pattern. We must know how to instantiate these to use the pattern.
 - Required constraints are inputs to the pattern. We must satisfy these constraints to use the pattern.
 - Existentially quantified variables are outputs of the pattern. After the pattern match is successful, these type variables are bound.
 - Provided constraints are outputs of the pattern. After the pattern match is successful, we can assume the truth of these constraints.
 - Arguments are the types of the variables bound by the pattern.
 - The result type of the pattern is the type of the thing being pattern-matched against (aka the "scrutinee").

>  you must have exactly 2 `... => ... => ...`
Not quite:
- If you have 0 =>s, then we assume that there are no required constraints, no existentially quantified variables, and no provided constraints.
- If you have 1 =>, then the constraints to its left are required. Any forall to its immediate right lists the existentially quantified variables. There are no provided constraints.
- If you have 2 =>s, then the constraints to the left of the first one are the required ones, the constraints to the left of the second one are the provided ones.
- If you have 3 or more =>s, then the result type is a quantified type. This is quite strange, but possible, if you, say, have a view pattern whose function has a higher-rank type:


> data Eqy a = Eq a => MkEqy
> 
> blah :: (Num a => a) -> Eqy a
> blah _ = undefined
> 
> pattern P :: Show a => Eq a => Num a => a
> pattern P <- (blah -> MkEqy)

This is accepted by GHC 8.10.5.
>  and exactly 2 `forall`s (possibly empty) -- that is, if you explicitly quantify at all. Or you can go:
> 
> >    MyPat :: Num a =>          a -> Baz a      -- which is shorthand for
> >    MyPat :: Num a => ()    => a -> Baz a      -- which is equiv to
Yes. These signatures are equivalent.


> >    MyPat :: Num a => Num a => a -> Baz a
But this is something else. This MyPat has a provided constraint Num a, where as the others did not.


> >    MyPat :: ()    => Num a => a -> Baz a      -- this means something different

This is also something else: this has no required constraint at all.

I hope this is helpful!
Richard

> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20211005/94efffad/attachment.html>