Alexey Egorov | 25 Apr 18:29 2013
Picon

pattern matching on data families constructors

Hi,

suppose that there is following data family:

> data family D a
> data instance D Int = DInt Int
> data instance D Bool = DBool Bool

it is not possible to match on constructors from different instances:

> -- type error
> a :: D a -> a
> a (DInt x) = x
> a (DBool x) = x

however, following works:

> data G :: * -> * where
> GInt :: G Int
> GBool :: G Bool
>
> b :: G a -> D a -> a
> b GInt (DInt x) = x
> b GBool (DBool x) = x

The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's constructors, I suppose.

I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints while typechecking pattern matching?

Thanks.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Francesco Mazzoli | 25 Apr 20:08 2013
Picon

Re: pattern matching on data families constructors

At Thu, 25 Apr 2013 20:29:16 +0400,
Alexey Egorov wrote:
> I'm curious - why data families constructors (such as DInt and DBool) doesn't
> imply such constraints while typechecking pattern matching?

I think you are misunderstanding what data families do.  ‘DInt :: DInt -> D Int’
and ‘DBool :: DBool -> D Bool’ are two data constructors for *different* data
types (namely, ‘D Int’ and ‘D Bool’).  The type family ‘D :: * -> *’ relates
types to said distinct data types.

On the other hand the type constructor ‘D :: * -> *’ parametrises a *single*
data type over another type—the fact that the parameter can be constrained
depending on the data constructor doesn’t really matter here.

Would you expect this to work?

> newtype DInt a = DInt a
> newtype DBool a = DBool a
> 
> type family D a
> type instance D Int = DInt Int
> type instance D Bool = DBool Bool
> 
> a :: D a -> a
> a (DInt x) = x
> a (DBool x) = x

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Francesco Mazzoli | 25 Apr 20:13 2013
Picon

Re: pattern matching on data families constructors

At Thu, 25 Apr 2013 19:08:17 +0100,
Francesco Mazzoli wrote:
> ... ‘DInt :: DInt -> D Int’ and ‘DBool :: DBool -> D Bool’ ...

This should read ‘DInt :: Int -> D Int’ and ‘DBool :: Bool -> D Bool’.

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Francesco Mazzoli | 25 Apr 22:08 2013
Picon

Re: pattern matching on data families constructors

At Thu, 25 Apr 2013 19:08:17 +0100,
Francesco Mazzoli wrote:
> Would you expect this to work?
> 
> > newtype DInt a = DInt a
> > newtype DBool a = DBool a
> > 
> > type family D a
> > type instance D Int = DInt Int
> > type instance D Bool = DBool Bool
> > 
> > a :: D a -> a
> > a (DInt x) = x
> > a (DBool x) = x

Or even better:

> data family D a
> data instance D Int = DInt1 Int | DInt2 Int
> data instance D Bool = DBool Bool
> 
> a :: D a -> a
> a (DInt1 x) = x
> a (DInt2 x) = x
> a (DBool x) = x

Francesco
Alexey Egorov | 25 Apr 22:20 2013
Picon

Re: pattern matching on data families constructors

> Would you expect this to work?
> 
> newtype DInt a = DInt a
> newtype DBool a = DBool a
>
> type family D a
> type instance D Int = DInt Int
> type instance D Bool = DBool Bool
> 
> a :: D a -> a
> a (DInt x) = x
> a (DBool x) = x
> 
> Or even better:
> 
> data family D a
> data instance D Int = DInt1 Int | DInt2 Int
> data instance D Bool = DBool Bool
> 
> a :: D a -> a
> a (DInt1 x) = x
> a (DInt2 x) = x
> a (DBool x) = x

Yes, my question is about why different instances are different types even if they have the same type
constructor (D).
I'm just find it confusing that using GADTs trick it is possible to match on different constructors.

Another confusing thing is that following works:

> data G :: * -> * where
> { GInt :: G Int
> ; GBool :: G Bool }
>
> b :: G a -> D a -> a
> b GInt (DInt x) = x
> b GBool (DBool x) = x

while quite similar doesn't:

> c :: D a -> G a -> a
> c (DInt x) GInt = x
> c (DBool x) GBool = x

However, viewing data families as "type families + per-instance newtype/data declaration" is helpful,
thank you.
Francesco Mazzoli | 25 Apr 22:36 2013
Picon

Re: pattern matching on data families constructors

At Fri, 26 Apr 2013 00:20:36 +0400,
Alexey Egorov wrote:
> Yes, my question is about why different instances are different types even if
> they have the same type constructor (D).
> I'm just find it confusing that using GADTs trick it is possible to match on
> different constructors.

See it this way: the two ‘D’s (the GADTs and the data family one) are both type
functions, taking a type and giving you back another type.

In standard Haskell all such type functions return instances of the same data
type (with a set of data constructors you can pattern match on), much like the
‘D’ of the GADTs.  With type/data families the situation changes, and the
returned type can be different depending on the provided type, which is what’s
happening here.

Now the thing you want to do is ultimately write your ‘a’, which as you said
relies on type coercions, but this fact (the ‘GADTs trick’) has nothing to do
with the fact that type families will relate types to different data types.

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Roman Cheplyaka | 25 Apr 23:19 2013

Re: pattern matching on data families constructors

Let's look at it from the operational perspective.

In the GADT case, the set of possibilities is fixed in advance (closed).

Every GADT constructor has a corresponding tag (a small integer) which,
when pattern-matching, tells us which branch to take.

In the data family case, the set of possibilities is open. It is harder
to do robust tagging over all the instances, given that new instances
can be added after the module is compiled.

The right way to do what you want is to use a type class and associate
your data family with that class:

  class C a where
    data D a
    a :: D a -> a

  instance C Int where
    data D Int = DInt Int
    a (DInt x) = x

  instance C Bool where
    data D Bool = DBool Bool
    a (DBool x) = x

Roman

* Alexey Egorov <electreg <at> list.ru> [2013-04-25 20:29:16+0400]
> 
> Hi,
> suppose that there is following data family:
> > data family D a
> > data instance D Int = DInt Int
> > data instance D Bool = DBool Bool
> it is not possible to match on constructors from different instances:
> > -- type error
> > a :: D a -> a
> > a (DInt x) = x
> > a (DBool x) = x
> however, following works:
> > data G :: * -> * where
> > GInt :: G Int
> > GBool :: G Bool
> >
> > b :: G a -> D a -> a
> > b GInt (DInt x) = x
> > b GBool (DBool x) = x
> The reason why second example works is equality constraints (a ~ Int) and (a ~ Bool) introduced by GADT's
constructors, I suppose.
> I'm curious - why data families constructors (such as DInt and DBool) doesn't imply such constraints
while typechecking pattern matching?
> Thanks.

> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ryan Ingram | 19 Nov 00:44 2008
Picon

Pattern matching on numbers?

How does this work?

> fac n = case n of
>    0 -> 1
>    _ -> n * fac (n-1)

ghci> :t fac
fac :: (Num t) => t -> t

The first line of "fac" pattern matches on 0.  So how does this work
over any value of the Num typeclass?  I know that the "1" on the rhs
of fac are replaced with (fromInteger 1), but what about numeric
literals in patterns?  Does it turn into a call to (==)?

Should whatever technique is used be extended to other typeclasses too?

  -- ryan
Henning Thielemann | 19 Nov 00:56 2008
Picon

Re: Pattern matching on numbers?


On Tue, 18 Nov 2008, Ryan Ingram wrote:

> How does this work?
>
>> fac n = case n of
>>    0 -> 1
>>    _ -> n * fac (n-1)
>
> ghci> :t fac
> fac :: (Num t) => t -> t
>
> The first line of "fac" pattern matches on 0.  So how does this work
> over any value of the Num typeclass?  I know that the "1" on the rhs
> of fac are replaced with (fromInteger 1), but what about numeric
> literals in patterns?  Does it turn into a call to (==)?

As far as I know, yes. It is even possible to trap into an error on 
pattern matching this way if fromInteger generates an 'undefined'.

> Should whatever technique is used be extended to other typeclasses too?

  It is unusual to do pattern matching on fractions, you mostly need it for 
recursion on natural numbers. Thus I think the cleanest solution would be 
to treat natural numbers like strict Peano numbers
   data PeanoStrict = Zero | Succ !PeanoStrict
  but with an efficient implementation using GMP integers, maybe using 
'views', if they were part of Haskell language. Then you can implement:

fac :: Integer -> Integer
fac Zero = 1
fac n1 <at> (Succ n) = n1 * fac n

  I would then give up pattern matching on any numeric type.
David Menendez | 19 Nov 01:00 2008

Re: Pattern matching on numbers?

On Tue, Nov 18, 2008 at 6:56 PM, Henning Thielemann
<lemming <at> henning-thielemann.de> wrote:
>
> On Tue, 18 Nov 2008, Ryan Ingram wrote:
>
>> How does this work?
>>
>>> fac n = case n of
>>>   0 -> 1
>>>   _ -> n * fac (n-1)
>>
>> ghci> :t fac
>> fac :: (Num t) => t -> t
>>
>> The first line of "fac" pattern matches on 0.  So how does this work
>> over any value of the Num typeclass?  I know that the "1" on the rhs
>> of fac are replaced with (fromInteger 1), but what about numeric
>> literals in patterns?  Does it turn into a call to (==)?
>
> As far as I know, yes. It is even possible to trap into an error on pattern
> matching this way if fromInteger generates an 'undefined'.

As I understand it, the use of (==) in numeric pattern matching is why
Num requires Eq.

--

-- 
Dave Menendez <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>
Tobias Bexelius | 19 Nov 12:01 2008
Picon

RE: Pattern matching on numbers?

Yes, fromInteger and == is used for pattern matching on numbers.
However, on GHC you can use -XNoImplicitPrelude to make it use whatever
fromInteger and == that's in scope (without any Num or Eq).

Eg. if == is a method of MyEq class and fromInteger is a method of
MyNum, and MyNum doesn't inherit MyEq, then the type of this function

f 0 = ""
f x = 'e' : f (x-1)

Will be inferred as (MyEq a, MyNum a) => a -> String

/Tobias

-----Original Message-----
From: haskell-cafe-bounces <at> haskell.org
[mailto:haskell-cafe-bounces <at> haskell.org] On Behalf Of David Menendez
Sent: den 19 november 2008 01:00
To: Henning Thielemann
Cc: Haskell Cafe
Subject: Re: [Haskell-cafe] Pattern matching on numbers?

On Tue, Nov 18, 2008 at 6:56 PM, Henning Thielemann
<lemming <at> henning-thielemann.de> wrote:
>
> On Tue, 18 Nov 2008, Ryan Ingram wrote:
>
>> How does this work?
>>
>>> fac n = case n of
>>>   0 -> 1
>>>   _ -> n * fac (n-1)
>>
>> ghci> :t fac
>> fac :: (Num t) => t -> t
>>
>> The first line of "fac" pattern matches on 0.  So how does this work 
>> over any value of the Num typeclass?  I know that the "1" on the rhs 
>> of fac are replaced with (fromInteger 1), but what about numeric 
>> literals in patterns?  Does it turn into a call to (==)?
>
> As far as I know, yes. It is even possible to trap into an error on 
> pattern matching this way if fromInteger generates an 'undefined'.

As I understand it, the use of (==) in numeric pattern matching is why
Num requires Eq.

--
Dave Menendez <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tom Brow | 23 Apr 08:52 2011
Picon

Pattern matching on lazy bytestrings: how does it work?

I noticed today that I can pattern match against lazy bytestrings when using the OverloadedStrings extension:


import Data.ByteString.Char8 ()
import Data.ByteString.Lazy.Char8

f :: ByteString -> Bool
f "abc" = True
f _ = False

main = do
print $ f $ fromChunks ["abc"]
print $ f $ fromChunks ["a","bc"]

When I run the above, I get:

True
True

Given that pattern matching is based on data constructors, how is it possible that (Chunk "abc Empty) and (Chunk "a" (Chunk "bc" Empty)) match the same pattern?

Tom

 


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Stephen Tetley | 23 Apr 09:17 2011
Picon

Re: Pattern matching on lazy bytestrings: how does it work?

Surely `fromChunks` is making the both lines in the code snippet the same?

Also, in your last sentence I think you've miscalculated the shape of
the initial input.

Best wishes

Stephen
Picon

Re: Pattern matching on lazy bytestrings: how does it work?

On Fri, Apr 22, 2011 at 11:52:32PM -0700, Tom Brow wrote:
> I noticed today that I can pattern match against lazy bytestrings when using
> the OverloadedStrings extension:
[..]
> Given that pattern matching is based on data constructors, how is it possible
> that (Chunk "abc Empty) and (Chunk "a" (Chunk "bc" Empty)) match the same
> pattern?
> 
> Tom
> 

According to the haskell report[1] string literals use the overloaded (==)
for pattern matching.

    Matching a numeric, character, or string literal pattern k against a
    value v succeeds if v == k, where == is overloaded based on the type of
    the pattern. The match diverges if this test diverges.

    [1]: http://www.haskell.org/onlinereport/exps.html#sect3.17.2

--

-- 
Helgi Kristvin Sigurbjarnarson <helgikrs (at) gmail (dot) com>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane