On 3/3/15, Simon Peyton Jones <simo...@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-boun...@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 <simo...@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@haskell.org
> | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
