Typechecker Plugin Constraint Solving

Previous Topic Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

Typechecker Plugin Constraint Solving

Armin Wurzinger

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:

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!

Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.