Confused about type seen in the wild

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

Confused about type seen in the wild

Alexander Solla
I'm using the yesod-markdown package as a "template" for making my own yesod-mathjax package.  I'm pretty much done, and it does compile now, but I'm just really confused by a type that looks like bad syntax.  In fact, I ended up trying to "fix" it, which lead to errors:

mathJaxField :: Monad m 
             => RenderMessage (HandlerSite m) FormMessage 
             => Field m MathJax

Notice that there are two type arrows (=>).  Interestingly,

mathJaxField :: ( Monad m 
                , RenderMessage (HandlerSite m) FormMessage
                ) => Field m MathJax

compiles too.  So it looks like currying/uncurrying, at the type level.  But when did this start?  I'm using GHC 7.6.3

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Albert Y. C. Lai
On 14-04-08 11:11 PM, Alexander Solla wrote:

> mathJaxField  ::  Monad  m
>
>               =>  RenderMessage  (HandlerSite  m)  FormMessage
>
>               =>  Field  m  MathJax
>
>
> Notice that there are two type arrows (=>).  Interestingly,
>
>
> mathJaxField  ::  (Monad  m
>
>
>                  ,  RenderMessage  (HandlerSite  m)  FormMessage
>
>
>                  )  =>  Field  m  MathJax
>
>
>
> compiles too.  So it looks like currying/uncurrying, at the type level.  But when did this start?  I'm using GHC 7.6.3

Yes, GHC accepts "X => Y => Z" and makes it "(X, Y) => Z". In fact, go
wilder:

whee :: Show a => Eq a => a => Bool
whee x = x == x && null (show x)

It is valid and it means (Show a, Eq a) => a -> Bool. Try it!

My understanding is that when the type checker has to support all those
generalizations like ConstraintKind, DataKinds, etc etc, it becomes so
general that some traditional distinctions vanish.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Jason Dagit-3



On Thu, Apr 10, 2014 at 9:27 AM, Albert Y. C. Lai <[hidden email]> wrote:
 
Yes, GHC accepts "X => Y => Z" and makes it "(X, Y) => Z". In fact, go wilder:

whee :: Show a => Eq a => a => Bool
whee x = x == x && null (show x)

It is valid and it means (Show a, Eq a) => a -> Bool. Try it!

What extensions do you have turned on? I'm trying this is ghci (7.6.3) and I can't get it to work even with DataKinds and ConstraintKinds.

Jason

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Kim-Ee Yeoh
Administrator
No problems here:

# ghci
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> let whee :: Show a => Eq a => a => Bool; whee x = x == x && null (show x)
Prelude> :t whee
whee :: (Eq a, Show a) => a -> Bool

-- Kim-Ee

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Jason Dagit-3



On Thu, Apr 10, 2014 at 10:21 AM, Kim-Ee Yeoh <[hidden email]> wrote:
No problems here:

# ghci
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> let whee :: Show a => Eq a => a => Bool; whee x = x == x && null (show x)
Prelude> :t whee
whee :: (Eq a, Show a) => a -> Bool

It seems to be an issue with giving everything on a single line:

$ ghci
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude λ> let whee x = x == x && null (show x) :: Show a => Eq a => a => Bool

<interactive>:2:14:
    Couldn't match expected type `a -> Bool' with actual type `Bool'
    In the expression:
        x == x && null (show x) :: Show a => Eq a => a => Bool
    In an equation for `whee':
        whee x = x == x && null (show x) :: Show a => Eq a => a => Bool

I see now to make it work as a one liner I could do it this way:
Prelude λ> :t (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool
(\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool
  :: (Eq a, Show a) => a -> Bool

Thanks!

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Felipe Lessa
In reply to this post by Albert Y. C. Lai
Em 10-04-2014 13:27, Albert Y. C. Lai escreveu:

> Yes, GHC accepts "X => Y => Z" and makes it "(X, Y) => Z". In fact, go
> wilder:
>
> whee :: Show a => Eq a => a => Bool
> whee x = x == x && null (show x)
>
> It is valid and it means (Show a, Eq a) => a -> Bool. Try it!
>
> My understanding is that when the type checker has to support all those
> generalizations like ConstraintKind, DataKinds, etc etc, it becomes so
> general that some traditional distinctions vanish.
What?  Shouldn't that be a bug?

$ ghci -XHaskell98
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> let f :: a => a; f = id

<interactive>:2:15:
    Predicate `a' used as a type
    In the type signature for `f': f :: a => a
Prelude> let f :: Eq a => a => a; f = id

Not even with Haskell98 turned on!

--
Felipe.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (919 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Brandon Allbery
On Thu, Apr 10, 2014 at 1:43 PM, Felipe Lessa <[hidden email]> wrote:
Em 10-04-2014 13:27, Albert Y. C. Lai escreveu:
> My understanding is that when the type checker has to support all those
> generalizations like ConstraintKind, DataKinds, etc etc, it becomes so
> general that some traditional distinctions vanish.

What?  Shouldn't that be a bug?

It "should be" but I suspect actually treating it as one is rather difficult now that it's possible for `a` there to be a Constraint or etc., in which case it is on the correct side of the =>. 

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Kim-Ee Yeoh
Administrator
In reply to this post by Jason Dagit-3

On Fri, Apr 11, 2014 at 12:28 AM, Jason Dagit <[hidden email]> wrote:
It seems to be an issue with giving everything on a single line:

Prelude λ> let whee x = x == x && null (show x) :: Show a => Eq a => a => Bool

<interactive>:2:14:
    Couldn't match expected type `a -> Bool' with actual type `Bool'
    In the expression:
        x == x && null (show x) :: Show a => Eq a => a => Bool
    In an equation for `whee':
        whee x = x == x && null (show x) :: Show a => Eq a => a => Bool

As the error message indicates, the (:: type) is being applied to the open term: x == x && null (show x), and not to the function whee.
 
To do this single-line def properly, I think you need -XScopedTypeVariables:

    let whee (x :: a) = x == x && null (show x) :: Show a => Eq a => Bool



I see now to make it work as a one liner I could do it this way:
Prelude λ> :t (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool
(\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool
  :: (Eq a, Show a) => a -> Bool

And to recover the named binding:

    let whee = (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool


-- Kim-Ee

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Felipe Lessa
In reply to this post by Brandon Allbery
Em 10-04-2014 14:45, Brandon Allbery escreveu:
> It "should be" but I suspect actually treating it as one is rather
> difficult now that it's possible for `a` there to be a Constraint or
> etc., in which case it is on the correct side of the =>.

What you're saying is that it would be difficult to ban this on the
parser level.  However, somewhere inside GHC this `a` that was used as a
constraint got promoted to being an argument.  This is where it should
have been stopped on its track.

Or am I missing something? =)

--
Felipe.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (919 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Brandon Allbery
On Thu, Apr 10, 2014 at 1:59 PM, Felipe Lessa <[hidden email]> wrote:
Em 10-04-2014 14:45, Brandon Allbery escreveu:
> It "should be" but I suspect actually treating it as one is rather
> difficult now that it's possible for `a` there to be a Constraint or
> etc., in which case it is on the correct side of the =>.

What you're saying is that it would be difficult to ban this on the
parser level.  However, somewhere inside GHC this `a` that was used as a
constraint got promoted to being an argument.  This is where it should
have been stopped on its track.

Actually, what I'm saying is that it might be difficult to reliably catch it at that point; consider that the parse leading to that interpretation may not exist within ghc at that point, only an AST that may have been rearranged by uses of ConstraintKinds so as to lose its direct relationship to the parse that initially led to it.

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Jason Dagit-3
In reply to this post by Kim-Ee Yeoh



On Thu, Apr 10, 2014 at 10:45 AM, Kim-Ee Yeoh <[hidden email]> wrote:

And to recover the named binding:

    let whee = (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool

Right, or even:
Prelude λ> :t let whee x = x == x && null (show x) in whee :: Show a => Eq a => a => Bool
let whee x = x == x && null (show x) in whee :: Show a => Eq a => a => Bool
  :: (Eq a, Show a) => a -> Bool

Which is what I think I meant to type initially but then confused myself and also misread the type error :)

Jason


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Brandon Allbery
In reply to this post by Brandon Allbery
On Thu, Apr 10, 2014 at 2:03 PM, Brandon Allbery <[hidden email]> wrote:
Actually, what I'm saying is that it might be difficult to reliably catch it at that point; consider that the parse leading to that interpretation may not exist within ghc at that point, only an AST that may have been rearranged by uses of ConstraintKinds so as to lose its direct relationship to the parse that initially led to it.

Or worse, this is happening inside the typechecker and the tree it's manipulating has *no* relationship to the original parse or its AST, such that it has no idea whether it was on the wrong side of an =>. Depends on the internal representations used by the typechecker, and most likely doing it right means carrying around a lot more information than it currently does.

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Andres Löh
I also find this scary. Even this works:

Prelude> let whee :: (Show a, Eq a, a) => Bool; whee x = x == x && null (show x)
Prelude> :t whee
whee :: (Eq a, Show a) => a -> Bool

But:

Prelude> let test :: (Eq a) => a => b => a; test = undefined

<interactive>:35:13:
    Illegal polymorphic or qualified type: (b) => a
    Perhaps you intended to use -XRankNTypes or -XRank2Types
    In the type signature for `test': test :: Eq a => a => b => a
Prelude> :set -XRankNTypes
Prelude> let test :: (Eq a) => a => b => a; test = undefined

<interactive>:8:13:
    Illegal constraint: b (Use -XConstraintKinds to permit this)
    In the type signature for `test': test :: Eq a => a => b => a

So this is what I'd also expect for "a" to happen. I think this is a bug.

Cheers,
  Andres

--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Andres Löh
And even more:

Prelude> let test :: (Eq a, a, Eq b, b) => a; test = const
Prelude> :t test
test :: (Eq a, Eq b) => a -> b -> a
Prelude> let test :: (Eq a, Eq b, a, b) => a; test = const
Prelude> :t test
test :: (Eq a, Eq b) => a -> b -> a
Prelude> let test :: (a, b, Eq a, Eq b) => a; test = const

<interactive>:19:35:
    Predicate `a' used as a type
    In the type signature for `test': test :: (a, b, Eq a, Eq b) => a

Cheers,
  Andres

--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Andres Löh
Sorry for continuing to reply to myself. But all this seems fixed in 7.8.1:

Prelude> let whee :: (Show a, Eq a, a) => Bool; whee x = x == x && null (show x)

<interactive>:5:28:
    Expected a constraint, but 'a' has kind '*'
    In the type signature for 'whee': whee :: (Show a, Eq a, a) => Bool
Prelude> let whee :: (Show a, Eq a) => a => Bool; whee x = x == x &&
null (show x)

<interactive>:6:31:
    Expected a constraint, but 'a' has kind '*'
    In the type signature for 'whee':
      whee :: (Show a, Eq a) => a => Bool

Cheers,
  Andres

On Thu, Apr 10, 2014 at 8:37 PM, Andres Löh <[hidden email]> wrote:

> And even more:
>
> Prelude> let test :: (Eq a, a, Eq b, b) => a; test = const
> Prelude> :t test
> test :: (Eq a, Eq b) => a -> b -> a
> Prelude> let test :: (Eq a, Eq b, a, b) => a; test = const
> Prelude> :t test
> test :: (Eq a, Eq b) => a -> b -> a
> Prelude> let test :: (a, b, Eq a, Eq b) => a; test = const
>
> <interactive>:19:35:
>     Predicate `a' used as a type
>     In the type signature for `test': test :: (a, b, Eq a, Eq b) => a
>
> Cheers,
>   Andres
>
> --
> Andres Löh, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com
>
> Registered in England & Wales, OC335890
> 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England



--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Alexander Solla
On Thu, Apr 10, 2014 at 11:40 AM, Andres Löh <[hidden email]> wrote:
Sorry for continuing to reply to myself. But all this seems fixed in 7.8.1:

Prelude> let whee :: (Show a, Eq a, a) => Bool; whee x = x == x && null (show x)

<interactive>:5:28:
    Expected a constraint, but 'a' has kind '*'
    In the type signature for 'whee': whee :: (Show a, Eq a, a) => Bool
Prelude> let whee :: (Show a, Eq a) => a => Bool; whee x = x == x &&
null (show x)

I don't have a GHC 7.8 handy.  Can you check to see if:

whee :: Show a => Eq a => (a -> Bool) 

works over there? 

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Andres Löh
> I don't have a GHC 7.8 handy.  Can you check to see if:
>
> whee :: Show a => Eq a => (a -> Bool)
>
> works over there?

Yes, it does. I also see no problem with this one. Even this works
(but funnily enough, it requires RankNTypes, even though it translates
to the same type):

let whee :: a -> Show a => Eq a => Bool; whee = undefined

None of these are kind errors though. And while I don't know if it's
clearly specified what exactly is possible, it makes sense to me to
allow these.

Cheers,
  Andres

--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Niklas Haas
In reply to this post by Alexander Solla
On Thu, 10 Apr 2014 11:44:25 -0700, Alexander Solla <[hidden email]> wrote:
> On Thu, Apr 10, 2014 at 11:40 AM, Andres Löh <[hidden email]> wrote:
> I don't have a GHC 7.8 handy.  Can you check to see if:
>
> whee :: Show a => Eq a => (a -> Bool)
>
> works over there?

It does, see:

> λ let whee :: Show a => Eq a => (a -> Bool); whee x = x == x && null
> (show x)
> λ :t whee
> whee :: (Show a, Eq a) => a -> Bool
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Confused about type seen in the wild

Felipe Lessa
In reply to this post by Andres Löh
Em 10-04-2014 15:40, Andres Löh escreveu:
> Sorry for continuing to reply to myself. But all this seems fixed in 7.8.1:

Great, thanks!

--
Felipe.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (919 bytes) Download Attachment