[Haskell-cafe] GADTs and pattern matching

[Brent Yorgey]

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.
> >> >
> >> > [...]
> >> >
> >> > 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
> >
> >   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.
> >
> > -Brent
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 
> 
> -- 
> Felipe.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>