off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the

abstracted constructors matters!

consider

foo,bar,baz,quux,boom :: Nat -> String

plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd"

foo (PowerOfTwo x) = "power of two"

foo (Even x) = "even"

foo (Odd x) = "odd"

bar (Even x) = "even"

bar (Odd x) = "odd"

baz (PowerOfTwo x) = "power of two"

baz (Odd x) = "odd"

quux (Even x) = "even"

quux (Odd x) = "odd"

quux (PowerOfTwo) = "power of two"

boom (Even x) = "even"

boom (PowerOfTwo x) = "power of two"

boom (Odd x) = "odd"

foo and bar are both total definitions with unambiguous meanings, even

though bar's patterns are a suffix of foos'!

baz is partial!

both boom and quux have a redudant overlapping case, power of two!

so some thoughts

1) order matters!

2) pattern synonyms at type T are part of an infinite lattice, Top element

== accept everything, Bottom element = reject everything

3) PowerOfTwo <= Even in the Lattice for Natual, both are "incomparable"

with Odd

4) for a simple case on a single value at type T, assume c1 <= c2

, then if c1 x -> ... is before c2 x -> in the

cases, then both are useful/computationally meaningful

OTHERWISE

when its

case x :: T of

c2 x -> ...

c1 x -> ...

then the 'c1 x' is redundant

this is slightly orthogonal to other facets of this discussion so far, but

i realized that Richard's Set of Sets of patterns model misses some useful/

meaningful examples/extra structure from

a) the implicit lattice of different patterns possibly being super/subsets

(which is still something of an approximation, but with these example I

shared above I hope i've sketched out some motivation )

b) we can possibly model HOW ordering of clauses impacts coverage/totality

/ redundancy of clauses

I'm not sure if it'd be pleasant/good from a user experience perspective to

have this sort of partial ordering modelling stuff, but certainly seems

like it would help distinguish some useful examples where the program

meaning / coverage is sensitive to clause ordering

i can try to spell this out more if theres interest, but I wanted to share

while the iron was hot

best!

-Carter

*Post by Richard Eisenberg*Aha. So you're viewing complete sets as a type-directed property, where we

can take a type and look up what complete sets of patterns of that type

might be.

Then, when checking a pattern-match for completeness, we use the inferred

type of the pattern, access its complete sets, and if these match up.

(Perhaps an implementation may optimize this process.)

What I like about this approach is that it works well with GADTs, where,

e.g., VNil is a complete set for type Vec a Zero but not for Vec a n.

I take back my claim of "No types!" then, as this does sound like it has

the right properties.

For now, I don't want to get bogged down by syntax -- let's figure out how

the idea should work first, and then we can worry about syntax.

Let C : Type -> Set of set of patterns. C will be the lookup function for

complete sets. Suppose we have a pattern match, at type tau, matching

against patterns Ps. Let S = C(tau). S is then a set of sets of patterns.

The question is this: Is there a set s in S such that Ps is a superset of

s? If yes, then the match is complete.

What do we think of this design? Of course, the challenge is in building

C, but we'll tackle that next.

Richard

Sorry I wasn't clear. I'm not an expert on the topic but it seems to me

1) How does the checker retrieve COMPLETE sets.

Currently it seems to "attach" them to data type constructors (e.g.

Maybe). If instead it retrieved them by matching types (e.g. "Maybe a",

{-# COMPLETE LL #-}

From an implementation point of view, it seems to me that finding complete

sets would become similar to finding (flexible, overlapping) class

class Complete a where

conlikes :: [ConLike]

instance Complete (Maybe a) where

instance Complete (Maybe a) where

instance Complete a where

...

2) COMPLETE set depending on the matched type.

It is a thread hijack from me but while we are thinking about refactoring

COMPLETE pragmas to support polymorphism, maybe we could support this too.

The idea is to build a different set of conlikes depending on the matched

instance Complete (Variant cs) where

(I don't really care about the pragma syntax)

Sorry for the thread hijack!

Regards,

Sylvain

I'm afraid I don't understand what your new syntax means. And, while I

know it doesn't work today, what's wrong (in theory) with

{-# COMPLETE LL #-}

No types! (That's a rare thing for me to extol...)

I feel I must be missing something here.

Thanks,

Richard

*Post by Ryan Scott*In the case where all the patterns are polymorphic, a user must

provide a type signature but we accept the definition regardless of

the type signature they provide.

pattern J :: a -> Maybe apattern J a = Just apattern N :: Maybe apattern N = Nothing{-# COMPLETE N, J :: Maybe #-}

Instead if we could specify the type with its free vars, we could refer to

{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}

{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}

I'm borrowing the list comprehension syntax on purpose because it would

{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs

| c <- cs

] :: Variant cs

#-}

*Post by Ryan Scott*To make things more formal, when the pattern-match checker > requests a

set of constructors for some data type constructor T, the > checker

returns: > > * The original set of data constructors for T > * Any COMPLETE

sets of type T > > Note the use of the phrase **type constructor**. The

return type of all > constructor-like things in a COMPLETE set must all be

headed by the > same type constructor T. Since `LL`'s return type is simply

a type > variable `a`, this simply doesn't work with the design of COMPLETE

Could we use a mechanism similar to instance resolution (with

FlexibleInstances) for the checker to return matching COMPLETE sets instead?

--Sylvain

[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html

_______________________________________________

ghc-devs mailing list

http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________

ghc-devs mailing list

http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs