
On Tue, 18 Oct 2005, Martin Sulzmann wrote:
Semantic subtyping issue:
Assume we have a function f of type f :: Reg (r*) -> ... to which we pass a value x of type Reg (r,r*). We have that (r,r*) is a semantic subtype of r*, hence, the code f x is accepted in languages such as XDuce/CDuce.
I see. If I understand you correctly, this can be done like this: 1. Introducing a type constructor sub (T1, T2) to mean that T1 is a subtype of T2 2. Then introducing constructors to represent semantic subtyping rules (These constructors are justified semantically) 3. Then introducing the following function coerce: forall T1, T2. (sub (T1, T2), T1) -> T2 and prove that coerce can be erased at run-time. ------ In your example, we have a proof of the type sub (Reg (r, r*), Reg (r*)); let us call the proof pf; for x of the type Reg (r, r*), we can do f (coerce (pf, x)).
I'm just saying that the fact regexp can be represented via GADTs doesn't imply that we get the same expressive power of languages such as XDuce/CDuce.
My view is that XDuce/CDuce provides an automatic approach to constructing the part: coerce (pf, ...). But in terms of type theory, I am yet to see why it is more expressive. ------ We are currently debating whether the above approach to semantic subtyping should be added into ATS. The trouble is that there seems no good way of verifying semantic subtyping rules. Maybe we should just blame the user if things go wrong (including core dump) :) Cheers, --Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hwxi@cs.bu.edu Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department)