Pattern matching and GADTs

[Gabor Greif]

On 3/3/15, Simon Peyton Jones <simonpj at microsoft.com> 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 at haskell.org] On Behalf Of Gabor
> |  Greif
> |  Sent: 03 March 2015 14:13
> |  To: ghc-devs at 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 <simonpj at microsoft.com> 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 at haskell.org
> |  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>