[Haskell-cafe] Typechecker Plugin Constraint Solving
Armin Wurzinger
e1528532 at student.tuwien.ac.at
Wed Jul 4 15:23:10 UTC 2018
Good day,
I am currently developing a typechecker plugin for GHC for realizing an
idea
regarding types based on regular expressions to describe the contents of
a string.
This is done using type-level literals to denote a particular regex.
Additionally
there are additional constraints for working with such types. One of those
constraints is called Intersectable and denotes whether an intersection
between
two regexes would be possible in the sense that there is some common
alphabet
between them. Furthermore there is a type-level function that calculates
the
actual intersection between two regex types and returns the resulting
regex type:
type family Intersectable (a :: Symbol) (b :: Symbol) :: Constraint
type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol
Now i've created a typechecker plugin that resolves such constraints by
using a
finite-automata representation of the regexes to do the actual work.
While my
plugin is already able to proof progams where regexes are fully applied,
i.e. they
can reduce terms to a single regex and then verify the constraints
accordingly
or reject them, it fails to type "intermediate" functions. As a small
example
assume the following program:
checkFour :: Intersectable a "[0-4]" => RgxString a -> RgxString
(Intersection a "[0-4]")
checkFour a = undefined
checkEight :: Intersectable a "[0-8]" => RgxString a -> RgxString
(Intersection a "[0-8]")
checkEight a = undefined
test = checkFour . checkEight -- this fails to type correctly
test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*") -- this
works fine
The constraint solver wants me to proof the following constraints for test:
tcPluginSolve
given = []
derived = []
wanted = [
[WD] irred_a2GV {0}:: Intersectable
(Intersection a0 "[0-8]")
"[0-4]" (CNonCanonical),
[WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)]
My plugin reduces the first constraint to Intersectable a0 [0-4] as regex
intersection is commutative so i can intersect [0-8] with [0-4] first.
But i
haven't found out yet how i would tell the compiler to put this reduced
constraint to the type signature instead of the current one where the
constraint
got dropped at all instead of at least remain unnormalized, and the
return type
remains unnormalized as well:
RgxString a -> RgxString (Intersection (Intersection a "[0-8]") "[0-4]")
I'd need to tell the typechecker somehow that (Intersection
(Intersection a "[0-8]") "[0-4]") is equal to Intersection a "[0-4]" so
it substitutes
it accordingly. My idea is that i have to generate given type and
function equality
constraints during the typechecking telling it that those
representations are equal,
but i am really not sure what kind of constraints i need. CTyEqCan for
instance
seems to require a TyVar on one side while i though i could generate
something like
Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a "[0-4]"
I have already tried a lot but there is little documentation on the whole
constraint solving process and i am slowly getting stuck. Thanks for
helping!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180704/e882f654/attachment.html>
More information about the Haskell-Cafe
mailing list