[Haskell-cafe] Regular Expressions, was Re: Interest in helping
w/ Haskell standard
hwxi at cs.bu.edu
Tue Oct 18 09:27:12 EDT 2005
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) :)
Computer Science Department
111 Cummington Street
Boston, MA 02215
Email: hwxi at cs.bu.edu
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)
More information about the Haskell-Cafe