Re: Pattern matching and GADTs

9 Mar 2015

      On 3/3/15, Simon Peyton Jones  wrote:
...
|  data Bar a where
|    Listy :: Bar [Int]
|
|  {-
|  foo :: a -> Bar a -> Int
|  foo [0] Listy = 1
Well you'd get a seg-fault from the call (foo True (undefined :: Bar
[Int])).  So we really MUST match the (Bar a) arg before the 'a' arg.  And
Oh, okay, I see! But you surely mean
  (foo True (undefined :: Bar Bool))
...
Haskell only offers one way to do that, which is to put it first.
You don't have to change the argument order.  Write
foo xs Listy | [0] <- xs = 1
Yeah, this is what I gave as foo'' in my examples. What about making
an irrefutable pattern match?

{{{
foo :: a -> Bar a -> Int
foo ~[a] Listy = a
}}}

While I guess this won't SEGV, it may error with a pattern match
failure. Besides, the type-checker won't let us:

    Couldn't match expected type `a' with actual type `[a0]'
      `a' is a rigid type variable bound by
          the type signature for: foo :: a -> Bar a -> Int

So the pattern guard solution looks like our best option to fix the
ordering issue.

Thanks,

    Gabor
...
Simon
|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Gabor
|  Greif
|  Sent: 03 March 2015 14:13
|  To: ghc-devs@haskell.org
|  Subject: Re: Pattern matching and GADTs
|
|  This might be off-topic for your paper, but possibly relevant for GADT-
|  based programming:
|
|  In the below snippet
|  -----------------------------------------------------------------
|  {-# LANGUAGE GADTs, PatternGuards #-}
|
|  data Bar a where
|    Listy :: Bar [Int]
|
|  {-
|  foo :: a -> Bar a -> Int
|  foo [0] Listy = 1
|
|  gadtTest.hs:8:5:
|      Couldn't match expected type `a' with actual type `[a0]'
|        `a' is a rigid type variable bound by
|            the type signature for: foo :: a -> Bar a -> Int
|            at /home/ggreif/gadtTest.hs:7:8
|      Relevant bindings include
|        foo :: a -> Bar a -> Int (bound at /home/ggreif/gadtTest.hs:8:1)
|      In the pattern: [0]
|      In an equation for `foo': foo [0] Listy = 1 -}
|
|  foo' :: Bar a -> a -> Int
|  foo' Listy [a] = a
|
|  foo'' :: a -> Bar a -> Int
|  foo'' l Listy | [a] <- l = a
|  -----------------------------------------------------------------
|
|  the "wrong" order of pattern matches (i.e. foo) causes an error, the
|  flipped order works (i.e. foo') and pattern guards remedy the situation
|  (e.g. foo'').
|
|  Since the type signatures are isomorphic this is a bit disturbing. Why
|  is it like this?
|  My guess is that patterns are matched left-to-right and refinements
|  become available "too late". Or is the reason buried in the OutsideIn
|  algorithm (and function arrow associativity: a -> (Bar a -> Int)) ?
|
|  Would it be a big deal to forward-propagate type information in from
|  GADT pattern matches?
|
|  Thanks and cheers,
|
|      Gabor
|
|  On 3/2/15, Simon Peyton Jones  wrote:
|  > GHC developers
|  > You may be interested in this paper, submitted to ICFP GADTs meet
|  > their match: pattern-matching warnings that account for GADTs,
|  guards,
|  > and
|  > laziness<http://research.microsoft.com/%7Esimonpj/papers/pattern-
|  match
|  > ing>, with Georgios Karachalias, Tom Schrijvers, and Dimitrios
|  > Vytiniotis.
|  > It describes a GADT-aware algorithm for detecting missing and
|  > redundant patterns.
|  > The implementation is not yet up to production quality, but it will
|  be!
|  > If you feel able to give us any feedback about the paper itself, that
|  > would be incredibly useful. Thanks Simon
|  >
|  >
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs@haskell.org
|  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Pattern matching and GADTs

Gabor Greif