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 On Fri, Oct 26, 2018 at 1:05 PM Richard Eisenberg <r...@cs.brynmawr.edu> wrote: > 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. > > Here's a stab at a formalization of this idea, written in metatheory, not > Haskell: > > 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 > > On Oct 26, 2018, at 5:20 AM, Sylvain Henry <sylv...@haskus.fr> wrote: > > Sorry I wasn't clear. I'm not an expert on the topic but it seems to me > that there are two orthogonal concerns: > > 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", > "a") we could write: > > {-# COMPLETE LL #-} > > From an implementation point of view, it seems to me that finding complete > sets would become similar to finding (flexible, overlapping) class > instances. Pseudo-code: > > class Complete a where > conlikes :: [ConLike] > instance Complete (Maybe a) where > conlikes = [Nothing @a, Just @a] > instance Complete (Maybe a) where > conlikes = [N @a, J @a] > instance Complete a where > conlikes = [LL @a] > ... > > > 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 > type. Pseudo-code: > > instance Complete (Variant cs) where > conlikes = [V @c | c <- cs] -- cs is a type list > > (I don't really care about the pragma syntax) > > Sorry for the thread hijack! > Regards, > Sylvain > > > On 10/26/18 5:59 AM, Richard Eisenberg wrote: > > 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 > > On Oct 25, 2018, at 12:24 PM, Sylvain Henry <sylv...@haskus.fr> wrote: > > > 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. > > Currently we can specify the type *constructor* in a COMPLETE pragma: > > 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 > them in conlike signatures: > > {-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-} > > The COMPLETE pragma for LL could be: > > {-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-} > > > I'm borrowing the list comprehension syntax on purpose because it would > allow to define a set of conlikes from a type-list (see my request [1]): > > {-# COMPLETE [ V :: (c :< cs) => c -> Variant cs > | c <- cs > ] :: Variant cs > #-} > > > 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 > > sets. > > 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 > 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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs