Francesco Mazzoli | 19 Jun 11:47 2013
Picon

GADTs and pattern matching

Hi list,

I have stumbled upon a strange annoyance:

    {-# LANGUAGE GADTs #-}

    data Foo v where
        Foo :: Foo (Maybe v)

    -- This doesn't work
    foo1 :: a -> Foo a -> Int
    foo1 Nothing  Foo = undefined
    foo1 (Just x) Foo = undefined

    -- This does
    foo2 :: a -> Foo a -> Int
    foo2 x Foo = foo2' x

    foo2' :: Maybe a -> Int
    foo2' Nothing  = undefined
    foo2' (Just x) = undefined

The first definition fails with the error

    Couldn't match expected type `a' with actual type `Maybe t0'
      `a' is a rigid type variable bound by
          the type signature for foo1 :: a -> Foo a -> Int
          at /tmp/foo_flymake.hs:8:9
    In the pattern: Nothing
    In an equation for `foo1': foo1 Nothing Foo = undefined
(Continue reading)

AntC | 19 Jun 12:03 2013
Picon

Re: GADTs and pattern matching

Francesco Mazzoli <f <at> mazzo.li> writes:

> 
> I have stumbled upon a strange annoyance:
> 
>     {-# LANGUAGE GADTs #-}

Hi Francesco, I think you'll find that the 'annoyance' is nothing to do 
with GADTs. I suggest you take the type signature off of foo1, and see 
what type ghc infers for it. It isn't :: a -> Foo a -> Int.

>     data Foo v where
>         Foo :: Foo (Maybe v)
> 
>     -- This doesn't work
>     --  ****  foo1 :: a -> Foo a -> Int
>     foo1 Nothing  Foo = undefined
>     foo1 (Just x) Foo = undefined
  ...

> The first definition fails with the error
> 
>     Couldn't match expected type `a' with actual type `Maybe t0'
 ...
>     In the pattern: Nothing

Yep, that message explains what's going on well enough for me.
Francesco Mazzoli | 19 Jun 12:11 2013
Picon

Re: GADTs and pattern matching

At Wed, 19 Jun 2013 10:03:27 +0000 (UTC),
AntC wrote:
> Hi Francesco, I think you'll find that the 'annoyance' is nothing to do 
> with GADTs. I suggest you take the type signature off of foo1, and see 
> what type ghc infers for it. It isn't :: a -> Foo a -> Int.
> 
> [...]
>
> Yep, that message explains what's going on well enough for me.

Did you read the rest of the code?  That ought to work, because GHC
infers and uses the type equality (something like ‘v ~ Var v1’) and uses
it to coerce the ‘x’.

And, surprise surprise, if the argument order is switched, it works!

    data Foo v where
        Foo :: forall v. Foo (Maybe v)

    foo1 :: Foo a -> a -> Int
    foo1 Foo Nothing  = undefined
    foo1 Foo (Just x) = undefined

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
(Continue reading)

Brent Yorgey | 19 Jun 12:59 2013

Re: GADTs and pattern matching

On Wed, Jun 19, 2013 at 11:11:16AM +0100, Francesco Mazzoli wrote:
> At Wed, 19 Jun 2013 10:03:27 +0000 (UTC),
> AntC wrote:
> > Hi Francesco, I think you'll find that the 'annoyance' is nothing to do 
> > with GADTs. I suggest you take the type signature off of foo1, and see 
> > what type ghc infers for it. It isn't :: a -> Foo a -> Int.
> > 
> > [...]
> >
> > Yep, that message explains what's going on well enough for me.
> 
> Did you read the rest of the code?  That ought to work, because GHC
> infers and uses the type equality (something like ‘v ~ Var v1’) and uses
> it to coerce the ‘x’.
> 
> And, surprise surprise, if the argument order is switched, it works!
> 
>     data Foo v where
>         Foo :: forall v. Foo (Maybe v)
>     
>     foo1 :: Foo a -> a -> Int
>     foo1 Foo Nothing  = undefined
>     foo1 Foo (Just x) = undefined

Yes, I was going to suggest switching the argument order before
reading your message.  This is an interesting way in which you can
observe that Haskell does not really have "multi-argument functions".
All multi-argument functions are really one-argument functions which
return functions.  So a function of type

(Continue reading)

Francesco Mazzoli | 19 Jun 13:08 2013
Picon

Re: GADTs and pattern matching

At Wed, 19 Jun 2013 06:59:00 -0400,
Brent Yorgey wrote:
> Yes, I was going to suggest switching the argument order before
> reading your message.  This is an interesting way in which you can
> observe that Haskell does not really have "multi-argument functions".
> All multi-argument functions are really one-argument functions which
> return functions.  So a function of type
> 
>   foo1 :: a -> (Foo a -> Int)
> 
> must take something of type a (for *any* choice of a, which the caller
> gets to choose) and return a function of type (Foo a -> Int).  *Which*
> function is returned (e.g. one that tries to pattern match on the Foo)
> makes no difference to whether foo1 typechecks.
> 
> On the other hand, a function of type
> 
>   foo2 :: Foo a -> (a -> Int)
> 
> receives something of type Foo a as an argument.  It may pattern-match
> on the Foo a, thus bringing into scope the fact that (a ~ Maybe v).
> Now when constructing the output function of type (a -> Int) it may
> make use of this fact.

Hi Brent,

Thanks for your answer.

I was reminded by shachaf on Haskell a few moments ago about the details
of pattern matching in GHC
(Continue reading)

Felipe Almeida Lessa | 19 Jun 16:42 2013
Picon

Re: GADTs and pattern matching

Brent, maybe I'm misunderstanding what you're saying, but I don't
think that the order of the arguments is playing any role here besides
defining the order in which the pattern matches are desugared.

To illustrate,

  -- This does work
  foo1' :: a -> Foo a -> Int
  foo1' m Foo = case m of
                  Nothing -> undefined
                  Just _  -> undefined

Despite having the same type as foo1, foo1' does work because now I've
pattern matched on the GADT first.  As soon as I do that, its equality
constraint of (a ~ Maybe v) enters into scope of the case branches.

Cheers,

On Wed, Jun 19, 2013 at 7:59 AM, Brent Yorgey <byorgey <at> seas.upenn.edu> wrote:
> On Wed, Jun 19, 2013 at 11:11:16AM +0100, Francesco Mazzoli wrote:
>> At Wed, 19 Jun 2013 10:03:27 +0000 (UTC),
>> AntC wrote:
>> > Hi Francesco, I think you'll find that the 'annoyance' is nothing to do
>> > with GADTs. I suggest you take the type signature off of foo1, and see
>> > what type ghc infers for it. It isn't :: a -> Foo a -> Int.
>> >
>> > [...]
>> >
>> > Yep, that message explains what's going on well enough for me.
>>
(Continue reading)

Brent Yorgey | 19 Jun 20:36 2013

Re: GADTs and pattern matching

Good point.  I stand corrected.

-Brent

On Wed, Jun 19, 2013 at 11:42:23AM -0300, Felipe Almeida Lessa wrote:
> Brent, maybe I'm misunderstanding what you're saying, but I don't
> think that the order of the arguments is playing any role here besides
> defining the order in which the pattern matches are desugared.
> 
> To illustrate,
> 
>   -- This does work
>   foo1' :: a -> Foo a -> Int
>   foo1' m Foo = case m of
>                   Nothing -> undefined
>                   Just _  -> undefined
> 
> Despite having the same type as foo1, foo1' does work because now I've
> pattern matched on the GADT first.  As soon as I do that, its equality
> constraint of (a ~ Maybe v) enters into scope of the case branches.
> 
> Cheers,
> 
> On Wed, Jun 19, 2013 at 7:59 AM, Brent Yorgey <byorgey <at> seas.upenn.edu> wrote:
> > On Wed, Jun 19, 2013 at 11:11:16AM +0100, Francesco Mazzoli wrote:
> >> At Wed, 19 Jun 2013 10:03:27 +0000 (UTC),
> >> AntC wrote:
> >> > Hi Francesco, I think you'll find that the 'annoyance' is nothing to do
> >> > with GADTs. I suggest you take the type signature off of foo1, and see
> >> > what type ghc infers for it. It isn't :: a -> Foo a -> Int.
(Continue reading)


Gmane