text: Non-free data types are data types whose data have no canonical forms. For example, multisets are non-free data types because the multiset @math has two other equivalent but literally different forms @math and @math . Pattern matching is known to provide a handy tool set to treat such data types. Although many studies on pattern matching and implementations for practical programming languages have been proposed so far, we observe that none of these studies satisfy all the criteria of practical pattern matching, which are as follows: i) efficiency of the backtracking algorithm for non-linear patterns, ii) extensibility of matching process, and iii) polymorphism in patterns. This paper aims to design a new pattern-matching-oriented programming language that satisfies all the above three criteria. The proposed language features clean Scheme-like syntax and efficient and extensible pattern matching semantics. This programming language is especially useful for the processing of complex non-free data types that not only include multisets and sets but also graphs and symbolic mathematical expressions. We discuss the importance of our criteria of practical pattern matching and how our language design naturally arises from the criteria. The proposed language has been already implemented and open-sourced as the Egison programming language.
  @cite_14: Pattern matching and data abstraction are important concepts in designing programs, but they do not fit well together. Pattern matching depends on making public a free data type representation, while data abstraction depends on hiding the representation. This paper proposes the views mechanism as a means of reconciling this conflict. A view allows any type to be viewed as a free data type, thus combining the clarity of pattern matching with the efficiency of data abstraction.
  @cite_22: Abstract Laws in the Miranda programming language provide a means of implementing non-free algebraic types, by means of term rewriting. In this paper we investigate program verification in such a context. Specifically, we look at how to deduce properties of functions over these “lawful” types. After examining the general problem, we look at a particular class of functions, the faithful functions. For such functions we are able, in a direct manner, to transfer properties of functions from free types to non-free types. We introduce sufficient model theory to explain these transfer results, and then find characterisations of various classes of faithful functions. Then we investigate an application of this technique to general, unfaithful, situations. In conclusion we survey Wadler's work on views and assess the utility of laws and views.
  @cite_23: In Standard ML, as in many other languages, programmers are often confronted with an unpleasant choice between pattern matching and abstraction. Because pattern matching can only be performed on concrete datatypes, programmers must often sacrifice either the convenience of pattern matching or the engineering benefits of abstraction. Views relieve this tension by allowing pattern matching on abstract datatypes. We propose a modest extension of Standard ML with views and define its semantics via a source-to-source translation back into Standard ML without views. We claim no particular technical innovation; rather, we have attempted to engineer a solution that blends as seamlessly as possible with the rest of the language, including the module system and the stateful features of the language.
  @cite_5: 
  @cite_10: A chrysanthemum plant named Marmalade characterized by the combined characteristics of incurved capitulum form; standard capitulum type; light bronze ray floret color; diameter across face of capitulum ranging from 130 to 150 mm. at maturity; uniform nine (9) week photoperiodic flowering response to short days; 55 to 70 cm. plant height when grown single stem with no long days and a low temperature tolerance of 13 DEG C. (55 DEG F.) for initiation and development under controlled short days with a continuous dark period of 12 to 14 hours.
summary: Miranda laws @cite_10 @cite_5 @cite_22 and Wadler's views @cite_14 @cite_23 are seminal work. These proposals provide methods to decompose data with multiple representations by explicitly declaring transformations between each representation. These are the earliest studies that allow users to customize the execution process of pattern matching. However, the pattern-matching systems in these proposals treat neither multiple pattern matching results nor non-linear patterns. Also, these studies demand a canonical form for each representation.