[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Richard Eisenberg]

The intended semantics here is from the paper (https://richarde.dev/papers/2018/pat-tyvars/pat-tyvars.pdf). See the paragraph right before section 5.6, which describes the change from the outdated documentation (saying that each scoped type variable must refer to a distinct variable) to the current implementation (where a scoped type variable can stand for any type).

The idea behind the change is that, when we write f x = not x, we intend for x to stand for any Bool. So, when we write f (x :: a) = not x, we should allow a to stand for any type -- in this case, it will stand for Bool.

Going back to Tom's original post, suggesting a refinement: consider

data Ex2 = forall a. Ex2 a a
f (Ex2 (x :: b) (y :: c)) = False

Is that accepted or rejected? I think Tom's rules would accept, because neither b nor c are bound to a variable from an outer scope. Yet this suggests that b and c are different. Or what about

data Eql = forall a. (a ~ Int) => Eql a
g :: Eql -> Int
g (Eql (x :: b)) = x + x

Hrm. Now it seems we can allow `b` to stand for `a`... but `a` is also the same as Int. So that's confusing. We could also have `a` equal a type variable from an outer scope, thus circumventing the check Tom wants to introduce. It all gets very murky. Simplest to allow variables in that position unify with any type, as GHC is today.

Regardless, the documentation must be updated. Thanks for making the ticket.

Richard

> On Aug 21, 2020, at 8:29 PM, Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
> 
> On Fri, Aug 21, 2020 at 06:13:23PM -0500, Alexis King wrote:
> 
>>> On Aug 19, 2020, at 18:22, Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
>>> 
>>> Though perhaps much too careful/complete a read of the documentation is
>>> needed to see support in the documentation for the conclusions I
>>> ultimately reached, I do believe that the text is on some level there
>> 
>> I do not agree with your interpretation. :)
> 
> Fair enough, the text is ultimately not clear.  [ TL;DR the rest is
> inessential detail for the morbidly curious. ]
> 
>>> But when we get to "9.17.4. Pattern type signatures" […] we see that
>>> are they are rather different beasts, that deviate from the
>>> description in the overview.  In particular, "2" no longer holds,
>>> because these are neither generalised, nor universally quantified.
>> 
>> It is true that such variables are not generalized, but the
>> documentation does not say “generalized”—it says rigid. If we consider
>> that the primary purpose of this feature is to bring existentials into
>> scope, then there is no violation of the principle when used in the
>> intended way. After all, existentials brought into scope via `case`
>> are very much rigid (and distinct from all other variables).
> 
> The leap I was making is that it is specifically universal
> quantification that leaves the design no choice but to make the
> variables rigid.  With "forall a b." naturally "a" and "b" vary
> *independently*, and so must be kept distinct.
> 
> On the other hand, given that Pattern Type Signatures are not
> universally quantified, there is no longer a *prior requirement* to keep
> them distinct, and so I am ultimately not surprised that they may not be
> rigid in the same way as those brought into scope via "forall", indeed
> we can now (as of GHC 8.8) write:
> 
>    foo :: Int -> Int -> String
>    foo (x :: a) (y :: b) = "(" ++ (show @a x) ++ ", " ++ (show @b y) ++ ")"
> 
>    λ> foo 1 2
>    "(1, 2)"
> 
> where "a" becomes a synonym for "Int" and so does "b", and so are surely
> not distinct types.  But even with GHC 8.0 (7.10 and perhaps older would
> also be OK were this example changed to avoid TypeApplications), we can
> write:
> 
>    foo :: Show c => c -> c -> String
>    foo (x :: a) (y :: b) = "(" ++ (show @a x) ++ ", " ++ (show @b y) ++ ")"
> 
>    λ> foo 1 2
>    "(1, 2)"
> 
> where "a" and "b" are aliases for "c".  I don't think you disagree that
> this is what the actual implementation is doing.  My point was just that
> with some effort one might read the actual behaviour as consistent with
> the spirit of the documentation, and that the leap required to read it
> that way may not be too great.
> 
>> It is true that GHC implements a much more flexible behavior that
>> allows entirely different things to be brought into scope. But that is
>> just part of the divergence from the documentation—there’s nothing
>> that says pattern signatures are exempt from that restriction. It only
>> states that pattern signatures that refer to unbound variables bring
>> those variables into scope, nothing more.
> 
> Yes, the literal text does not actually carve out an exception, I'm
> making a retroactive extrapolation from the inferred constraints on
> the implementation given the context.
> 
>> Of course, this is all somewhat immaterial—there is no way to
>> objectively determine which interpretation is “correct,” and the docs
>> are unambiguously unclear regardless, so they should be changed. But
>> purely as a matter of friendly debate, I stand by my interpretation.
> 
> Yes it would be nice for someone to craft a proposed change to the docs.
> Any volunteers?
> 
> My attempt to read the docs liberally was largely in order to better
> understand the actual implementation and to intuit how and why the
> actual choice was made, and might be seen to be consistent with the
> overall design.
> 
> -- 
>    Viktor.
> _______________________________________________
> 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.