Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Active or View patterns #12

Closed
wants to merge 1 commit into from
Closed

Active or View patterns #12

wants to merge 1 commit into from

Conversation

bash-spbu
Copy link

@bash-spbu bash-spbu commented Feb 10, 2020

This RFC aims to extend the support of patterns in the language and make it

  • first class values;
  • go well with abstraction and encapsulation;
  • be able to be parameterized.

We spent quite a lot of time of overviewing in which ways pattern matching can be theoretically extented and which features are already supported in different languages. Its results are presented in the separate repo to keep this RFC more concise. The goals of that document is to support this discussion with objective criterions and examples.

Why this particular extension

There are actually dozens of possible ideas/designs/approaches of pattern matching extension. We reviewed quite a lot of them (results are presented by the link above) and found out that active (or view) patterns are

  • the most powerful in the ratio of flexibility & opportunities TO implementation complexity & language influence;
  • are able to solve (almost) all of the known issues about OCaml pattern matching.

What is next

We want to discuss and come up to the particular syntax of the extension. Semantically active and view patterns are absolutely the same. Personally we prefer active patterns over view patterns because they are more concise, require less modifications of the language grammar, and are pretty easy to extend to suport the infix notattion of constuctors (to make :: not being the special syntax anymore). Please, write your thoughts and ideas about this.

@Octachron
Copy link
Member

After reading your proposal, I have no clear idea on how active patterns could be implemented while preserving both the efficiency of pattern matching and the exhaustiveness check in the context of the current pattern matching compiler. Overall, the drawback analysis seems a bit lacking and your current proposal would be more at home as a feature request on ocaml/ocaml.

@bash-spbu
Copy link
Author

You are absolutely right, it is not the complete proposal for now. Actually I deliberately omitted technical details like syntax, semantics and pattern matching compilation scheme patch, because even the kind of extension has not been selected by now: we are still on the design selection phase. Dozens of different extensions have been already suggested for different languages (in particular on the discourse for OCaml) and I prepared a big overview which tries to systemize all of them to select the best objectively. According to it active patterns were example of the such good design, though I understood that it was a little bit opinionated from my side and that is why I requested for comments of the community.

We have discussed it with several people and I have got the desired fact that some people find active patterns attractive, and now the main problem is that it is indeed unclear how to introduce them to the existing ecosystem without loss of the efficiency, exhaustiveness check and other desired properties, what actually is a significant reason of not implementing it. I missed that fact.

So in the nearest time I will prepare the in-detailed version of the proposal with accent on the implementation features like the compilation scheme and exhaustiveness checking to be able to discuss it more substantively.

@Octachron
Copy link
Member

Since we agree that the full proposal is not ready, I am closing it for now. Feel free to reopen it when you have a full proposal.

However, I should mention that the existence of a decidable exhaustiveness check for pattern matching is an important property of today's OCaml; and it is really not clear how to preserve this property after the introduction of view patterns.

@Octachron Octachron closed this Feb 12, 2020
@lpw25
Copy link
Contributor

lpw25 commented Feb 12, 2020

it is really not clear how to preserve this property after the introduction of view patterns.

I don't disagree with closing this RFC for now as it is under prepared, but I think it is worth pointing out that it is fairly obvious how to make active patterns support exhausitivity -- indeed F# provides both exhaustive and non-exhausitve active patterns.

@cemerick
Copy link

cemerick commented Mar 19, 2020

Leaving aside this specific proposal, it might be good to have some clarity w.r.t. the language being open to future work on view patterns or similar capabilities. The last two comments here reveal perhaps some disagreement as to whether they are categorically desirable or not given other settled design decisions.

As for the challenges of exhaustiveness checking raised by @Octachron, I wanted to just point out that of course guard expressions are opaque to those checks, at least for those patterns that have guards; wouldn't a view patterns implementation (at least, one similar to e.g. Haskell's where there is no way [IIRC] to check exhaustiveness) fall into the same category? (I am much less familiar with F#'s Active Patterns feature, but will shortly be looking into what it provides re: optional exhaustiveness checks.)

@maranget
Copy link

maranget commented Mar 19, 2020 via email

@bash-spbu
Copy link
Author

I will try to add some notes too.

The Motivation

Active (and view) patterns are pretty neat and can solve some tasks clearer and shorter. Personally, my main motivation in extension of such kind is to maximally generalize the definition of pattern itself. It will simultaneously simplify the language (leaving private type definitions, lazy patterns, and-patterns unneeded) and generalize existing constructions: for example, if we then implement symbolic infix-notation for the patterns, we will be able to express the same notation as Haskell's Pattern Synonyms and Scala's infix class names. And at the same time the notation x :: xs won't be a specific language construct for built-in lists anymore, and will be able to be defined by the user.

Is it free?

If we won't be able to save the same levels of performance and exhaustiveness checking, most probably the extension will not worth the implementation. So I spent some time on investigating this carefully. The short answer is yes, we can, and thanks to @maranget fundamental works, even without much effort.

Performance

Unfortunately, most probably, it won't be expedient (though possible) to extend the currently used compilation scheme, because it operates mainly on permutations of rows, and as with guards the question whether it is correct to swap two branches containing active patterns is undecidable. More specifically, the relation of pattern compatibility (see this work) can not be computed in presence of active patterns. Though the compilation of matches without active patterns usage will remain the same, the compilation of matches with them will be probably far from optimal.

But the situation is much better with schemes based on decision trees which use permutation of columns. If we claim that the order of evaluation of patterns in a row is not determined, we will be able to freely rearrange columns, and thereby to use all heuristics described here. Seems like even the definition of necessity can be safely extended on active patterns, but I have not proven it yet. Compilation to decision trees guided by heuristics can sometimes produce even more good results than the current one. So if we change the compilation scheme to the one described here, we will probably save the performance on the same high level even in presence of active patterns.

There is also an interesting idea about inlining. Sometimes we can safely inline the definition of active pattern to the its usage place, fully neutralizing the overhead of its usage. And sometimes even between modules (for instance, if they are in the same compilation unit, or if the definition of the active pattern target type is exported as well). But now the OCaml compiler performs the inlining after the compilation of pattern matching, so this idea demands some technical workarounds.

Exhaustiveness checking

The situation with it is quite simple, actually. Yes, the question of exhaustiveness is undecidable in presence of active patterns (as with guards), but we can give quite accurate and simple approximation on it: active pattern just declare the set of alternatives (which form its name), all of which must be mentioned in the occurrence test in the match.

For instance, multi-case active patterns are checked on exhaustiveness exactly like data constructors. Taking an example from the original work:

// F# code
type Type with
  member IsGenericType : bool
  member GetGenericTypeDefinition : unit -> Type
  member GetGenericArguments : unit -> Type[]
  member HasElementType : bool
  member GetElementType : unit -> Type
  member IsByRef : bool // an managed pointer
  member IsPointer : bool // an unmanaged pointer
  member IsGenericParameter : bool
  member GenericParameterPosition : int

let (|Named|Array|Ptr|Param|) (typ : System.Type) =
  if typ.IsGenericType
  then Named(typ.GetGenericTypeDefinition(), typ.GetGenericArguments())
  elif typ.IsGenericParameter
  then Param(typ.GenericParameterPosition)
  elif not typ.HasElementType
  then Named(typ, [| |])
  elif typ.IsArray
  then Array(typ.GetElementType(), typ.GetArrayRank())
  elif typ.IsByRef
  then Ptr(true,typ.GetElementType())
  elif typ.IsPointer
  then Ptr(false,typ.GetElementType())
  else failwith "MSDN says this can’t happen"

// pretty printing
let rec formatType typ =
  match typ with
  | Named (con, [])   -> sprintf "%s" con.Name
  | Named (con, args) -> sprintf "%s<%s>" con.Name (formatTypes args)
  | Array (arg, rank) -> sprintf "Array(%d,%s)" rank (formatType arg)
  | Ptr(true,arg)     -> sprintf "%s&" (formatType arg)
  | Ptr(false,arg)    -> sprintf "%s*" (formatType arg)
  | Param(pos)        -> sprintf "!%d" pos

and formatTypes typs =
  String.Join(",",Array.map formatType typs)

// collecting free generic type variables
let rec freeVarsAcc typ acc =
  match typ with
  | Array (arg, rank) -> freeVarsAcc arg acc
  | Ptr (_,arg)       -> freeVarsAcc arg acc
  | Param _           -> (typ :: acc)
  | Named (con, args) -> Array.fold_right freeVarsAcc args acc

let freeVars typ = freeVarsAcc typ []

Here matching with Type value acts just like if Type was declared using the following sum type definition:

type Type =
  | Named of Type * Type array
  | Array of int * Type
  | Ptr of bool * Type
  | Param of int

Matches in formatTypes and freeVarsAcc are checked to be exhaustive. If one of the alternatives was missed, the compiler would complain about it and would show values of which category (-ies) have not been checked by the match.

One-case active patterns are irrefutable.

Partial active patterns do not add any troubles: they just say that one of the alternatives must be a wildcard _ (because not all values are guaranteed to be matched by this active pattern), and this fact is again mentioned in the name of the pattern:

// F# code
let (|ParseRegex|_|) re s =
  let m = Regex(re).Match(s)
  if m.Success
  then Some [ for x in m.Groups -> x.Value ]
  else None

let swap s =
  match s with
  | ParseRegex "(\w+)-(\w+)" [l;r] -> r ^ "-" ^ l
  | _ -> s

Here in swap definition the _ alternative must be mentioned explicitly. If total pattern (-s) were used on this occurrence in next branches, the _ would not be needed.

With respect to exhaustiveness all guards act just like partial active patterns: to be used safely they need default case when true, just like active pattern a wildcard _ (though current implementation of the OCaml compiler do not take in consideration the content of guard and in such variant the compiler will issue a warning):

let swap s =
  match s with
  | s when matchRegex "(\w+)-(\w+)" -> .
  | s when true -> .
  | ...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants