[Haskell-cafe] Regular Expressions, was Re: Interest in helping w/ Haskell standard

[Hongwei Xi]

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 at cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)