|
|
CONVERSION ERROR
|
|
|
|
|
|
Error: HttpError (HttpExceptionRequest Request {
|
|
|
host = "ghc.haskell.org"
|
|
|
port = 443
|
|
|
secure = True
|
|
|
requestHeaders = []
|
|
|
path = "/trac/ghc/wiki/TypeFunctionsSynTC/PlanMS"
|
|
|
queryString = "?version=1"
|
|
|
method = "GET"
|
|
|
proxy = Nothing
|
|
|
rawBody = False
|
|
|
redirectCount = 10
|
|
|
responseTimeout = ResponseTimeoutDefault
|
|
|
requestVersion = HTTP/1.1
|
|
|
}
|
|
|
(StatusCodeException (Response {responseStatus = Status {statusCode = 403, statusMessage = "Forbidden"}, responseVersion = HTTP/1.1, responseHeaders = [("Date","Sun, 10 Mar 2019 07:00:00 GMT"),("Server","Apache/2.2.22 (Debian)"),("Strict-Transport-Security","max-age=63072000; includeSubDomains"),("Vary","Accept-Encoding"),("Content-Encoding","gzip"),("Content-Length","261"),("Content-Type","text/html; charset=iso-8859-1")], responseBody = (), responseCookieJar = CJ {expose = []}, responseClose' = ResponseClose}) "<!DOCTYPE HTML PUBLIC \"-//IETF//DTD HTML 2.0//EN\">\n<html><head>\n<title>403 Forbidden</title>\n</head><body>\n<h1>Forbidden</h1>\n<p>You don't have permission to access /trac/ghc/wiki/TypeFunctionsSynTC/PlanMS\non this server.</p>\n<hr>\n<address>Apache/2.2.22 (Debian) Server at ghc.haskell.org Port 443</address>\n</body></html>\n"))
|
|
|
|
|
|
Original source:
|
|
|
|
|
|
```trac
|
|
|
{{{
|
|
|
ALGORITHM
|
|
|
|
|
|
Ax axioms
|
|
|
C locals
|
|
|
W wanted
|
|
|
|
|
|
The task:
|
|
|
|
|
|
Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible).
|
|
|
|
|
|
For this purpose we normalize C and W, written (C | W) -->* (C' | W'),
|
|
|
by performing the following steps
|
|
|
|
|
|
- axiom step, apply axioms on C and W
|
|
|
- local step, build the closure of C
|
|
|
- wanted step, reduce W wrt C (in the axiom step we reduce W wrt Ax)
|
|
|
|
|
|
We can verify that W follows from C wrt Ax if
|
|
|
all constraints in W' are either True, or are syntactically
|
|
|
present in C'.
|
|
|
|
|
|
Normalization terminates if
|
|
|
- we have exhaustively applied the axiom and wanted steps and
|
|
|
- the set C' of locals remains stable (ie any local step
|
|
|
generates equations which are already present in C').
|
|
|
|
|
|
The individual normalization steps are:
|
|
|
(I'll skip the rigid/wobbly issue)
|
|
|
1) Axiom step (affects C and W)
|
|
|
|
|
|
We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W'
|
|
|
|
|
|
We exhaustively apply rewritings implied by Ax on terms
|
|
|
in C and W and obtain C' and W' (no surprise here).
|
|
|
We also apply the common rules such as
|
|
|
|
|
|
[t]=[s] --> t=s etc
|
|
|
|
|
|
2) Local step (affects only C)
|
|
|
|
|
|
We build the closure of all locals: (C | W) --> (C' | W)
|
|
|
|
|
|
Let s=t or t=s in C such that s \equiv S s1 ... sn where
|
|
|
S is a type function and si are terms
|
|
|
|
|
|
a) if s'[s] =t' in C
|
|
|
|
|
|
then C cup W --> C cup {s'[t]=t'} cup W
|
|
|
|
|
|
b) if t'=s'[s] in C
|
|
|
|
|
|
then C cup W --> C cup {t'=s'[t]} cup W
|
|
|
|
|
|
c) if s'=t'[t] in C
|
|
|
|
|
|
then C cup W --> C cup {s'=t'[s]} cup W
|
|
|
|
|
|
d) if t'[t]=s' in C
|
|
|
|
|
|
then C cup W --> C-{t'=s'} cup {t'[t]=s'} cup W
|
|
|
|
|
|
|
|
|
We write t[s] to denote the occurrence of a term s in
|
|
|
a term t.
|
|
|
|
|
|
Point to note:
|
|
|
We don't care about the orientation of locals.
|
|
|
The "order issue" is solved by simpling computing the fixpont (ie closure of C).
|
|
|
Steps a)-d) effectively build the closure of all local assumptions.
|
|
|
|
|
|
3) Wanted step (affects only W)
|
|
|
|
|
|
We rewrite W wrt C: (C | W) --> (C' | W)
|
|
|
|
|
|
Let s=t in C such that s \equiv S s1 ... sn where
|
|
|
S is a type function and si are terms
|
|
|
(NOTE: there was a typo in my earlier email,
|
|
|
I wrote "Let s=t in W ..." but of course we reduce W wrt C)
|
|
|
|
|
|
a') if s'[s] =t' in W
|
|
|
|
|
|
then C cup W --> C cup W-{s'=t'} cup {s'[t]=t'}
|
|
|
^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
we replace s'=t' by s'[t]=t'
|
|
|
|
|
|
Point to note:
|
|
|
|
|
|
We actually rewrite s'[s]=t' in W to s'[t]=t'.
|
|
|
The other cases b'), c') and d') are similar to the
|
|
|
above cases b), c) and d).
|
|
|
|
|
|
The above algorithm is inspired by the typefunction vs chr
|
|
|
correspondence.
|
|
|
|
|
|
How to build evidence during the application of
|
|
|
axiom, local and wanted steps is obvious
|
|
|
(but please yell if there's something I've overlooked).
|
|
|
|
|
|
|
|
|
EXAMPLES
|
|
|
|
|
|
Example 1:
|
|
|
|
|
|
forall a. S [a] = [S a] -- axiom, Ax
|
|
|
|
|
|
T Int = Int (2) -- locals, C
|
|
|
T [Int] = S [Int] (3)
|
|
|
T Int = S Int (4)
|
|
|
|
|
|
|
|
|
T [Int] = [Int] -- wanted, W
|
|
|
|
|
|
|
|
|
We'll only show the reduction of W.
|
|
|
|
|
|
T [Int] = [Int]
|
|
|
--> apply (3) from left to right
|
|
|
S [Int] = [Int]
|
|
|
--> apply axiom
|
|
|
[S Int] = [Int]
|
|
|
--> "decompose"
|
|
|
S Int = Int
|
|
|
--> apply (4) from right to left
|
|
|
T Int = Int
|
|
|
--> apply (2) from left to right
|
|
|
Int = Int
|
|
|
--> True
|
|
|
|
|
|
The above normalization steps can be mapped directly to CHR solving
|
|
|
steps. Application of axioms correspond to CHR rule applications.
|
|
|
Application of local assumptions correspond to FD rule applications.
|
|
|
|
|
|
|
|
|
Example 2:
|
|
|
|
|
|
no axioms
|
|
|
|
|
|
Bool = G Int (1) -- locals, C
|
|
|
F (G Int) = Int (2)
|
|
|
|
|
|
F Bool = Int -- wanted, W
|
|
|
|
|
|
In this example, we actually need to build the closure of C
|
|
|
to verify W.
|
|
|
|
|
|
We find that
|
|
|
|
|
|
Bool = G Int
|
|
|
F (G Int) = Int
|
|
|
|
|
|
-->* Bool = G Int
|
|
|
F (G Int) = Int
|
|
|
F Bool = Int
|
|
|
|
|
|
Thus, we can immediately verify W
|
|
|
|
|
|
|
|
|
TERMINATION OF NORMALIZATION
|
|
|
|
|
|
At this point you may wonder what about termination?
|
|
|
For example, in case of the local assumptions
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
we may repetively apply (2) on (1) and thus we keep adding in
|
|
|
"copies" of S Int = Int. Notice that normalization of C to the form C'
|
|
|
means that we apply the axiom and local steps until the set C' remains
|
|
|
stable. The claim is that the size of C' is bound. This must be the
|
|
|
case because the local steps correspond almost directly to FD rule
|
|
|
applications. For example, the above local assumptions
|
|
|
are represented as the following CHR constraints
|
|
|
|
|
|
T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
Application of the FD rule yields
|
|
|
|
|
|
b=Int, T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
<--> equivalent to
|
|
|
|
|
|
b=Int, T Int Int, S Int Int
|
|
|
|
|
|
the above can be interpreted as
|
|
|
|
|
|
T Int= Int
|
|
|
T Int = S Int
|
|
|
S Int = Int
|
|
|
|
|
|
The point here is that although the number of local steps may be
|
|
|
infinite, we'll eventually reach a stable constraint store.
|
|
|
As said above, each local step corresponds almost directly to a FD
|
|
|
rule application step.
|
|
|
Guess it may be more appropriate to say that the above method is
|
|
|
specificed declaratively rather than algorithmic.
|
|
|
(more on how to avoid infinite application of local steps below).
|
|
|
|
|
|
Actually, there's another termination issue.
|
|
|
Recall the earlier example
|
|
|
|
|
|
|
|
|
S [[Int]] = [T Int]
|
|
|
S [[Int]] = T Int
|
|
|
|
|
|
-->
|
|
|
|
|
|
T Int = [T Int]
|
|
|
S [[Int]] = [T Int]
|
|
|
S [[Int]] = T Int
|
|
|
|
|
|
It seems we have introduced a non-terminating local rewrite relation
|
|
|
T Int = [T Int]. As observed earlier, such "non-terminating"
|
|
|
relations correspond to inconsistent CHR stores.
|
|
|
I'm sure the condition that rewrite relations must be "decreasing"
|
|
|
is sufficient to guarantee termination, not sure whether it's also
|
|
|
necessary. The brute force method would be to translate
|
|
|
C cup W into its CHR form and check the CHR store for consistency.
|
|
|
|
|
|
AVOIDING INFINITE LOCAL STEPS/SMARTER LOCAL STEPS
|
|
|
|
|
|
Let's consider again the example
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
As observed above, normalization yields the fixpoint
|
|
|
|
|
|
T Int = Int
|
|
|
T Int = S Int
|
|
|
S Int = Int
|
|
|
|
|
|
but a naive algorithm may keep applying (2) on (1), thus
|
|
|
adding in the already present equation S Int = Int.
|
|
|
|
|
|
Is there a smart method to avoid infinite local steps?
|
|
|
(thus we don't need to check whether we've reached a fixpoint,
|
|
|
this may be costly).
|
|
|
We may get some insight from the CHR derivation. Eg
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
is represented as the CHR constraint store
|
|
|
|
|
|
T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
Application of the FD rule yields
|
|
|
|
|
|
b=Int, T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
<--> equivalent to
|
|
|
|
|
|
b=Int, T Int Int, S Int Int
|
|
|
|
|
|
In terms of the type function notation, we can thus argue that
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
is normalized to
|
|
|
|
|
|
T Int = Int
|
|
|
S Int = Int
|
|
|
|
|
|
There's no termination issue anymore. Of course, the details have yet
|
|
|
to be worked out.
|
|
|
}}}
|
|
|
``` |
|
|
```wiki
|
|
|
ALGORITHM
|
|
|
|
|
|
Ax axioms
|
|
|
C locals
|
|
|
W wanted
|
|
|
|
|
|
The task:
|
|
|
|
|
|
Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible).
|
|
|
|
|
|
For this purpose we normalize C and W, written (C | W) -->* (C' | W'),
|
|
|
by performing the following steps
|
|
|
|
|
|
- axiom step, apply axioms on C and W
|
|
|
- local step, build the closure of C
|
|
|
- wanted step, reduce W wrt C (in the axiom step we reduce W wrt Ax)
|
|
|
|
|
|
We can verify that W follows from C wrt Ax if
|
|
|
all constraints in W' are either True, or are syntactically
|
|
|
present in C'.
|
|
|
|
|
|
Normalization terminates if
|
|
|
- we have exhaustively applied the axiom and wanted steps and
|
|
|
- the set C' of locals remains stable (ie any local step
|
|
|
generates equations which are already present in C').
|
|
|
|
|
|
The individual normalization steps are:
|
|
|
(I'll skip the rigid/wobbly issue)
|
|
|
1) Axiom step (affects C and W)
|
|
|
|
|
|
We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W'
|
|
|
|
|
|
We exhaustively apply rewritings implied by Ax on terms
|
|
|
in C and W and obtain C' and W' (no surprise here).
|
|
|
We also apply the common rules such as
|
|
|
|
|
|
[t]=[s] --> t=s etc
|
|
|
|
|
|
2) Local step (affects only C)
|
|
|
|
|
|
We build the closure of all locals: (C | W) --> (C' | W)
|
|
|
|
|
|
Let s=t or t=s in C such that s \equiv S s1 ... sn where
|
|
|
S is a type function and si are terms
|
|
|
|
|
|
a) if s'[s] =t' in C
|
|
|
|
|
|
then C cup W --> C cup {s'[t]=t'} cup W
|
|
|
|
|
|
b) if t'=s'[s] in C
|
|
|
|
|
|
then C cup W --> C cup {t'=s'[t]} cup W
|
|
|
|
|
|
c) if s'=t'[t] in C
|
|
|
|
|
|
then C cup W --> C cup {s'=t'[s]} cup W
|
|
|
|
|
|
d) if t'[t]=s' in C
|
|
|
|
|
|
then C cup W --> C-{t'=s'} cup {t'[t]=s'} cup W
|
|
|
|
|
|
|
|
|
We write t[s] to denote the occurrence of a term s in
|
|
|
a term t.
|
|
|
|
|
|
Point to note:
|
|
|
We don't care about the orientation of locals.
|
|
|
The "order issue" is solved by simpling computing the fixpont (ie closure of C).
|
|
|
Steps a)-d) effectively build the closure of all local assumptions.
|
|
|
|
|
|
3) Wanted step (affects only W)
|
|
|
|
|
|
We rewrite W wrt C: (C | W) --> (C' | W)
|
|
|
|
|
|
Let s=t in C such that s \equiv S s1 ... sn where
|
|
|
S is a type function and si are terms
|
|
|
(NOTE: there was a typo in my earlier email,
|
|
|
I wrote "Let s=t in W ..." but of course we reduce W wrt C)
|
|
|
|
|
|
a') if s'[s] =t' in W
|
|
|
|
|
|
then C cup W --> C cup W-{s'=t'} cup {s'[t]=t'}
|
|
|
^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
we replace s'=t' by s'[t]=t'
|
|
|
|
|
|
Point to note:
|
|
|
|
|
|
We actually rewrite s'[s]=t' in W to s'[t]=t'.
|
|
|
The other cases b'), c') and d') are similar to the
|
|
|
above cases b), c) and d).
|
|
|
|
|
|
The above algorithm is inspired by the typefunction vs chr
|
|
|
correspondence.
|
|
|
|
|
|
How to build evidence during the application of
|
|
|
axiom, local and wanted steps is obvious
|
|
|
(but please yell if there's something I've overlooked).
|
|
|
|
|
|
|
|
|
EXAMPLES
|
|
|
|
|
|
Example 1:
|
|
|
|
|
|
forall a. S [a] = [S a] -- axiom, Ax
|
|
|
|
|
|
T Int = Int (2) -- locals, C
|
|
|
T [Int] = S [Int] (3)
|
|
|
T Int = S Int (4)
|
|
|
|
|
|
|
|
|
T [Int] = [Int] -- wanted, W
|
|
|
|
|
|
|
|
|
We'll only show the reduction of W.
|
|
|
|
|
|
T [Int] = [Int]
|
|
|
--> apply (3) from left to right
|
|
|
S [Int] = [Int]
|
|
|
--> apply axiom
|
|
|
[S Int] = [Int]
|
|
|
--> "decompose"
|
|
|
S Int = Int
|
|
|
--> apply (4) from right to left
|
|
|
T Int = Int
|
|
|
--> apply (2) from left to right
|
|
|
Int = Int
|
|
|
--> True
|
|
|
|
|
|
The above normalization steps can be mapped directly to CHR solving
|
|
|
steps. Application of axioms correspond to CHR rule applications.
|
|
|
Application of local assumptions correspond to FD rule applications.
|
|
|
|
|
|
|
|
|
Example 2:
|
|
|
|
|
|
no axioms
|
|
|
|
|
|
Bool = G Int (1) -- locals, C
|
|
|
F (G Int) = Int (2)
|
|
|
|
|
|
F Bool = Int -- wanted, W
|
|
|
|
|
|
In this example, we actually need to build the closure of C
|
|
|
to verify W.
|
|
|
|
|
|
We find that
|
|
|
|
|
|
Bool = G Int
|
|
|
F (G Int) = Int
|
|
|
|
|
|
-->* Bool = G Int
|
|
|
F (G Int) = Int
|
|
|
F Bool = Int
|
|
|
|
|
|
Thus, we can immediately verify W
|
|
|
|
|
|
|
|
|
TERMINATION OF NORMALIZATION
|
|
|
|
|
|
At this point you may wonder what about termination?
|
|
|
For example, in case of the local assumptions
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
we may repetively apply (2) on (1) and thus we keep adding in
|
|
|
"copies" of S Int = Int. Notice that normalization of C to the form C'
|
|
|
means that we apply the axiom and local steps until the set C' remains
|
|
|
stable. The claim is that the size of C' is bound. This must be the
|
|
|
case because the local steps correspond almost directly to FD rule
|
|
|
applications. For example, the above local assumptions
|
|
|
are represented as the following CHR constraints
|
|
|
|
|
|
T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
Application of the FD rule yields
|
|
|
|
|
|
b=Int, T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
<--> equivalent to
|
|
|
|
|
|
b=Int, T Int Int, S Int Int
|
|
|
|
|
|
the above can be interpreted as
|
|
|
|
|
|
T Int= Int
|
|
|
T Int = S Int
|
|
|
S Int = Int
|
|
|
|
|
|
The point here is that although the number of local steps may be
|
|
|
infinite, we'll eventually reach a stable constraint store.
|
|
|
As said above, each local step corresponds almost directly to a FD
|
|
|
rule application step.
|
|
|
Guess it may be more appropriate to say that the above method is
|
|
|
specificed declaratively rather than algorithmic.
|
|
|
(more on how to avoid infinite application of local steps below).
|
|
|
|
|
|
Actually, there's another termination issue.
|
|
|
Recall the earlier example
|
|
|
|
|
|
|
|
|
S [[Int]] = [T Int]
|
|
|
S [[Int]] = T Int
|
|
|
|
|
|
-->
|
|
|
|
|
|
T Int = [T Int]
|
|
|
S [[Int]] = [T Int]
|
|
|
S [[Int]] = T Int
|
|
|
|
|
|
It seems we have introduced a non-terminating local rewrite relation
|
|
|
T Int = [T Int]. As observed earlier, such "non-terminating"
|
|
|
relations correspond to inconsistent CHR stores.
|
|
|
I'm sure the condition that rewrite relations must be "decreasing"
|
|
|
is sufficient to guarantee termination, not sure whether it's also
|
|
|
necessary. The brute force method would be to translate
|
|
|
C cup W into its CHR form and check the CHR store for consistency.
|
|
|
|
|
|
AVOIDING INFINITE LOCAL STEPS/SMARTER LOCAL STEPS
|
|
|
|
|
|
Let's consider again the example
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
As observed above, normalization yields the fixpoint
|
|
|
|
|
|
T Int = Int
|
|
|
T Int = S Int
|
|
|
S Int = Int
|
|
|
|
|
|
but a naive algorithm may keep applying (2) on (1), thus
|
|
|
adding in the already present equation S Int = Int.
|
|
|
|
|
|
Is there a smart method to avoid infinite local steps?
|
|
|
(thus we don't need to check whether we've reached a fixpoint,
|
|
|
this may be costly).
|
|
|
We may get some insight from the CHR derivation. Eg
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
is represented as the CHR constraint store
|
|
|
|
|
|
T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
Application of the FD rule yields
|
|
|
|
|
|
b=Int, T Int Int,
|
|
|
T Int b, S Int b
|
|
|
|
|
|
<--> equivalent to
|
|
|
|
|
|
b=Int, T Int Int, S Int Int
|
|
|
|
|
|
In terms of the type function notation, we can thus argue that
|
|
|
|
|
|
T Int = Int (1)
|
|
|
T Int = S Int (2)
|
|
|
|
|
|
is normalized to
|
|
|
|
|
|
T Int = Int
|
|
|
S Int = Int
|
|
|
|
|
|
There's no termination issue anymore. Of course, the details have yet
|
|
|
to be worked out.
|
|
|
``` |
|
|
\ No newline at end of file |