[Haskell-cafe] 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
Now, GHC can clearly derive and use the type equalities correctly, given
that the second definition works, but why can’t I pattern match
directly?
Thanks,
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs and pattern matching
At Wed, 19 Jun 2013 10:03:27 + (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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 + (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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 http://www.haskell.org/pipermail/glasgow-haskell-users/2013-June/023994.html. However, I’d argue that the issue doesn’t have much to do with the fact that Haskell has only ‘1 argument functions’, at least at the type level. It’s more about how Haskell treats pattern matching. In Agda/Epigram/Idris pattern matching works the other way around: they allow it only in top-level definitions, and every other kind of match get desugared to a new top level definition. Thus you can reason about the constraints on all the arguments in a better way. Lately I’ve grown used to that kind of pattern matching :). In Haskell however where you expect _|_ and diverging matches, so it probably makes more sense to have matching like is is now, otherwise you’d have to force arguments to get equalities concerning earlier arguments and things would probably get really messy. Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 byor...@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 + (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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 byor...@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 + (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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
