Position of a constraint in a function's signature

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Position of a constraint in a function's signature

Al Zohali
Dear Cafe!

I've encountered quite strange behaviour in GHC (v8.0.2) and I would
like to ask you to give me a hint.

Suppose we have the following functions:
----
foo :: (Show a) => Int -> a -> [String]
foo n = replicate n . show

bar :: Int -> (Show a) => a -> [String]
bar n = replicate n . show

baz :: Int -> a -> (Show a) => [String]
baz n = replicate n . show
----

This won't compile, and that is ok. But if we add `RankNTypes`
extension, this will compile and (:t) will give us the same signature
for all three functions.

There are two things I cannot get:

1) Why do this even compile?
I saw constraints being defined either in the beginning of a signature
or right after `forall` expression. I thought that it was a rule (or
convention), but it's not. Is this way of declaring constraints (in
the middle of a signature) discouraged or can be considered as a bug?

2) Even if this was supposed to be so, why was the constraint in `baz`
hoisted to the top?
There are at least two ways to interpret that signature:
----
baz :: Int -> a -> forall a. (Show a) => [String]
baz :: forall a. (Show a) => Int -> a -> [String]
----
Is there any reason why the second one was chosen?
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Position of a constraint in a function's signature

Brandon Allbery
There's a number of weirdnesses currently that basically fall out of the fact that the kinds Constraint and * are treated identically internally. See https://ghc.haskell.org/trac/ghc/ticket/11715 and stay tuned; it's not going to be fixed for 8.2 but probably will for 8.4 --- unless more bugs come crawling out of the woodwork, as has been happening a lot if you look at the ticket history. :)

On Mon, May 15, 2017 at 5:09 PM, Al Zohali <[hidden email]> wrote:
Dear Cafe!

I've encountered quite strange behaviour in GHC (v8.0.2) and I would
like to ask you to give me a hint.

Suppose we have the following functions:
----
foo :: (Show a) => Int -> a -> [String]
foo n = replicate n . show

bar :: Int -> (Show a) => a -> [String]
bar n = replicate n . show

baz :: Int -> a -> (Show a) => [String]
baz n = replicate n . show
----

This won't compile, and that is ok. But if we add `RankNTypes`
extension, this will compile and (:t) will give us the same signature
for all three functions.

There are two things I cannot get:

1) Why do this even compile?
I saw constraints being defined either in the beginning of a signature
or right after `forall` expression. I thought that it was a rule (or
convention), but it's not. Is this way of declaring constraints (in
the middle of a signature) discouraged or can be considered as a bug?

2) Even if this was supposed to be so, why was the constraint in `baz`
hoisted to the top?
There are at least two ways to interpret that signature:
----
baz :: Int -> a -> forall a. (Show a) => [String]
baz :: forall a. (Show a) => Int -> a -> [String]
----
Is there any reason why the second one was chosen?
_______________________________________________
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.



--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Position of a constraint in a function's signature

Will Yager
In reply to this post by Al Zohali
Disclaimer: My understanding of this may be out of date/incomplete. My understanding of Haskell typing is largely based on https://web.cecs.pdx.edu/~mpj/thih/thih.pdf which is old and doesn't contain RankNTypes.

1)

Why wouldn't it compile?

"C => T" means (or is equivalent to) "A function which takes an implicit parameter C and returns a T". There's no particular reason this can't show up on the RHS of a "->" arrow.

Admittedly, no one really uses typeclasses in this way, but it's not fundamentally wrong.

2)

I don't believe the former interpretation of baz is valid. The "a" on its own and the one in "Show a" ought to be unified.

When you quantify an unquantified type, you do it over the *entire* type, not just the variables that show up in constraints. There's no reason you would insert a "forall" in the RHS of an arrow.

--Will



On Mon, May 15, 2017 at 4:09 PM, Al Zohali <[hidden email]> wrote:
Dear Cafe!

I've encountered quite strange behaviour in GHC (v8.0.2) and I would
like to ask you to give me a hint.

Suppose we have the following functions:
----
foo :: (Show a) => Int -> a -> [String]
foo n = replicate n . show

bar :: Int -> (Show a) => a -> [String]
bar n = replicate n . show

baz :: Int -> a -> (Show a) => [String]
baz n = replicate n . show
----

This won't compile, and that is ok. But if we add `RankNTypes`
extension, this will compile and (:t) will give us the same signature
for all three functions.

There are two things I cannot get:

1) Why do this even compile?
I saw constraints being defined either in the beginning of a signature
or right after `forall` expression. I thought that it was a rule (or
convention), but it's not. Is this way of declaring constraints (in
the middle of a signature) discouraged or can be considered as a bug?

2) Even if this was supposed to be so, why was the constraint in `baz`
hoisted to the top?
There are at least two ways to interpret that signature:
----
baz :: Int -> a -> forall a. (Show a) => [String]
baz :: forall a. (Show a) => Int -> a -> [String]
----
Is there any reason why the second one was chosen?
_______________________________________________
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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Position of a constraint in a function's signature

Brandon Allbery

On Mon, May 15, 2017 at 6:55 PM, William Yager <[hidden email]> wrote:
"C => T" means (or is equivalent to) "A function which takes an implicit parameter C and returns a T". There's no particular reason this can't show up on the RHS of a "->" arrow.

The Report requires that all constraints be in a tuple before the rest of a signature. ghc relaxes this since it implements not Haskell 2010, but System FC. But yes, this is why it's syntactically correct once you enable any extension that liberalizes type signature parsing. (Even without, ghc permits constraint => constraint ... => type for reasons that iirc are hard to "fix" and are not really considered bugs, just not Haskell 2010 syntax; but ghc's Haskell 2010 support broke when Num lost Eq and Show superclasses, and broke further when Monad gained Applicative prerequisite/"superclass", so nobody's much worried about the Report violation.)

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
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.