Design Decisions on polymorphic XML transformation.
I summarize the issues and design decisions as follows.
Issue 1: Ambiguous Instantiation.
regtype A = A[]
regtype B = B[]
f :: (a,B,b) -> b
f (x :: (a,B), y :: b) = y
assume we apply f to value of type (B,B,A). There are at least two "ambiguous" type instances: (1) a = (), b = (B,A), and (2) a = B, b = A.
It either leads to loss of coherence or type unsoundness.
Design Decision 1:
a) Perform ambiguous check on type annotations. (Employed by Hosoya et al. POPL 2005)
b) Type application is provided by the programmer. (Employed by Vouillon POPL 2006) and Sulzmann and Lu PLAN-X 2006)
Issue 2: Pattern Inference.
f :: a* -> ()
f (x :: a+) = ()
f (x :: a*) = () --(2)
If we assume patterns are processed from top
to bottom, we can conclude that
type environment for pattern (2) is x::().
Design Decision 2:
a) Perform no pattern inference, and takes the pattern annotation litterally.
Pro : it is simple to translation, it should work for most of the realistic examples (Really?)
Con: It rejects some programs. The programmer needs to provide proper pattern annotations.
b) Perform a conservative inference.
Pro: It is not hard to extend intersection and difference to handle polymorphic variables. The system is sound.
Con: The system is incomplete. In case of inference failure, let the unsolvable constraints flow out as part of the function type annotations. It requires the programmere to provide addtional information to satisfy the constraints. And the generated constraints potentially lead to context-free solution.
Issue 3: Inference under (In)deterministic matching policy.
Inference w.r.t a deterministic matching policy helps to type more programs.
f :: a* -> ()
f (x::a*, y ::a*) = y
Design Decision 3: inference under deterministic
Pro: as mentioned above.
Con: It blows up the type annotation. In case of type error, the constraints might not be managible by the programmer.
Issue 4: Exhaustiveness Check
It is undecidable in general.
Design decision: Simple conservative check.
f :: r1 -> r2
f [pi = ei]
r1 <= \Cup \stript(pi)
Cons: The algorithm is incomplete. We might reject useful programs, (we need to compare this against Hosoya's approach). Otherwise, we let the unsatisfiable constraints flow out as annotation. I
Question : n case of type error, are the constraints managible by the programmers?
Issue 1: Ambiguous Instantiation.
regtype A = A[]
regtype B = B[]
f :: (a,B,b) -> b
f (x :: (a,B), y :: b) = y
assume we apply f to value of type (B,B,A). There are at least two "ambiguous" type instances: (1) a = (), b = (B,A), and (2) a = B, b = A.
It either leads to loss of coherence or type unsoundness.
Design Decision 1:
a) Perform ambiguous check on type annotations. (Employed by Hosoya et al. POPL 2005)
b) Type application is provided by the programmer. (Employed by Vouillon POPL 2006) and Sulzmann and Lu PLAN-X 2006)
Issue 2: Pattern Inference.
f :: a* -> ()
f (x :: a+) = ()
f (x :: a*) = () --(2)
If we assume patterns are processed from top
to bottom, we can conclude that
type environment for pattern (2) is x::().
Design Decision 2:
a) Perform no pattern inference, and takes the pattern annotation litterally.
Pro : it is simple to translation, it should work for most of the realistic examples (Really?)
Con: It rejects some programs. The programmer needs to provide proper pattern annotations.
b) Perform a conservative inference.
Pro: It is not hard to extend intersection and difference to handle polymorphic variables. The system is sound.
Con: The system is incomplete. In case of inference failure, let the unsolvable constraints flow out as part of the function type annotations. It requires the programmere to provide addtional information to satisfy the constraints. And the generated constraints potentially lead to context-free solution.
Issue 3: Inference under (In)deterministic matching policy.
Inference w.r.t a deterministic matching policy helps to type more programs.
f :: a* -> ()
f (x::a*, y ::a*) = y
Design Decision 3: inference under deterministic
Pro: as mentioned above.
Con: It blows up the type annotation. In case of type error, the constraints might not be managible by the programmer.
Issue 4: Exhaustiveness Check
It is undecidable in general.
Design decision: Simple conservative check.
f :: r1 -> r2
f [pi = ei]
r1 <= \Cup \stript(pi)
Cons: The algorithm is incomplete. We might reject useful programs, (we need to compare this against Hosoya's approach). Otherwise, we let the unsatisfiable constraints flow out as annotation. I
Question : n case of type error, are the constraints managible by the programmers?
