Distributing intersection and union types with splits and duality (functional pearl)

Subtyping with intersection and union types is nowadays common in many programming languages. From the perspective of logic, the subtyping problem is essentially the problem of determining logical entailment : does a logical statement follow from another one? Unfortunately, algorithms for deciding subtyping and logical entailment with intersections, unions and various distributivity laws can be highly non-trivial. This functional pearl presents a novel algorithmic formulation for subtyping (and logical entailment) in the presence of various distributivity rules between intersections, unions and implications (i.e. function types). Unlike many existing algorithms which first normalize types and then apply a subtyping algorithm on the normalized types, our new subtyping algorithm works directly on source types. Our algorithm is based on two recent ideas: a generalization of subtyping based on the duality of language constructs called duotyping ; and splittable types , which characterize types that decompose into two simpler types. We show that our algorithm is sound, complete and decidable with respect to a declarative formulation of subtyping based on the minimal relevant logic B + . Moreover, it leads to a simple and compact implementation in under 50 lines of functional code.

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library’s test suite, and interfaces from Coq’s standard library. Our work shows that it is feasible to verify mature, widely used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested functional code.

Research and Application of Rule Engine in Scheduled Outage Management

With the rapid development of economy, the requirement for electricity supply is growing dramatically, and the consumers are claiming for higher power supply quality with less outage. Scheduled outage makes a major part of power outage, and it is mainly caused by power grid construction and power equipment maintenance. Scheduled outage has a lot of concerns, such as grid structure, potential outage loss, critical consumers or important occasions, and such factors are changing rapidly with the quick development of distribution network. As a result, the validation and optimization of scheduled outage becomes complicated. Rule engine [1] can describe business rules by pre-defined language, separate such rules from functional code [2], and execute them when trigger condition is satisfied. The application of rule engine can increase system adaptability to business variation, and decrease the system coupling and maintenance cost. With the application of rule engine in scheduled outage management, outage plan can be effectively validated and flexibly optimized, and the outage loss and consumer complaints could be significantly decreased.