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