[Haskell-cafe] GADTs and pattern matching
f at mazzo.li
Wed Jun 19 13:08:56 CEST 2013
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.
Thanks for your answer.
I was reminded by shachaf on Haskell a few moments ago about the details
of pattern matching in GHC
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.
More information about the Haskell-Cafe