<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Because things on the internet live forever, I want to correct a few small misunderstandings here:<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 5, 2021, at 1:28 AM, Anthony Clayden <<a href="mailto:anthony.d.clayden@gmail.com" class="">anthony.d.clayden@gmail.com</a>> wrote:</div><div class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">`-XRankNTypes` enables something called Rank 1 types, which accepts this:</font></pre></div></div></blockquote><div>The -XRankNTypes extension is a bit of an unfortunate name.</div><div><br class=""></div><div>My best understanding is:</div><div><br class=""></div><div>Ranks are cumulative: all rank-0 types are rank-1 types, all rank-0 and rank-1 types are rank-2 types, etc.</div><div><br class=""></div><div>A rank-0 type has no quantification (that is, no "forall", implicit or explicit). Examples:</div><div>> ex1 :: Int -> Int</div><div>> ex2 :: Bool -> String -> [Int]</div><div>Non-examples:</div><div>> ex3 :: [a] -> Int</div><div>> ex4 :: String -> a</div><div>> ex5 :: forall a. a -> a</div><div>> ex6 :: a -> Bool</div><div>> ex7 :: (forall a. a -> a -> a) -> Int -> Int</div><div><br class=""></div><div>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:</div><div>> ex8 :: a -> a</div><div>> ex9 :: forall a. a -> a</div><div>> ex10 :: a -> b -> a</div><div>> ex11 :: forall a. forall b. a -> b -> a</div><div>> ex12 :: forall a. a -> forall b. b -> a</div><div>> ex13 :: Int -> forall a. a -> a -> a</div><div>> ex14 :: forall a. Int</div><div>Non-examples:</div><div>> ex15 :: (forall a. a -> a -> a) -> Int -> Int</div><div>> ex16 :: (forall a b. a -> b -> a) -> Int</div><div><br class=""></div><div>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:</div><div>> ex17 :: (forall a. a -> a -> a) -> Int -> Int</div><div>> ex18 :: (forall a b. a -> b -> a) -> ()</div><div>> ex19 :: forall r. (forall a. a -> a -> r) -> r</div><div>> ex20 :: Int -> (forall a. a -> a -> a) -> Int</div><div>> ex21 :: (Int -> forall a. a -> a) -> Bool</div><div>Non-example:</div><div>> ex21 :: ((forall a. a -> a) -> Int) -> Bool</div><div><br class=""></div><div>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:</div><div>> ex22 :: ((forall a. a -> a) -> Int) -> Bool</div><div>Non-example:</div><div>> ex23 :: Int -> (((forall a. a -> a) -> Bool) -> Double) -> Char</div><div><br class=""></div><div>And so on.</div><div><br class=""></div><div>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</div><div>> ex24 :: forall a. (Show a => a -> a) -> a -> String</div><div>to be a rank-2 type, even though a type theorist would call it a rank-1 type.</div><div><br class=""></div><div>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:</div><div>> ex25 :: a -> a</div><div>> ex26 :: forall a b. a -> b -> a</div><div>> ex27 :: Show a => a -> String</div><div>Non-examples:</div><div>> ex28 :: Int -> forall a. a -> a</div><div>> ex29 :: Show a => Ord a => a -> Int</div><div><br class=""></div><div>GHC's -XRankNTypes extension allows types of arbitrary rank, and those which are non-prenex.</div><div><br class=""></div><div>So,</div><div>> ex30 :: Show a => Num a => Eq a => a -> a -> Bool</div><div>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.)</div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""><br class=""></font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> foo :: Ord a => Num b => a -> Show b => b</font></pre></div></div></blockquote><div>As AntC says, this type is rank-1, and yet it needs -XRankNTypes. However, all prenex rank-1 types are accepted without any extension.</div><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> bar :: forall a. forall {- empty -}. forall b. blah</font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> -- bar :: forall a b. blah -- equivalent</font></pre></div></blockquote><div>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`.</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""><br class=""></font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">But `PatternSynonyms` drives a cart and horses through that:</font></pre></div></blockquote><div>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:</div><div> - Universally quantified variables are inputs to the pattern. We must know how to instantiate these to use the pattern.</div><div> - Required constraints are inputs to the pattern. We must satisfy these constraints to use the pattern.</div><div> - Existentially quantified variables are outputs of the pattern. After the pattern match is successful, these type variables are bound.</div><div> - Provided constraints are outputs of the pattern. After the pattern match is successful, we can assume the truth of these constraints.</div><div> - Arguments are the types of the variables bound by the pattern.</div><div> - The result type of the pattern is the type of the thing being pattern-matched against (aka the "scrutinee").</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""> you must have exactly 2 `... => ... => ...`</font></pre></div></blockquote><div>Not quite:</div><div>- If you have 0 =>s, then we assume that there are no required constraints, no existentially quantified variables, and no provided constraints.</div><div>- 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.</div><div>- 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.</div><div>- 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:</div><div><br class=""></div><div><br class=""><blockquote type="cite" class="">data Eqy a = Eq a => MkEqy<br class=""><br class="">blah :: (Num a => a) -> Eqy a<br class="">blah _ = undefined<br class=""><br class="">pattern P :: Show a => Eq a => Num a => a<br class="">pattern P <- (blah -> MkEqy)</blockquote><br class=""></div><div>This is accepted by GHC 8.10.5.</div><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""> and exactly 2 `forall`s (possibly empty) -- that is, if you explicitly quantify at all. Or you can go:</font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""><br class=""></font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> MyPat :: Num a => a -> Baz a -- which is shorthand for</font></pre><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> MyPat :: Num a => () => a -> Baz a -- which is equiv to</font></pre></div></blockquote><div>Yes. These signatures are equivalent.</div><div><br class=""></div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> MyPat :: Num a => Num a => a -> Baz a</font></pre></div></blockquote><div>But this is something else. This MyPat has a provided constraint Num a, where as the others did not.</div><div><br class=""></div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class="">> MyPat :: () => Num a => a -> Baz a -- this means something different</font></pre></div></blockquote><div><br class=""></div><div>This is also something else: this has no required constraint at all.</div><div><br class=""></div><div>I hope this is helpful!</div><div>Richard</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><pre style="white-space: pre-wrap;" class=""><font face="arial, sans-serif" class=""><br class=""></font></pre><pre style="white-space: pre-wrap;" class=""><br class=""></pre></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</blockquote></div><br class=""></body></html>