Pattern matching and GADTs

older
Re: How to better parallelize GHC...

Simon Peyton Jones

2 Mar 2015 2 Mar '15

11:16 a.m.

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 lazinesshttp://research.microsoft.com/%7Esimonpj/papers/pattern-matching, 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

Attachments:

attachment.html (text/html — 3.2 KB)

Show replies by date

Gabor Greif

3 Mar 3 Mar

9:13 a.m.

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 lazinesshttp://research.microsoft.com/%7Esimonpj/papers/pattern-matching, 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

Simon Peyton Jones

9:23 a.m.

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

Gabor Greif

9 Mar 9 Mar

7:09 a.m.

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

Simon Peyton Jones

9:24 a.m.

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

3725

Age (days ago)

3732

Last active (days ago)

List overview

Download

4 comments

2 participants

participants (2)

Gabor Greif
Simon Peyton Jones