A Short summary on polymorphic regular tree types and patterns
I reviewed [1] and summarize what I see as follows
The author present a parametric polymorphic type system for languages like XDuce and CDuce which operate on regular trees.
The paper can be divided into to two main parts.
1. A typed semantics : A more liberal polymorphic language.
For instance, the following program is typable in this system.
f :: forall a.(a|B) -> (a|())
f = Lambda a. lambda x:(a|B).
match x with
y:a -> y
B -> ()
To make the above program typable, the author defines the following rule in the subtyping system,
a<:a
Note that this program is rejected by [2], because it does not satisify the non-ambiguity constraint.
Note that a* is not expressible in this system, because of the type language does not handle concatenation. Hence our filter and map are not supported.
Their subtyping is complete if subtyping relation is interpreted as follows,
r1<:r2 iff for all substitution S, S(r1)<:S(r2).
Another question is why they require value matches a function pattern must be typable under the empty environment??
2. They present a untype semantics, (which is a language that does not support polymorphism). They show a type-driven approach to translate typable program in 1 into this system.
The trick can be summarized as follows,
2a. Remove all type abstraction and type application;
2b. Replace type variable by wild card type _
2c. Note that _ in 2 has same effect as Any type (I think).
Suppose we translate the running example as follows,
f = lambda x:(_|B).
match x with
(y:_) -> y
B -> ()
Note that the above translation is not faithful because in case the function is applied to a value B, the first pattern can be applied, but in the original program this is not always the case, (e.g. instantiate a with A)
The rest of the paper develop on how to detect cases where unfaithfulness would occur.
[1] Polymorphic Regular Tree Types and Patterns Jerome Vouillon POPL 2006
[2] Parametric Polymorphism for XML Hosoya Haruo, Alain Frisch and Guiseppe Castagna POPL 2005
The author present a parametric polymorphic type system for languages like XDuce and CDuce which operate on regular trees.
The paper can be divided into to two main parts.
1. A typed semantics : A more liberal polymorphic language.
For instance, the following program is typable in this system.
f :: forall a.(a|B) -> (a|())
f = Lambda a. lambda x:(a|B).
match x with
y:a -> y
B -> ()
To make the above program typable, the author defines the following rule in the subtyping system,
a<:a
Note that this program is rejected by [2], because it does not satisify the non-ambiguity constraint.
Note that a* is not expressible in this system, because of the type language does not handle concatenation. Hence our filter and map are not supported.
Their subtyping is complete if subtyping relation is interpreted as follows,
r1<:r2 iff for all substitution S, S(r1)<:S(r2).
Another question is why they require value matches a function pattern must be typable under the empty environment??
2. They present a untype semantics, (which is a language that does not support polymorphism). They show a type-driven approach to translate typable program in 1 into this system.
The trick can be summarized as follows,
2a. Remove all type abstraction and type application;
2b. Replace type variable by wild card type _
2c. Note that _ in 2 has same effect as Any type (I think).
Suppose we translate the running example as follows,
f = lambda x:(_|B).
match x with
(y:_) -> y
B -> ()
Note that the above translation is not faithful because in case the function is applied to a value B, the first pattern can be applied, but in the original program this is not always the case, (e.g. instantiate a with A)
The rest of the paper develop on how to detect cases where unfaithfulness would occur.
[1] Polymorphic Regular Tree Types and Patterns Jerome Vouillon POPL 2006
[2] Parametric Polymorphism for XML Hosoya Haruo, Alain Frisch and Guiseppe Castagna POPL 2005
