<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>
</p>
<div class="moz-text-flowed" style="font-family: -moz-fixed;
font-size: 14px;" lang="x-western">Good day,
<br>
<br>
I am currently developing a typechecker plugin for GHC for
realizing an idea
<br>
regarding types based on regular expressions to describe the
contents of a string.
<br>
This is done using type-level literals to denote a particular
regex. Additionally
<br>
there are additional constraints for working with such types. One
of those
<br>
constraints is called Intersectable and denotes whether an
intersection between
<br>
two regexes would be possible in the sense that there is some
common alphabet
<br>
between them. Furthermore there is a type-level function that
calculates the
<br>
actual intersection between two regex types and returns the
resulting regex type:
<br>
<br>
type family Intersectable (a :: Symbol) (b :: Symbol) ::
Constraint
<br>
type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol
<br>
<br>
Now i've created a typechecker plugin that resolves such
constraints by using a
<br>
finite-automata representation of the regexes to do the actual
work. While my
<br>
plugin is already able to proof progams where regexes are fully
applied, i.e. they
<br>
can reduce terms to a single regex and then verify the constraints
accordingly
<br>
or reject them, it fails to type "intermediate" functions. As a
small example
<br>
assume the following program:
<br>
<br>
checkFour :: Intersectable a "[0-4]" => RgxString a ->
RgxString (Intersection a "[0-4]")
<br>
checkFour a = undefined
<br>
<br>
checkEight :: Intersectable a "[0-8]" => RgxString a ->
RgxString (Intersection a "[0-8]")
<br>
checkEight a = undefined
<br>
<br>
test = checkFour . checkEight -- this fails to type correctly
<br>
test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*")
-- this works fine
<br>
<br>
The constraint solver wants me to proof the following constraints
for test:
<br>
<br>
tcPluginSolve
<br>
given = []
<br>
derived = []
<br>
wanted = [
<br>
[WD] irred_a2GV {0}:: Intersectable
<br>
(Intersection a0 "[0-8]")
<br>
"[0-4]" (CNonCanonical),
<br>
[WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)]
<br>
<br>
My plugin reduces the first constraint to Intersectable a0 [0-4]
as regex
<br>
intersection is commutative so i can intersect [0-8] with [0-4]
first. But i
<br>
haven't found out yet how i would tell the compiler to put this
reduced
<br>
constraint to the type signature instead of the current one where
the constraint
<br>
got dropped at all instead of at least remain unnormalized, and
the return type
<br>
remains unnormalized as well:
<br>
<br>
RgxString a -> RgxString (Intersection (Intersection a "[0-8]")
"[0-4]")
<br>
<br>
I'd need to tell the typechecker somehow that (Intersection
<br>
(Intersection a "[0-8]") "[0-4]") is equal to Intersection a
"[0-4]" so it substitutes
<br>
it accordingly. My idea is that i have to generate given type and
function equality
<br>
constraints during the typechecking telling it that those
representations are equal,
<br>
but i am really not sure what kind of constraints i need. CTyEqCan
for instance
<br>
seems to require a TyVar on one side while i though i could
generate something like
<br>
<br>
Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a
"[0-4]"
<br>
<br>
I have already tried a lot but there is little documentation on
the whole
<br>
constraint solving process and i am slowly getting stuck. Thanks
for helping!
<br>
</div>
</body>
</html>