Reasoning about GADT Pattern Matching in Haskell

Channel:
Microsoft Research
Subscribers:
342,000
Published on ● Video Link: https://www.youtube.com/watch?v=xCwtN9wUjtA


Duration: 36:24
3,619 views
12

Generalized Algebraic Data Types (GADTs) are a simple but powerful generalization of Algebraic Data Types (ADTs) in Haskell and the ML family. Reasoning about the accessibility of case branches and the exhaustiveness of pattern matching is a well studied and efficiently solved problem for ADTs. However, classic algorithms fall short in the presence of GADTs, issuing false warnings: Since GADT constructors introduce local constraints, we must allow for the fact that particular combinations of patterns and/or values cannot actually occur. We present a novel algorithm for checking pattern matching that accounts for Haskell's laziness and relies on implication constraints generated and solved by the OutsideIn(X) type inference engine. Since we rely on the existing type inference engine, our approach is efficient and robust to future extensions of the type system. We also report on a proof-of-concept implementation of our algorithm in GHC.



Other Videos By Microsoft Research


2016-06-21Provable Submodular Minimization via Wolfe’s Algorithm
2016-06-21A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization
2016-06-21Stochastic Methods for Complex Performance Measures: A Tale of Two Families
2016-06-21Parallel Bayesian Network Structure Learning for Genome-Scale Gene Networks
2016-06-21Empirical Inference for Intelligent Systems
2016-06-21Ordered Stick-breaking Prior for Sequential MCMC Inference of Bayesian Non-Parametric Models
2016-06-21Effective-Resistance-Reducing Flows, Spectrally Thin Trees and Asymmetric TSP
2016-06-21Non-Convex Robust PCA
2016-06-21Communication-Avoiding Algorithms and Fast Matrix Multiplication
2016-06-21The Forza Motorsport 5 Original Soundtrack, An Insider's View
2016-06-21Reasoning about GADT Pattern Matching in Haskell
2016-06-21Non-Convex Robust PCA - Part 2
2016-06-21Modeling, Quantifying, and Limiting Adversary Knowledge
2016-06-21Sampling Techniques for Constraint Satisfaction and Beyond
2016-06-21Cell Classification of FT-IR Spectroscopic Data for Histopathology using Neural Networks
2016-06-21Sequential Equilibrium Distributions in Multi-Stage Games with Infinite Sets of Types and Actions
2016-06-21Randomized Interior Point Methods for Sampling and Optimization
2016-06-21Introduction to large-scale optimization - Part1
2016-06-21Welcome and Microsoft Research Asia Update
2016-06-21An average-case depth hierarchy theorem for Boolean circuits
2016-06-21Enabling Connected Cars through Named Data.


Tags:
microsoft research
algorithms