Pattern matching and GADTs

[Simon Peyton Jones]

|  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
|  }}}

Yes that's attractive, but you have do to strictness analysis to find out when the pattern is forced.  E.g.

	foo ~[x] (True <- f x) Listy = x

Is this ok?  Well, if f is strict in 'x' it's not ok. But if 'f' is lazy, the it'd be fine.  I don't want type correctness to depend on strictness analysis.

Simon


|  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
|  >