Pattern matching and GADTs

[Simon Peyton Jones]

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

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