BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Reasoning about GADT Pattern Matching in Haskell
- George Karachalias\, Ghent University
DTSTART;TZID=Europe/London:20141022T140000
DTEND;TZID=Europe/London:20141022T150000
UID:TALK55356AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/55356
DESCRIPTION:Generalized Algebraic Data Types (GADTs) are a sim
ple but powerful generalization of Algebraic Data
Types (ADTs) in Haskell and the ML family.\n\nReas
oning about the accessibility of case branches and
the exhaustiveness of pattern matching is a well
studied and efficiently solved problem for ADTs. H
owever\, classic algorithms fall short in the pres
ence of GADTs\, issuing false warnings: Since GADT
constructors introduce local constraints\, we mus
t allow for the fact that particular combinations
of patterns and/or values cannot actually occur. \
n\nWe present a novel algorithm for checking patte
rn matching that accounts for Haskell's laziness a
nd relies on implication constraints generated and
solved by the OutsideIn(X) type inference engine.
Since we rely on the existing type inference engi
ne\, our approach is efficient and robust to futur
e extensions of the type system. We also report on
a proof-of-concept implementation of our algorith
m in GHC. \n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station R
oad\, Cambridge\, CB1 2FB
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR